{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,28]],"date-time":"2026-10-28T00:32:13Z","timestamp":1793147533942,"version":"4.5.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"6","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2006,11]]},"abstract":"<jats:p>\n                    We first introduce\n                    <jats:italic>Abstract DPLL<\/jats:italic>\n                    , a rule-based formulation of the Davis--Putnam--Logemann--Loveland (DPLL) procedure for propositional satisfiability. This abstract framework allows one to cleanly express practical DPLL algorithms and to formally reason about them in a simple way. Its properties, such as soundness, completeness or termination, immediately carry over to the modern DPLL implementations with features such as backjumping or clause learning.We then extend the framework to Satisfiability Modulo background Theories (SMT) and use it to model several variants of the so-called\n                    <jats:italic>lazy approach<\/jats:italic>\n                    for SMT. In particular, we use it to introduce a few variants of a new, efficient and modular approach for SMT based on a general DPLL(\n                    <jats:italic>X<\/jats:italic>\n                    ) engine, whose parameter\n                    <jats:italic>X<\/jats:italic>\n                    can be instantiated with a specialized solver\n                    <jats:italic>Solver<\/jats:italic>\n                    <jats:sub>\n                      <jats:italic>T<\/jats:italic>\n                    <\/jats:sub>\n                    for a given theory\n                    <jats:italic>T<\/jats:italic>\n                    , thus producing a DPLL(\n                    <jats:italic>T<\/jats:italic>\n                    ) system. We describe the high-level design of DPLL(\n                    <jats:italic>X<\/jats:italic>\n                    ) and its cooperation with\n                    <jats:italic>Solver<\/jats:italic>\n                    <jats:sub>\n                      <jats:italic>T<\/jats:italic>\n                    <\/jats:sub>\n                    , discuss the role of\n                    <jats:italic>theory propagation<\/jats:italic>\n                    , and describe different DPLL(\n                    <jats:italic>T<\/jats:italic>\n                    ) strategies for some theories arising in industrial applications.Our extensive experimental evidence, summarized in this article, shows that DPLL(\n                    <jats:italic>T<\/jats:italic>\n                    ) systems can significantly outperform the other state-of-the-art tools, frequently even in orders of magnitude, and have better scaling properties.\n                  <\/jats:p>","DOI":"10.1145\/1217856.1217859","type":"journal-article","created":{"date-parts":[[2007,4,5]],"date-time":"2007-04-05T15:20:08Z","timestamp":1175786408000},"page":"937-977","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":554,"title":["Solving SAT and SAT Modulo Theories"],"prefix":"10.1145","volume":"53","author":[{"given":"Robert","family":"Nieuwenhuis","sequence":"first","affiliation":[{"name":"Technical University of Catalonia, Barcelona, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Albert","family":"Oliveras","sequence":"additional","affiliation":[{"name":"Technical University of Catalonia, Barcelona, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[{"name":"The University of Iowa, Iowa City, Iowa"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2006,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/647768.733787"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 5th European Conference on Planning","volume":"1809","author":"Armando A."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT","author":"Armando A.","year":"2004"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the CADE-18","volume":"2392","author":"Audemard G."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04)","volume":"3114","author":"Ball T."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_4"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 14th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science","volume":"2404","author":"Barrett C."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 1st International Conference on Formal Methods in Computer Aided Design. Lecture Notes in Computer Science","volume":"1166","author":"Barrett C."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04)","volume":"3114","author":"Barrett C. W."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 14th National Conference on Artificial Intelligence (AAAI'97)","author":"Bayardo R. J. J."},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of IJCAI-03","author":"Beame P."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799352474"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_21"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/371282.371364"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 14th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science","volume":"2404","author":"Bryant R."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/566385.566390"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 6th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science","volume":"818","author":"Burch J. R."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 5th International Symposium on the Theory and Applications of Satisfiability Testing (SAT'02)","author":"de Moura L."},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04)","volume":"3114","author":"de Moura L."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning","author":"de Moura L."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322228"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT). 502--518","author":"E\u00e9n N."},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 13th International Conference on Computer Aided Verification (CAV'2001)","volume":"2102","author":"Filli\u00e2tre J.-C."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 15th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science","volume":"2725","author":"Flanagan C."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04)","volume":"3114","author":"Ganzinger H."},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the Symposium on Design, Automation, and Test in Europe (DATE '02)","author":"Goldberg E."},{"key":"e_1_2_1_30_1","volume-title":"Model Theory. Enclyclopedia of mathematics and its applications","author":"Hodges W."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90033-7"},{"key":"e_1_2_1_32_1","volume-title":"16th International Conference (CAV). Lecture Notes in Computer Science","volume":"3114","author":"Lahiri S. K."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2005.1487914"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.257"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_32"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 10h International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), M. Vardi and A. Voronkov, Eds. Lecture Notes in Artificial Intellegence","volume":"2850","author":"Nieuwenhuis R."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_33"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_33"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the 11th International Conference Logic for Programming, Artificial Intelligence and Reasoning (LPAR). F. Baader and A. Voronkov, Eds. Lecture Notes in Computer Science","volume":"3452","author":"Nieuwenhuis R."},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the 11th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science","volume":"1633","author":"Pnueli A."},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the 1st Workshop on Pragmatics of Decision Procedures in Automated Reasoning","author":"Ranise S."},{"key":"e_1_2_1_45_1","volume-title":"Theory of Linear and Integer Programming","author":"Schrijver A."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775945"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS","author":"Seshia S. A.","year":"2004"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/646187.683257"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the 14th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol 2404","author":"Strichman O."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_34"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_12"},{"key":"e_1_2_1_53_1","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Proceedings of the 8th European Conference on Logics in Artificial Intelligence","author":"Tinelli C."},{"key":"e_1_2_1_54_1","unstructured":"Tinelli C. and Ranise S. 2005. SMT-LIB: The Satisfiability Modulo Theories Library. http:\/\/goedel.cs.uiowa.edu\/smtlib\/.]]  Tinelli C. and Ranise S. 2005. SMT-LIB: The Satisfiability Modulo Theories Library. http:\/\/goedel.cs.uiowa.edu\/smtlib\/.]]"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/648233.753307"},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the International Conference on Computer-Aided Design (ICCAD'01)","author":"Zhang L."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/789083.1022835"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1217856.1217859","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T16:32:25Z","timestamp":1672245145000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1217856.1217859"}},"subtitle":["From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(\n                    <i>T<\/i>\n                    )"],"short-title":[],"issued":{"date-parts":[[2006,11]]},"references-count":54,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2006,11]]}},"alternative-id":["10.1145\/1217856.1217859"],"URL":"https:\/\/doi.org\/10.1145\/1217856.1217859","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,11]]},"assertion":[{"value":"2006-11-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}