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
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages139-146
Number of pages8
ISBN (Print)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

Other

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

Fingerprint

Surface mount technology
Integer programming
Linear programming
Digital arithmetic
Theorem proving
Computer systems

ASJC Scopus subject areas

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

Cite this

King, T., Barrett, C., & Tinelli, C. (2014). Leveraging linear and mixed integer programming for SMT. In 2014 Formal Methods in Computer-Aided Design, FMCAD 2014 (pp. 139-146). [6987606] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/FMCAD.2014.6987606

Leveraging linear and mixed integer programming for SMT. / King, Tim; Barrett, Clark; Tinelli, Cesare.

2014 Formal Methods in Computer-Aided Design, FMCAD 2014. Institute of Electrical and Electronics Engineers Inc., 2014. p. 139-146 6987606.

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

King, T, Barrett, C & Tinelli, C 2014, Leveraging linear and mixed integer programming for SMT. in 2014 Formal Methods in Computer-Aided Design, FMCAD 2014., 6987606, Institute of Electrical and Electronics Engineers Inc., pp. 139-146, 14th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 10/21/14. https://doi.org/10.1109/FMCAD.2014.6987606
King T, Barrett C, Tinelli C. Leveraging linear and mixed integer programming for SMT. In 2014 Formal Methods in Computer-Aided Design, FMCAD 2014. Institute of Electrical and Electronics Engineers Inc. 2014. p. 139-146. 6987606 https://doi.org/10.1109/FMCAD.2014.6987606
King, Tim ; Barrett, Clark ; Tinelli, Cesare. / Leveraging linear and mixed integer programming for SMT. 2014 Formal Methods in Computer-Aided Design, FMCAD 2014. Institute of Electrical and Electronics Engineers Inc., 2014. pp. 139-146
@inproceedings{c325bf14e25e4d0894d7dfaf36751ed5,
title = "Leveraging linear and mixed integer programming for SMT",
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.",
author = "Tim King and Clark Barrett and Cesare Tinelli",
year = "2014",
month = "12",
day = "16",
doi = "10.1109/FMCAD.2014.6987606",
language = "English (US)",
isbn = "9780983567844",
pages = "139--146",
booktitle = "2014 Formal Methods in Computer-Aided Design, FMCAD 2014",
publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

TY - GEN

T1 - Leveraging linear and mixed integer programming for SMT

AU - King, Tim

AU - Barrett, Clark

AU - Tinelli, Cesare

PY - 2014/12/16

Y1 - 2014/12/16

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

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

UR - http://www.scopus.com/inward/record.url?scp=84921328798&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84921328798&partnerID=8YFLogxK

U2 - 10.1109/FMCAD.2014.6987606

DO - 10.1109/FMCAD.2014.6987606

M3 - Conference contribution

SN - 9780983567844

SP - 139

EP - 146

BT - 2014 Formal Methods in Computer-Aided Design, FMCAD 2014

PB - Institute of Electrical and Electronics Engineers Inc.

ER -