Abstract
We offer a transition system representing a high-level but detailed architecture for SMT solvers that combine a propositional SAT engine with solvers for multiple disjoint theories. The system captures succintly and accurately all the major aspects of the solver’s global operation: boolean search with across-the-board backjumping, communication of theory-specific facts and equalities between shared variables, and cooperative conflict analysis. Provably correct and prudently underspecified, our system is a usable ground for high-quality implementations of comprehensive SMT solvers.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
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.
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Barrett, C.: Checking Validity of Quantifier-free Formulas in Combinations of First-Order Theories. PhD thesis, Stanford University (2002)
Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT Modulo Theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, Springer, Heidelberg (2006)
Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, Springer, Heidelberg (2006)
Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Ranise, S., Sebastiani, R.: Efficient theory combination via boolean search. Information and Computation 204(10), 1493–1525
Bryant, R., Lahiri, S., Seshia, S.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, Springer, Heidelberg (2002)
Conchon, S., Krstić, S.: Strategies for combining decision procedures. Theoretical Computer Science 354(2), 187–210 (2006)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Journal of the ACM 52(3), 365–473 (2005)
Dutertre, B., de Moura, L.: The Yices SMT solver. Technical report, SRI International (2006)
Eén, N., Sörensen, N.: An extensible SAT solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, Springer, Heidelberg (2004)
Krstić, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: TSDM 2000. LNCS, vol. 4424, Springer, Heidelberg (2007)
Mitchell, J.C.: Foundations of Programming Languages. MIT Press, Cambridge (1996)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: Conference on Design Automation (DAC), ACM Press, New York (2001)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6), 937–977 (2006)
Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) Frontiers of Combining Systems. LNCS (LNAI), vol. 3717, Springer, Heidelberg (2005)
Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Mason, R.E.A., (ed.) Information Processing: 9th World Computer Congress, pp. 513–523. North-Holland (1983)
Tinelli, C., Harandi, M.: A new correctness proof of the Nelson-Oppen combination procedure. In: Frontiers of Combining Systems (FroCoS), vol. 3 of Applied Logic, pp. 103–120 (1996)
Tinelli, C., Zarba, C.: Combining nonstably infinite theories. Journal of Automated Reasoning 34(3), 209–238 (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Krstić, S., Goel, A. (2007). Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL. In: Konev, B., Wolter, F. (eds) Frontiers of Combining Systems. FroCoS 2007. Lecture Notes in Computer Science(), vol 4720. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74621-8_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-74621-8_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74620-1
Online ISBN: 978-3-540-74621-8
eBook Packages: Computer ScienceComputer Science (R0)