{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T21:02:35Z","timestamp":1791061355921,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540252368","type":"print"},{"value":"9783540322757","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32275-7_3","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T21:14:41Z","timestamp":1292879681000},"page":"36-50","source":"Crossref","is-referenced-by-count":49,"title":["Abstract DPLL and Abstract DPLL Modulo Theories"],"prefix":"10.1007","author":[{"given":"Robert","family":"Nieuwenhuis","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Albert","family":"Oliveras","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/3-540-45620-1_17","volume-title":"Automated Deduction - CADE-18","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 195\u2013210. Springer, Heidelberg (2002)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/10720246_8","volume-title":"Recent Advances in AI Planning","author":"A. Armando","year":"2000","unstructured":"Armando, A., Castellini, C., Giunchiglia, E.: SATbased procedures for temporal reasoning. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS, vol.\u00a01809, pp. 97\u2013108. Springer, Heidelberg (2000)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2004","unstructured":"Barrett, C.W., Berezin, S.: CVC lite: A new implementation of the cooperating validity checker. Category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-45657-0_18","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2002","unstructured":"Barrett, C., Dill, D., Stump, A.: Checking satisfiability of first-order formulas by incremental translation into sat. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 236. Springer, Heidelberg (2002)"},{"issue":"7","key":"3_CR5","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Comm. of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Comm. of the ACM"},{"key":"3_CR6","unstructured":"de Moura, L., Rue\u00df, H.: Lemmas on demand for satisfiability solvers. In: Procs. 5th Int. Symp. on the Theory and Applications of Satisfiability Testing, SAT 2002, pp. 244\u2013251 (2002)"},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Computer Aided Verification","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explanation. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 355\u2013367. Springer, Heidelberg (2003)"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT-solver. In: Design, Automation, and Test in Europe (DATE 2002), pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. 38th Design Automation Conference (DAC 2001) (2001)","DOI":"10.1145\/378239.379017"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Comput.\u00a048(5), 506\u2013521","DOI":"10.1109\/12.769433"},{"key":"3_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-45757-7_26","volume-title":"Logics in Artificial Intelligence","author":"C. Tinelli","year":"2002","unstructured":"Tinelli, C.: A DPLL-based calculus for ground satisfiability modulo theories. In: Flesca, S., Greco, S., Leone, N., Ianni, G. (eds.) JELIA 2002. LNCS (LNAI), vol.\u00a02424, pp. 308\u2013319. Springer, Heidelberg (2002)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/3-540-63104-6_28","volume-title":"Automated Deduction - CADE-14","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32275-7_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:35:12Z","timestamp":1605760512000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32275-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540252368","9783540322757"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32275-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}