Constraint solving for finite model finding in SMT solvers

by Andrew Reynolds, Cesare Tinelli, Clark Barrett
Abstract:
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.
Reference:
Constraint solving for finite model finding in SMT solvers (Andrew Reynolds, Cesare Tinelli, Clark Barrett), In TPLP, volume 17, 2017.
Bibtex Entry:
@article{DBLP:journals/tplp/ReynoldsTB17,
  author    = {Andrew Reynolds and
               Cesare Tinelli and
               Clark Barrett},
  title     = {Constraint solving for finite model finding in {SMT} solvers},
  journal   = {{TPLP}},
  volume    = {17},
  number    = {4},
  pages     = {516--558},
  year      = {2017},
  url       = {https://doi.org/10.1017/S1471068417000175},
  doi       = {10.1017/S1471068417000175},
  timestamp = {Wed, 30 Aug 2017 15:38:05 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tplp/ReynoldsTB17},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  abstract  = "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."
}

Fork me on GitHub