Quantifier Instantiation Techniques for Finite Model Finding in SMT

by Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark Barrett
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.
Reference:
Quantifier Instantiation Techniques for Finite Model Finding in SMT (Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark Barrett), In Proceedings of the 24th International Conference on Automated Deduction (CADE ’13) (Maria Paola Bonacina, ed.), Springer Berlin Heidelberg, volume 7898, 2013. (Lake Placid, NY)
Bibtex Entry:
@inproceedings{RTG+13,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/RTG+13.pdf",
  author    = "Andrew Reynolds and Cesare Tinelli and Amit Goel and Sava Krstic and Morgan Deters and Clark Barrett",
  title     = "Quantifier Instantiation Techniques for Finite Model Finding in {SMT}",
  booktitle = "Proceedings of the 24th International Conference on Automated Deduction (CADE '13)",
  series    = "Lecture Notes in Computer Science",
  volume    = 7898,
  publisher = "Springer Berlin Heidelberg",
  editor    = "Bonacina, Maria Paola",
  pages     = "377-391",
  doi       = "10.1007/978-3-642-38574-2_26",
  isbn      = "978-3-642-38573-5",
  year      = 2013,
  note      = "Lake Placid, NY",
  category  = "Conference Publications",
  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."
}

Fork me on GitHub