Leveraging linear and mixed integer programming for SMT

Tim King, Clark Barrett, Cesare Tinelli

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publication2014 Formal Methods in Computer-Aided Design, FMCAD 2014
EditorsViktor Kuncak, Koen Claessen
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages139-146
Number of pages8
ISBN (Electronic)9780983567844
DOIs
StatePublished - Dec 16 2014
Event14th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2014 - Lausanne, Switzerland
Duration: Oct 21 2014Oct 24 2014

Publication series

Name2014 Formal Methods in Computer-Aided Design, FMCAD 2014

Other

Other14th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2014
CountrySwitzerland
CityLausanne
Period10/21/1410/24/14

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Leveraging linear and mixed integer programming for SMT'. Together they form a unique fingerprint.

Cite this