×

zbMATH — the first resource for mathematics

Constraint solving for finite model finding in SMT solvers. (English) Zbl 1379.68286
Summary: 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.
MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baader, F.; Nipkow, T., Term Rewriting and All That, pp., (1998), Cambridge University Press
[2] Barrett, C.; Conway, C.; Deters, M.; Hadarean, L.; Jovanovic, D.; King, T.; Reynolds, A.; Tinelli, C., pp., (2011)
[3] Barrett, C.; Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., pp., (2006)
[4] Barrett, C.; Tinelli, C.; Damm, W.; Hermanns, H., pp., (2007)
[5] Baumgartner, P.; Bax, J.; Waldmann, U., pp., (2014)
[6] Baumgartner, P.; Fuchs, A.; de Nivelle, H.; Tinelli, C., Computing finite models by reduction to function-free clause logic, Journal of Applied Logic, 7, 58-74, (2009) · Zbl 1171.68040
[7] Blanchette, J. C.; Böhme, S.; Paulson, L. C.; Børner, N.; Sofronie-Stokkermans, V., Automated Deduction, Extending Sledgehammer with SMT solvers, 116-130, (2011), Springer
[8] Blanchette, J. C.; Nipkow, T.; Kaufmann, M.; Paulson, L. C., ITP 2010, Nitpick: A counterexample generator for higher-order logic based on a relational model finder, 131-146, (2010), Springer · Zbl 1291.68326
[9] Bruttomesso, R.; Cimatti, A.; Franzén, A.; Griggio, A.; Sebastiani, R., Delayed theory combination versus Nelson-oppen for satisfiability modulo theories: A comparative analysis, AMAI, 55, 63-99, (2009) · Zbl 1192.68627
[10] Claessen, K.; Sörensson, N., pp., (2003)
[11] de Moura, L.; Bjørner, N., pp., (2007)
[12] De Moura, L.; Bjørner, N., pp., (2008)
[13] Déharbe, D.; Fontaine, P.; Merz, S.; Paleo, B. W., pp., (2011)
[14] Detlefs, D.; Nelson, G.; Saxe, J. B., Simplify: A theorem prover for program checking, Journal of ACM, 52, 365-473, (2003) · Zbl 1323.68462
[15] Dutertre, B.; De Moura, L., pp., (2006)
[16] Garey, M. R.; Johnson, D. S.; Stockmeyer, L., pp., (1974)
[17] Ge, Y.; Barrett, C.; Tinelli, C., Solving quantified verification conditions using satisfiability modulo theories, Annals of Mathematics and Artificial Intelligence 55, 101-122, (2009) · Zbl 1184.68461
[18] Ge, Y.; de Moura, L., pp., (2009)
[19] Goel, A.; Krstić, S.; Leslie, R.; Tuttle, M., pp., (2012)
[20] Ihlemann, C.; Jacobs, S.; Sofronie-Stokkermans, V.; Ramakrishnan, C. R.; Rehof, J., TACAS 2008, On local reasoning in verification, 265-281, (2008), Springer, Berlin Heidelberg · Zbl 1134.68410
[21] Jovanovic, D.; Barrett, C., Being careful about theory combination, Formal Methods in System Design, 42, 67-90, (2013) · Zbl 1284.68518
[22] Korovin, K., pp., (2008)
[23] Kovács, L.; Voronkov, A., pp., (2013)
[24] Krstić, S.; Goel, A., pp., (2007)
[25] McCune, W., pp., (1994)
[26] 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, 937-977, (2006) · Zbl 1326.68164
[27] Paulson, L. C.; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-Order Logic, pp., (2002), Springer · Zbl 0994.68131
[28] Reger, G.; Suda, M.; Voronkov, A., pp., (2016)
[29] Reynolds, A. J., pp., (2013)
[30] Reynolds, A.; Tinelli, C.; Goel, A.; Krstić, S.; Sharygina, N.; Veith, H., Computer Aided Verification, Finite model finding in SMT, 640-655, (2013), Springer, Berlin Heidelberg · Zbl 1268.68032
[31] Reynolds, A.; Tinelli, C.; Goel, A.; Krstić, S.; Deters, M.; Barrett, C.; Bonacina, M. P., Automated Deduction - CADE-24, Quantifier instantiation techniques for finite model finding in SMT, 377-391, (2013), Springer, Berlin Heidelberg · Zbl 1264.68002
[32] Reynolds, A.; Tinelli, C.; de Moura, L. M., Finding conflicting instances of quantified formulas in SMT, FMCAD, 195-202, (2014)
[33] Schulz, S., E-a brainiac theorem prover, Ai Communications, 15, 111-126, (2002) · Zbl 1020.68084
[34] Sutcliffe, G., The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0., Journal of Automated Reasoning, 43, 337-362, (2009) · Zbl 1185.68636
[35] Tinelli, C.; Harandi, M. T., pp., (1996)
[36] Torlak, E.; Jackson, D., pp., (2007)
[37] Tuttle, M. R.; Goel, A., pp., (2012)
[38] Zhang, J.; Zhang, H., pp., (1995)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.