Hostname: page-component-cd9895bd7-dzt6s Total loading time: 0 Render date: 2024-12-18T20:16:50.133Z Has data issue: false hasContentIssue false
  • English
  • Français

Constraint solving for finite model finding in SMT solvers*

Published online by Cambridge University Press:  28 June 2017

ANDREW REYNOLDS ,
CESARE TINELLI  and
CLARK BARRETT
ANDREW REYNOLDS
Affiliation:
Department of Computer Science, The University of Iowa, Iowa City, Iowa, USA (e-mail: [email protected], [email protected])
CESARE TINELLI
Affiliation:
Department of Computer Science, The University of Iowa, Iowa City, Iowa, USA (e-mail: [email protected], [email protected])
CLARK BARRETT
Affiliation:
Department of Computer Science, Stanford University, Stanford, California, USA (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

Satisfiability modulo theories (SMT) solvers have been used successfully as reasoning engines for automated verification and other applications based on automated reasoning. Current techniques for dealing with quantified formulas in SMT are generally incomplete, forcing SMT solvers to report “unknown” when they fail to prove the unsatisfiability of a formula with quantifiers. This inability to return counter models limits their usefulness in applications that produce queries involving quantified formulas. In this paper, we reduce these limitations by integrating finite model finding techniques based on constraint solving into the architecture used by modern SMT solvers. This approach is made possible by a novel solver for cardinality constraints, as well as techniques for on-demand instantiation of quantified formulas. Experiments show that our approach is competitive with the state of the art in SMT, and orthogonal to approaches in automated theorem proving.

Keywords

Satisfiability modulo theoriesfinite model finding
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 17 , Issue 4 , July 2017 , pp. 516 - 558
Copyright
Copyright © Cambridge University Press 2017 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

*

The work of the first two authors was partially funded by a grant from Intel Corporation.

References

Baader, F. and Nipkow, T. 1998. Term Rewriting and All That. Cambridge University Press.Google Scholar
Barrett, C., Conway, C., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A. and Tinelli, C. 2011. CVC4. In Proc. of CAV'11, Lecture Notes in Computer Science, vol. 6806. Springer, 171–177.Google Scholar
Barrett, C., Nieuwenhuis, R., Oliveras, A. and Tinelli, C. 2006. Splitting on demand in SAT modulo theories. In Proc. of LPAR'06, Lecture Notes in Computer Science, vol. 4246. Springer, 512–526.Google Scholar
Barrett, C. and Tinelli, C. 2007. CVC3. In Proc. of the 19th International Conference on Computer Aided Verification (CAV '07), Damm, W. and Hermanns, H., Eds. Lecture Notes in Computer Science, vol. 4590. Springer-Verlag, Berlin, Germany, 298–302.Google Scholar
Baumgartner, P., Bax, J. and Waldmann, U. 2014. Finite quantification in hierarchic theorem proving. In Proc. of Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, pp. 152–167.Google Scholar
Baumgartner, P., Fuchs, A., de Nivelle, H. and Tinelli, C. 2009. Computing finite models by reduction to function-free clause logic. Journal of Applied Logic 7 (1), 58–74.CrossRefGoogle Scholar
Blanchette, J. C., Böhme, S. and Paulson, L. C. 2011. Extending Sledgehammer with SMT solvers. In Automated Deduction, vol. 6803, Børner, N. and Sofronie-Stokkermans, V., Eds. Lecture Notes in Computer Science, Springer, 116–130.Google Scholar
Blanchette, J. C. and Nipkow, T. 2010. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In ITP 2010, Kaufmann, M. and Paulson, L. C., Eds. Lecture Notes in Computer Science, vol. 6172. Springer, 131–146.Google Scholar
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A. and Sebastiani, R. 2009. Delayed theory combination versus Nelson-Oppen for satisfiability modulo theories: A comparative analysis. AMAI 55 (1–2), 63–99.Google Scholar
Claessen, K. and Sörensson, N. 2003. New techniques that improve MACE-style finite model building. In CADE-19 Workshop: Model Computation – Principles, Algorithms, Applications, 11–27.Google Scholar
de Moura, L. and Bjørner, N. 2007. Efficient E-matching for SMT solvers. In Proc. of Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Lecture Notes in Computer Science, vol. 4603. Springer, Bremen, Germany, 183–198.Google Scholar
De Moura, L. and Bjørner, N. 2008. Z3: An efficient SMT solver. In Proc. of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'08/ETAPS'08, Springer-Verlag, Berlin, Heidelberg, 337–340.Google Scholar
Déharbe, D., Fontaine, P., Merz, S. and Paleo, B. W. 2011. Exploiting symmetry in SMT problems. In Proc. of CADE-23, Lecture Notes in Computer Science, vol. 6803. Springer, 222–236.Google Scholar
Detlefs, D., Nelson, G. and Saxe, J. B. 2003. Simplify: A theorem prover for program checking. Journal of ACM 52 (3), 365–473.CrossRefGoogle Scholar
Dutertre, B. and De Moura, L. 2006. The Yices SMT solver. Version 2.2. Tool paper at http://yices.csl.sri.com/tool-paper.pdf Google Scholar
Garey, M. R., Johnson, D. S. and Stockmeyer, L. 1974. Some simplified np-complete problems. In Proc. of the 6th Annual ACM Symposium on Theory of Computing, STOC '74, ACM, New York, NY, USA, 47–63.Google Scholar
Ge, Y., Barrett, C. and Tinelli, C. 2009. Solving quantified verification conditions using satisfiability modulo theories. Annals of Mathematics and Artificial Intelligence 55 (1–2), 101–122.Google Scholar
Ge, Y. and de Moura, L. 2009. Complete instantiation for quantified formulas in satisfiability modulo theories. In Proc. of CAV'09, Lecture Notes in Computer Science, vol. 5643. Springer, 306–320.Google Scholar
Goel, A., Krstić, S., Leslie, R. and Tuttle, M. 2012. SMT-based system verification with DVF. In Proc. of SMT'12.Google Scholar
Ihlemann, C., Jacobs, S. and Sofronie-Stokkermans, V. 2008. On local reasoning in verification. In TACAS 2008, Ramakrishnan, C. R. and Rehof, J., Eds. Springer, Berlin Heidelberg, 265–281.Google Scholar
Jovanovic, D. and Barrett, C. 2013. Being careful about theory combination. Formal Methods in System Design 42 (1), 67–90.CrossRefGoogle Scholar
Korovin, K. 2008. iProver – an instantiation-based theorem prover for first-order logic. In Proc. of IJCAR'08, Lecture Notes in Computer Science, vol. 5195. Springer, 292–298.Google Scholar
Kovács, L. and Voronkov, A. 2013. First-order theorem proving and vampire. In Proc. of Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, 1–35.Google Scholar
Krstić, S. and Goel, A. 2007. Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In Proc. of FroCoS'07, Lecture Notes in Computer Science, vol. 4720. Springer, 1–27.Google Scholar
McCune, W. 1994. A Davis–Putnam Program and its Application to Finite First-Order Model Search: Quasigroup Existence Problems. Technical Report, Argonne National Laboratory.Google Scholar
Nieuwenhuis, R., Oliveras, A. and Tinelli, C. 2006. 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.Google Scholar
Paulson, L. C. and Wenzel, M. 2002. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer.Google Scholar
Reger, G., Suda, M. and Voronkov, A. 2016. Finding finite models in multi-sorted first-order logic. In Proc. of Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, 323–341.Google Scholar
Reynolds, A. J. 2013. Finite Model Finding in Satisfiability Modulo Theories. PhD Thesis, The University of Iowa.Google Scholar
Reynolds, A., Tinelli, C., Goel, A. and Krstić, S. 2013. Finite model finding in SMT. In Computer Aided Verification, vol. 8044, Sharygina, N. and Veith, H., Eds. Lecture Notes in Computer Science, Springer, Berlin Heidelberg, 640–655.Google Scholar
Reynolds, A., Tinelli, C., Goel, A., Krstić, S., Deters, M. and Barrett, C. 2013. Quantifier instantiation techniques for finite model finding in SMT. In Automated Deduction - CADE-24, Bonacina, M. P. Ed. Lecture Notes in Computer Science, vol. 7898. Springer, Berlin Heidelberg, 377–391.Google Scholar
Reynolds, A., Tinelli, C. and de Moura, L. M. 2014. Finding conflicting instances of quantified formulas in SMT. In FMCAD, IEEE, 195–202.Google Scholar
Schulz, S. 2002. E–a brainiac theorem prover. Ai Communications 15 (2, 3), 111–126.Google Scholar
Sutcliffe, G. 2009. The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0. Journal of Automated Reasoning 43 (4), 337–362.CrossRefGoogle Scholar
Tinelli, C. and Harandi, M. T. 1996. A new correctness proof of the Nelson–Oppen combination procedure. In Proc. of FroCoS'96, Applied Logic, Kluwer, Academic Publishers, 103–120.Google Scholar
Torlak, E. and Jackson, D. 2007. Kodkod: A relational model finder. In Proc. of TACAS'07, Lecture Notes in Computer Science, vol. 4424. Springer, 632–647.Google Scholar
Tuttle, M. R. and Goel, A. 2012. Protocol proof checking simplified with SMT. In Proc. of NCA'12, IEEE Computer Society, 195–202.Google Scholar
Zhang, J. and Zhang, H. 1995. SEM: A system for enumerating models. In Proc. of IJCAI'95, 298–303.Google Scholar