Abstract
SMT solvers have traditionally been based on the DPLL(T) algorithm, where the driving force behind the procedure is a DPLL search over truth valuations. This traditional framework allows for a degree of modularity in the treatment of theory solvers. Over time, theory solvers have become more and more closely integrated into the DPLL process, and consequently less and less modular. In this paper, we present a DPLL-like algorithm for SMT solving in which the search takes place over the natural domain of the variables in the problem. As a case study, we analyze its application to continuous domain linear arithmetic, present implementation techniques and some experimentation with difference logic. Results indicate the method can sometimes outperform leading SMT solvers but that the method is not yet robust.
This is a preview of subscription content, log in via an institution to check access.
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
Bjørner, N., Dutertre, B., de Moura, L.: Accelerating Lemma Learning Using Joins – DPLL(⊔). In: Int. Conf. Logic for Programming, Artif. Intell. and Reasoning, LPAR (2008)
Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, ch. 16. Elsevier, Amsterdam (2006)
Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2008), http://www.SMT-LIB.org
Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories February 2009. Frontiers in Artificial Intelligence and Applications, ch. 26, vol. 185, pp. 825–885. IOS Press, Amsterdam (2009)
de Moura, L., Bjørner, N.: Engineering DPLL(T) + Saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 475–490. Springer, Heidelberg (2008)
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)
Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Constraint Programming (2009)
McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to Richer Logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 462–476. Springer, Heidelberg (2009)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC’01 (2001)
Marriott, K., Stuckey, P.J., Wallace, M.: Constraint logic programming. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, ch. 12, Elsevier, Amsterdam (2006)
Wang, C., Gupta, A., Gannai, M.K.: Predicate Learning and Selective Theory Deduction. In: Design Automation Conference, DAC (2006)
Zhang, L., Malik, S.: Validating sat solvers using an independent resolution-based checker: Practical implementations and other applications. In: Design, Automation and Test in Europe Conference and Exhibition (DATE’03), p. 10880 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cotton, S. (2010). Natural Domain SMT: A Preliminary Assessment. In: Chatterjee, K., Henzinger, T.A. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2010. Lecture Notes in Computer Science, vol 6246. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15297-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-15297-9_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15296-2
Online ISBN: 978-3-642-15297-9
eBook Packages: Computer ScienceComputer Science (R0)