Abstract
We describe and discuss DPLL(T ), a parametric calculus for proving the satisfiability of ground formulas in a logical theory T. The calculus tightly integrates a decision procedure for the satisfiability in T of sets of literals into a sequent calculus based on the well-known method by Davis, Putman, Logemann and Loveland for proving the satisfiability of propositional formulas. For being based on the DPLL method, DPLL(T ) can incorporate a number of very effective search heuristics developed by the SAT community for that method. Hence, it can be used as the formal basis for novel and efficient implementations of satisfiability checkers for theories with decidable ground consequences.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alessandro Armando, Claudio Castellini, and Enrico Giunchiglia. SAT-based procedures for temporal reasoning. In S. Biundo and M. Fox, editors, Proceedings of the 5th European Conference on Planning (Durham, UK), volume 1809of Lecture Notes in Computer Science, pages 97–1080. Springer, 2000.
Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, and Roberto Sebastiani. A SAT-based approach for solving formulas over boolean and linear mathematical propositions. In Reiner Hähnle, editor, Proceedings of the 18th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence. Springer, 2002. (to appear).
Clark W. Barrett, David L. Dill, and Jeremy R. Levitt. Validity checking for combinations of theories with equality. In M. K. Srivas and A. Camilleri, editors, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (Palo Alto, CA), volume 1166 of Lecture Notes in Computer Science, pages 187–201. Springer, 1996.
Clark W. Barrett, David L. Dill, and Aaron Stump. Checking satisfiability of first-order formulas by incremental translation to SAT. In J. C. Godskesen, editor, Proceedings of the International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, 2002. (to appear).
Nikolaj S. Bjørner, Mark. E. Stickel, and Tomás E. Uribe. A practical integration of first-order reasoning and decision procedures. In W. McCune, editor, Proceedings of the 14th International Conference on Automated Deduction, CADE-14 (Townsville, Australia), volume 1249 of Lecture Notes in Artificial Intelligence, pages 101–115, 1997.
Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394–397, July 1962.
Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201–215, July 1960.
Leonardo de Moura and Harald Rueß. Lemmas on demand for satisfiability solvers. Presented at the Fifth International Symposium on the Theory and Applications of Satisfiability Testing (SAT’02), Cincinnati, USA, May 2002.
Jon W. Freeman. Improvements to Propositional Satisfiability Search Algorithms. PhD thesis, Departement of computer and Information science, University of Pennsylvania, Philadelphia, 1995.
Wilfrid Hodges. Logical features of Horn clauses. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1, pages 449–503. Oxford University Press, 1993.
Joxan Jaffar and Michael Maher. Constraint Logic Programming: A Survey. Journal of Logic Programming, 19/20:503–581, 1994.
Shie-Jue Lee and David A. Plaisted. Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning, 9(1):25–42, August 1992.
Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Cha.: Engineering an Efficient SAT Solver. In Proceedings of the 38th Design Automation Conference (DAC’01), June 2001.
Greg Nelson and Dave Detlefs. The Simplify user’s manual. Compaq Systems Research Center. (http://research.compaq.com/SRC/esc/Simplify.html).
Cesare Tinelli. A DPLL-based calculus for ground satisfiability modulo theories. Technical report, Department of Computer Science, University of Iowa, 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tinelli, C. (2002). A DPLL-Based Calculus for Ground Satisfiability Modulo Theories. In: Flesca, S., Greco, S., Ianni, G., Leone, N. (eds) Logics in Artificial Intelligence. JELIA 2002. Lecture Notes in Computer Science(), vol 2424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45757-7_26
Download citation
DOI: https://doi.org/10.1007/3-540-45757-7_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44190-8
Online ISBN: 978-3-540-45757-2
eBook Packages: Springer Book Archive