Solving quantified linear arithmetic by counterexample-guided instantiation

by Andrew Reynolds, Tim King, Viktor Kuncak
Abstract:
This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedures for linear real arithmetic (LRA) and linear integer arithmetic (LIA) formulas with one quantifier alternation. We discuss extensions of these techniques for handling mixed real and integer arithmetic, and to formulas with arbitrary quantifier alternations. For the latter, we use a novel strategy that handles quantified formulas that are not in prenex normal form, which has advantages with respect to existing approaches. All of these techniques can be integrated within the solving architecture used by typical SMT solvers. Experimental results on standardized benchmarks from model checking, static analysis, and synthesis show that our implementation in the SMT solver CVC4 outperforms existing tools for quantified linear arithmetic.
Reference:
Solving quantified linear arithmetic by counterexample-guided instantiation (Andrew Reynolds, Tim King, Viktor Kuncak), In Formal Methods in System Design, Springer US, 2017.
Bibtex Entry:
@article{reynolds2017solving,
  title={Solving quantified linear arithmetic by counterexample-guided instantiation},
  author={Reynolds, Andrew and King, Tim and Kuncak, Viktor},
  journal={Formal Methods in System Design},
  pages={1--33},
  year={2017},
  publisher={Springer US},
  url       = {http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf},
  doi       = {10.1007/s10703-017-0290-y},
  abstract  = "This paper presents a framework to derive instantiation-based decision procedures
for satisfiability of quantified formulas in first-order theories, including its correctness,
implementation, and evaluation. Using this framework we derive decision procedures for
linear real arithmetic (LRA) and linear integer arithmetic (LIA) formulas with one quantifier
alternation. We discuss extensions of these techniques for handling mixed real and
integer arithmetic, and to formulas with arbitrary quantifier alternations. For the latter, we
use a novel strategy that handles quantified formulas that are not in prenex normal form,
which has advantages with respect to existing approaches. All of these techniques can be
integrated within the solving architecture used by typical SMT solvers. Experimental results
on standardized benchmarks from model checking, static analysis, and synthesis show that
our implementation in the SMT solver CVC4 outperforms existing tools for quantified linear
arithmetic."
}

Fork me on GitHub