Leveraging Linear and Mixed Integer Programming for SMT

by Tim King, Clark Barrett, Cesare Tinelli
Abstract:
SMT solvers combine SAT reasoning with specialized theory solvers to either find a feasible solution to a set of constraints or prove that no such solution exists. Linear programming (LP) solvers come from the tradition of optimization, and are designed to find feasible solutions that are optimal with respect to some optimization function. Typical LP solvers are designed to solve large systems quickly using floating point arithmetic. Because floating point arithmetic is inexact, rounding errors can lead to incorrect results, making inexact solvers inappropriate for direct use in theorem proving. Previous efforts to leverage such solvers in the context of SMT have concluded that in addition to being potentially unsound, such solvers are too heavyweight to compete in the context of SMT. In this paper, we describe a technique for integrating LP solvers that dramatically improves the performance of SMT solvers without compromising correctness. These techniques have been implemented using the SMT solver CVC4 and the LP solver GLPK. Experiments show that this implementation outperforms other state-of-the-art SMT solvers on the QF_LRA SMT-LIB benchmarks and is competitive on the QF_LIA benchmarks.
Reference:
Leveraging Linear and Mixed Integer Programming for SMT (Tim King, Clark Barrett, Cesare Tinelli), In Proceedings of the 14th International Conference on Formal Methods In Computer-Aided Design (FMCAD ’14), FMCAD Inc., 2014. (Lausanne, Switzerland)
Bibtex Entry:
@inproceedings{KBT14,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/KBT14.pdf",
  author    = "Tim King and Clark Barrett and Cesare Tinelli",
  title     = "Leveraging Linear and Mixed Integer Programming for {SMT}",
  booktitle = "Proceedings of the 14th International Conference on Formal Methods In Computer-Aided Design (FMCAD '14)",
  publisher = "FMCAD Inc.",
  pages     = "139--146",
  month     = oct,
  year      = 2014,
  note      = "Lausanne, Switzerland",
  category  = "Conference Publications",
  abstract  = "SMT solvers combine SAT reasoning with specialized theory
                  solvers to either find a feasible solution to a set of
                  constraints or prove that no such solution exists.  Linear
                  programming (LP) solvers come from the tradition of
                  optimization, and are designed to find feasible solutions
                  that are optimal with respect to some optimization function.
                  Typical LP solvers are designed to solve large systems
                  quickly using floating point arithmetic.  Because floating
                  point arithmetic is inexact, rounding errors can lead to
                  incorrect results, making inexact solvers inappropriate for
                  direct use in theorem proving.  Previous efforts to leverage
                  such solvers in the context of SMT have concluded that in
                  addition to being potentially unsound, such solvers are too
                  heavyweight to compete in the context of SMT.  In this paper,
                  we describe a technique for integrating LP solvers that
                  dramatically improves the performance of SMT solvers without
                  compromising correctness.  These techniques have been
                  implemented using the SMT solver CVC4 and the LP solver GLPK.
                  Experiments show that this implementation outperforms other
                  state-of-the-art SMT solvers on the QF_LRA SMT-LIB
                  benchmarks and is competitive on the QF_LIA benchmarks."
}

Fork me on GitHub