Book chapter
Quantifier Instantiation Techniques for Finite Model Finding in SMT
Automated Deduction – CADE-24, pp.377-391
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2013
DOI: 10.1007/978-3-642-38574-2_26
Abstract
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.
Details
- Title: Subtitle
- Quantifier Instantiation Techniques for Finite Model Finding in SMT
- Creators
- Andrew Reynolds - University of IowaCesare Tinelli - University of IowaAmit Goel - IntelSava Krstić - IntelMorgan Deters - New York UniversityClark Barrett - New York University
- Resource Type
- Book chapter
- Publication Details
- Automated Deduction – CADE-24, pp.377-391
- Publisher
- Springer Berlin Heidelberg; Berlin, Heidelberg
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-642-38574-2_26
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 2013
- Academic Unit
- Computer Science
- Record Identifier
- 9984259412202771
Metrics
13 Record Views