The DOI matches its Crossref record; 26 of the 26 references it cites were found in a registry or an index.
Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL( T )
Abstract
We first introduce Abstract DPLL , 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 lazy approach 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( X ) engine, whose parameter X can be instantiated with a specialized solver Solver T for a given theory T , thus producing a DPLL( T ) system. We describe the high-level design of DPLL( X ) and its cooperation with Solver T , discuss the role of theory propagation , and describe different DPLL( T ) strategies for some theories arising in industrial applications.Our extensive experimental evidence, summarized in this article, shows that DPLL( T ) systems can significantly outperform the other state-of-the-art tools, frequently even in orders of magnitude, and have better scaling properties.
Overview
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Citations
Cites
Lecture Notes in Artificial Intelligence
Brézillon, P., & Bouquet, P. (1999) · Cited by 7,473
Theory of Linear and Integer Programming
Letchford, A. N., & Schrijver, A. (2000) · The Journal of the Operational Research Society · doi:10.2307/253980 · Cited by 5,515
A machine program for theorem-proving
Davis, M., Logemann, G., & Loveland, D. (1962) · Communications of the ACM · doi:10.1145/368273.368557 · Cited by 3,220
Chaff: engineering an efficient SAT solver
Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., & Malik, S. (2001) · Proceedings of the 38th conference on Design automation - DAC '01 · doi:10.1145/378239.379017 · Cited by 2,940
Theory of Linear and Integer Programming
Smith, D. K. (1987) · Journal of the Operational Research Society · doi:10.1057/jors.1987.94 · Cited by 2,708
A Computing Procedure for Quantification Theory
Davis, M., & Putnam, H. (1960) · Journal of the ACM · doi:10.1145/321033.321034 · Cited by 2,647
Eén, N., & Sörensson, N. (2004) · Lecture Notes in Computer Science · doi:10.1007/978-3-540-24605-3_37 · Cited by 2,629
GRASP: a search algorithm for propositional satisfiability
Marques-Silva, J. P., & Sakallah, K. A. (1999) · IEEE Transactions on Computers · doi:10.1109/12.769433 · Cited by 1,374
Constraint logic programming: a survey
Jaffar, J., & Maher, M. J. (1994) · The Journal of Logic Programming · doi:10.1016/0743-1066(94)90033-7 · Cited by 1,312
Efficient Conflict Driven Learning in a Boolean Satisfiability Solver
Zhang, L., Madigan, C. F., Moskewicz, M. H., & Malik, S. (2001) · Cited by 682
Cited by
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
Katz, G., Barrett, C., Dill, D. L., Julian, K., & Kochenderfer, M. J. (2017) · Lecture Notes in Computer Science · doi:10.1007/978-3-319-63387-9_5 · Cited by 1,706
Satisfiability Modulo Theories
Barrett, C., & Tinelli, C. (2018) · Handbook of Model Checking · doi:10.1007/978-3-319-10575-8_11 · Cited by 1,122
Self-citationcvc5: A Versatile and Industrial-Strength SMT Solver
Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., et al. (2022) · Lecture Notes in Computer Science · doi:10.1007/978-3-030-99524-9_24 · Cited by 468
Self-citationMulti-shot ASP solving with clingo
GEBSER, M., KAMINSKI, R., KAUFMANN, B., & SCHAUB, T. (2019) · Theory and Practice of Logic Programming · doi:10.1017/s1471068418000054 · Cited by 309
Clingo = ASP + Control: Preliminary Report
Gebser, M., Kaminski, R., Kaufmann, B., & Schaub, T. (2014) · arXiv · doi:10.48550/arxiv.1405.3694 · Cited by 230
Metadata
- Authors
- Nieuwenhuis, R., Oliveras, A., & Tinelli, C.
- Venue
- Journal of the ACM
- Published
- 2006-11
- Volume
- 53
- Issue
- 6
- Pages
- 937-977
- ISSN
- 0004-5411 (ISSN-L)
- 1557-735X
- OpenAlex
- W2022846948
- Cited by
- 783
- References
- 26
- FWCI
- 34.51
- Type
- journal article
- Language
- en
- Open access
- closed
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
How to cite
Cite CoChat for the checks on this page, and the paper for its own findings.
- This page
- CoChat. (2026). Citation check: Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL( T ). https://app.cochat.ai/papers/10.1145/1217856.1217859
- The paper
- Nieuwenhuis, R., Oliveras, A., & Tinelli, C. (2006). Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL( T ). Journal of the ACM. https://doi.org/10.1145/1217856.1217859
Data sources
Bibliographic data: Semantic Scholar, OpenAlex, Crossref.
Contains information from the Semantic Scholar Academic Graph Datasets, made available under the ODC Attribution License (ODC-BY 1.0).
Semantic Scholar’s data is described in: Kinney, R., et al. (2023). The Semantic Scholar Open Data Platform. arXiv:2301.10140.
