Simplex with Sum of Infeasibilities for SMT

by Timothy King, Clark Barrett, Bruno Dutertre
Abstract:
The de facto standard for state-of-the-art real and integer linear reasoning within Satisfiability Modulo Theories (SMT) solvers is the Simplex for DPLL(T) algorithm given by Dutertre and de Moura. This algorithm works by performing a sequence of local optimization operations. While the algorithm is generally efficient in practice, its local pivoting heuristics lead to slow convergence on some problems. More traditional Simplex algorithms minimize a global criterion to determine the feasibility of the input constraints. We present a novel Simplexbased decision procedure for use in SMT that minimizes the sum of infeasibilities of the constraints. Experimental results show that this new algorithm is comparable with or outperforms Simplex for DPLL(T) on a broad set of benchmarks.
Reference:
Simplex with Sum of Infeasibilities for SMT (Timothy King, Clark Barrett, Bruno Dutertre), In Proceedings of the 13th International Conference on Formal Methods In Computer-Aided Design (FMCAD ’13), FMCAD Inc., 2013. (Portland, Oregon)
Bibtex Entry:
@inproceedings{KBD13,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/KBD13.pdf",
  author    = "Timothy King and Clark Barrett and Bruno Dutertre",
  title     = "Simplex with Sum of Infeasibilities for {SMT}",
  booktitle = "Proceedings of the 13th International Conference on Formal Methods In Computer-Aided Design (FMCAD '13)",
  publisher = "FMCAD Inc.",
  pages     = "189--196",
  month     = oct,
  year      = 2013,
  note      = "Portland, Oregon",
  category  = "Conference Publications",
  abstract  = "The de facto standard for state-of-the-art real and
integer linear reasoning within Satisfiability Modulo Theories
(SMT) solvers is the Simplex for DPLL(T) algorithm given by
Dutertre and de Moura. This algorithm works by performing a
sequence of local optimization operations. While the algorithm
is generally efficient in practice, its local pivoting heuristics
lead to slow convergence on some problems. More traditional
Simplex algorithms minimize a global criterion to determine the
feasibility of the input constraints. We present a novel Simplexbased
decision procedure for use in SMT that minimizes the sum
of infeasibilities of the constraints. Experimental results show that
this new algorithm is comparable with or outperforms Simplex
for DPLL(T) on a broad set of benchmarks."
}

Fork me on GitHub