Conference proceeding
Leveraging linear and mixed integer programming for SMT
2014 Formal Methods in Computer-Aided Design (FMCAD), pp.139-146
10/2014
DOI: 10.1109/FMCAD.2014.6987606
Abstract
SMT solvers combine SAT reasoning with specialized theory solvers either to find a feasible solution to a set of constraints or to 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 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.
Details
- Title: Subtitle
- Leveraging linear and mixed integer programming for SMT
- Creators
- Tim King - New York UniversityClark Barrett - New York UniversityCesare Tinelli - University of Iowa
- Resource Type
- Conference proceeding
- Publication Details
- 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.139-146
- DOI
- 10.1109/FMCAD.2014.6987606
- Publisher
- FMCAD and the authors
- Language
- English
- Date published
- 10/2014
- Academic Unit
- Computer Science
- Record Identifier
- 9984259412502771
Metrics
20 Record Views