TY - GEN
T1 - Quantifier instantiation techniques for finite model finding in SMT
AU - Reynolds, Andrew
AU - Tinelli, Cesare
AU - Goel, Amit
AU - Krstić, Sava
AU - Deters, Morgan
AU - Barrett, Clark
PY - 2013
Y1 - 2013
N2 - SMT-based applications increasingly rely on SMT solvers being able to deal with quantified formulas. Current work shows that for formulas with quantifiers over uninterpreted sorts counter-models can be obtained by integrating a finite model finding capability into the architecture of a modern SMT solver. We examine various strategies for on-demand quantifier instantiation in this setting. Here, completeness can be achieved by considering all ground instances over the finite domain of each quantifier. However, exhaustive instantiation quickly becomes unfeasible with larger domain sizes. We propose instantiation strategies to identify and consider only a selection of ground instances that suffices to determine the satisfiability of the input formula. We also examine heuristic quantifier instantiation techniques such as E-matching for the purpose of accelerating the search. We give experimental evidence that our approach is practical for use in industrial applications and is competitive with other approaches.
AB - SMT-based applications increasingly rely on SMT solvers being able to deal with quantified formulas. Current work shows that for formulas with quantifiers over uninterpreted sorts counter-models can be obtained by integrating a finite model finding capability into the architecture of a modern SMT solver. We examine various strategies for on-demand quantifier instantiation in this setting. Here, completeness can be achieved by considering all ground instances over the finite domain of each quantifier. However, exhaustive instantiation quickly becomes unfeasible with larger domain sizes. We propose instantiation strategies to identify and consider only a selection of ground instances that suffices to determine the satisfiability of the input formula. We also examine heuristic quantifier instantiation techniques such as E-matching for the purpose of accelerating the search. We give experimental evidence that our approach is practical for use in industrial applications and is competitive with other approaches.
UR - http://www.scopus.com/inward/record.url?scp=84879972079&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84879972079&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-38574-2_26
DO - 10.1007/978-3-642-38574-2_26
M3 - Conference contribution
AN - SCOPUS:84879972079
SN - 9783642385735
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 377
EP - 391
BT - CADE 2013 - 24th International Conference on Automated Deduction, Proceedings
T2 - 24th International Conference on Automated Deduction, CADE 2013
Y2 - 9 June 2013 through 14 June 2013
ER -