Quantifier instantiation techniques for finite model finding in SMT

Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstić, Morgan Deters, Clark Barrett

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationCADE 2013 - 24th International Conference on Automated Deduction, Proceedings
Number of pages15
StatePublished - 2013
Event24th International Conference on Automated Deduction, CADE 2013 - Lake Placid, NY, United States
Duration: Jun 9 2013Jun 14 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7898 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other24th International Conference on Automated Deduction, CADE 2013
Country/TerritoryUnited States
CityLake Placid, NY

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Quantifier instantiation techniques for finite model finding in SMT'. Together they form a unique fingerprint.

Cite this