# Leveraging Linear and Mixed Integer Programming for SMT

“Leveraging Linear and Mixed Integer Programming for SMT”
by Tim King, Clark Barrett, and Cesare Tinelli.
In *Proceedings of the **14^th* International Conference on Formal
Methods In Computer-Aided Design (FMCAD '14), Oct. 2014. Lausanne,
Switzerland, to appear.

## 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.

**BibTeX entry:**

@inproceedings{KBT14,
author = {Tim King and Clark Barrett and Cesare Tinelli},
title = {Leveraging Linear and Mixed Integer Programming for SMT},
booktitle = {Proceedings of the {\it 14^{th}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '14)},
publisher = {FMCAD Inc.},
month = oct,
year = {2014},
note = {Lausanne, Switzerland, to appear}
}

(This webpage was created with
bibtex2web.)