Take a look at the new version of this page: [ beta version ]. Tell us what you think.

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.

REFERENCES

• 1: Rajeev Alur, Timed Automata, Proceedings of the 11th International Conference on Computer Aided Verification, p.8-22, July 06-10, 1999
• 2: Alessandro Armando , Claudio Castellini , Enrico Giunchiglia, SAT-Based Procedures for Temporal Reasoning, Proceedings of the 5th European Conference on Planning: Recent Advances in AI Planning, p.97-108, September 08-10, 1999
• 3: Armando, A., Castellini, C., Giunchiglia, E., and Maratea, M. 2004. A SAT-based decision procedure for the Boolean combination of difference constraints. In Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004). Lecture Notes in Computer Science. Springer-Verlag, New York.
• 4: Gilles Audemard , Piergiorgio Bertoli , Alessandro Cimatti , Artur Kornilowicz , Roberto Sebastiani, A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions, Proceedings of the 18th International Conference on Automated Deduction, p.195-210, July 27-30, 2002
• 5: Ball, T., Cook, B., Lahiri, S. K., and Zhang, L. 2004. Zapato: Automatic theorem proving for predicate abstraction refinement. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04) (Boston, MA). R. Alur and D. Peled, Eds. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, New York. 457--461.
• 6: Barrett, C., de Moura, L., and Stump, A. 2005. SMT-COMP: Satisfiability modulo theories competition. In Proceedings of the 17th International Conference on Computer Aided Verification, K. Etessami and S. Rajamani, Eds. Lecture Notes in Computer Science, vol. 3576. Springer-Verlag, New York, 20--23. (See www.csl.sri.com/users/demoura/smt-comp.)
• 7: Clark W. Barrett , David L. Dill , Aaron Stump, Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT, Proceedings of the 14th International Conference on Computer Aided Verification, p.236-249, July 27-31, 2002
• 8: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, Validity Checking for Combinations of Theories with Equality, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.187-201, November 06-08, 1996
• 9: Barrett, C. W. 2003. Checking validity of quantifier-free formulas in combinations of first-order theories. Ph.D. dissertation. Stanford University, Stanford, CA.
• 10: Barrett, C. W., and Berezin, S. 2004. CVC lite: A new implementation of the cooperating validity checker. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04) (Boston, MA). R. Alur and D. Peled, Eds. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, New York, 515--518.
• 11: Bayardo, R. J. J., and Schrag, R. C. 1997. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the 14th National Conference on Artificial Intelligence (AAAI'97) (Providence, RI), 203--208.
• 12: Beame, P., Kautz, H., and Sabharwal, A. 2003. On the power of clause learning. In Proceedings of IJCAI-03, 18th International Joint Conference on Artificial Intelligence (Acapulco, MX).
• 13: Maria Luisa Bonet , Juan Luis Esteban , Nicola Galesi , Jan Johannsen, On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems, SIAM Journal on Computing, v.30 n.5, p.1462-1484, 2000 [doi>10.1137/S0097539799352474]
• 14: Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T. V. Rossum, P., Schulz, S., and Sebastiani, R. 2005. An incremental and layered procedure for the satisfiability of linear arithmetic logic. In Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference (TACAS). Lecture Notes in Computer Science, vol. 3440. Springer-Verlag, New York, 317--333.
• 15: Randal E. Bryant , Steven German , Miroslav N. Velev, Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.93-134, Jan. 2001 [doi>10.1145/371282.371364]
• 16: Randal E. Bryant , Shuvendu K. Lahiri , Sanjit A. Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Proceedings of the 14th International Conference on Computer Aided Verification, p.78-92, July 27-31, 2002
• 17: Randal E. Bryant , Miroslav N. Velev, Boolean satisfiability with transitivity constraints, ACM Transactions on Computational Logic (TOCL), v.3 n.4, p.604-627, October 2002 [doi>10.1145/566385.566390]
• 18: Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
• 19: Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
• 20: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 21: de Moura, L., and Rueß, H. 2002. Lemmas on demand for satisfiability solvers. In Proceedings of the 5th International Symposium on the Theory and Applications of Satisfiability Testing (SAT'02). 244--251.
• 22: de Moura, L., and Ruess, H. 2004. An experimental evaluation of ground decision procedures. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04) (Boston, MA). R. Alur and D. Peled, Eds. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, New York, 162--174.
• 23: de Moura, L., Rueß, H., and Shankar, N. 2004. Justifying equality. In Proceedings of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (Cork, Ireland).
• 24: Peter J. Downey , Ravi Sethi , Robert Endre Tarjan, Variations on the Common Subexpression Problem, Journal of the ACM (JACM), v.27 n.4, p.758-771, Oct. 1980 [doi>10.1145/322217.322228]
• 25: Eén, N., and Sörensson, N. 2003. An extensible SAT-solver. In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT). 502--518.
• 26: Jean-Christophe Filliâtre , Sam Owre , Harald Rueß , Natarajan Shankar, ICS: Integrated Canonizer and Solver, Proceedings of the 13th International Conference on Computer Aided Verification, p.246-249, July 18-22, 2001
• 27: Flanagan, C., Joshi, R., Ou, X., and Saxe, J. B. 2003. Theorem proving using lazy proof explanation. In Proceedings of the 15th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 2725. Springer-Verlag, New York.
• 28: Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., and Tinelli, C. 2004. DPLL(T): Fast Decision Procedures. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04) (Boston, MA). R. Alur and D. Peled, Eds. Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, New York, 175--188.
• 29: E. Goldberg , Y. Novikov, BerkMin: A Fast and Robust Sat-Solver, Proceedings of the conference on Design, automation and test in Europe, p.142, March 04-08, 2002
• 30: Hodges, W. 1993. Model Theory. Enclyclopedia of mathematics and its applications, vol. 42. Cambridge University Press, Cambridge, MA.
• 31: Jaffar, J., and Maher, M. 1994. Constraint Logic Programming: A Survey. J. Logic Prog. 19/20, 503--581.
• 32: Lahiri, S. K., and Seshia, S. A. 2004. The UCLID Decision Procedure. In Computer Aided Verification, 16th International Conference (CAV). Lecture Notes in Computer Science, vol. 3114. Springer-Verlag, New York, 475--478.
• 33: Manolios, P., and Srinivasan, S. K. 2005a. A computationally efficient method based on commitment refinement maps for verifying pipelined machines. In Proceedings of the ACM IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE). ACM, New York.
• 34: Panagiotis Manolios , Sudarshan K. Srinivasan, Refinement Maps for Efficient Verification of Processor Models, Proceedings of the conference on Design, Automation and Test in Europe, p.1304-1309, March 07-11, 2005 [doi>10.1109/DATE.2005.257]
• 35: João P. Marques-Silva , Karem A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, v.48 n.5, p.506-521, May 1999 [doi>10.1109/12.769433]
• 36: Meir, O., and Strichman, O. 2005. Yet another decision procedure for equality logic. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV'05) (Edimburgh, Scotland). K. Etessami and S. K. Rajamani, Eds. Lecture Notes in Computer Science, vol. 3576. Springer-Verlag, New York, 307--320.
• 37: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 38: Nieuwenhuis, R., and Oliveras, A. 2003. Congruence Closure with Integer Offsets. In 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, vol. 2850. Springer-Verlag, New York, 2850. 78--90.
• 39: Nieuwenhuis, R., and Oliveras, A. 2005a. DPLL(T) with exhaustive theory propagation and its application to difference logic. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV'05) (Edimburgh, Scotland). K. Etessami and S. K. Rajamani, Eds. Lecture Notes in Computer Science, vol. 3576. Springer-Verlag, New York, 321--334.
• 40: Nieuwenhuis, R., and Oliveras, A. 2005b. Proof-producing congruence closure. In Proceedings of the 16th International Conference on Term Rewriting and Applications (RTA'05) (Nara, Japan). J. Giesl, Ed. Lecture Notes in Computer Science, vol. 3467. Springer-Verlag, New York, 453--468.
• 41: Nieuwenhuis, R., Oliveras, A., and Tinelli, C. 2005. Abstract DPLL and abstract DPLL modulo theories. In 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, vol. 3452. Springer-Verlag, New York, 36--50.
• 42: Amir Pnueli , Yoav Rodeh , Ofer Shtrichman , Michael Siegel, Deciding Equality Formulas by Small Domains Instantiations, Proceedings of the 11th International Conference on Computer Aided Verification, p.455-469, July 06-10, 1999
• 43: Ranise, S., and Tinelli, C. 2003. The SMT-LIB format: An initial proposal. In Proceedings of the 1st Workshop on Pragmatics of Decision Procedures in Automated Reasoning. Miami.
• 44: Ryan, L. 2004. Efficient algorithms for clause-learning SAT solvers. M.S. dissertation, School of Computing Science, Simon Fraser University.
• 45: Alexandeer Schrijver, Theory of linear and integer programming, John Wiley & Sons, Inc., New York, NY, 1986
• 46: Sanjit A. Seshia , Shuvendu K. Lahiri , Randal E. Bryant, A hybrid SAT-based decision procedure for separation logic with uninterpreted functions, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775945]
• 47: Sanjit A. Seshia , Randal E. Bryant, Adaptive eager boolean encoding for arithmetic reasoning in verification, Carnegie Mellon University, Pittsburgh, PA, 2005
• 48: Sanjit A. Seshia , Randal E. Bryant, Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), p.100-109, July 13-17, 2004
• 49: Ofer Strichman, On Solving Presburger and Linear Arithmetic with SAT, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.160-170, November 06-08, 2002
• 50: Ofer Strichman , Sanjit A. Seshia , Randal E. Bryant, Deciding Separation Formulas with SAT, Proceedings of the 14th International Conference on Computer Aided Verification, p.209-222, July 27-31, 2002
• 51: Stump, A., and Tan, L.-Y. 2005. The algebra of equality proofs. In Proceedings of the 16th International Conference on Term Rewriting and Applications, RTA'05 (Nara, Japan). J. Giesl, Ed. Lecture Notes in Computer Science, vol. 3467. Springer-Verlag, New York, 469--483.
• 52: Talupur, M., Sinha, N., Strichman, O., and Pnueli, A. 2004. Range allocation for separation logic. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV 2004). (Boston, MA July 13--17). Lecture Notes in Computer Science, Springer-Verlag, New York, 148--161.
• 53: Cesare Tinelli, A DPLL-Based Calculus for Ground Satisfiability Modulo Theories, Proceedings of the European Conference on Logics in Artificial Intelligence, p.308-319, September 23-26, 2002
• 54: Tinelli, C., and Ranise, S. 2005. SMT-LIB: The Satisfiability Modulo Theories Library. http://goedel.cs.uiowa.edu/smtlib/.
• 55: Hantao Zhang, SATO: An Efficient Propositional Prover, Proceedings of the 14th International Conference on Automated Deduction, p.272-275, July 13-17, 1997
• 56: Lintao Zhang , Conor F. Madigan , Matthew H. Moskewicz , Sharad Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 57: Lintao Zhang , Sharad Malik, Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications, Proceedings of the conference on Design, Automation and Test in Europe, p.10880, March 03-07, 2003

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Deduction (e.g., natural, rule-based)

General Terms:
Theory, Verification

Keywords:
SAT solvers, Satisfiability Modulo Theories