Simplex with sum of infeasibilities for SMT

Tim King, Clark Barrett, Bruno Dutertre

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

Abstract

The de facto standard for state-of-the-art real and integer linear reasoning within Satisfiability Modulo Theories (SMT) solvers is the Simplex for DPLL(T) algorithm given by Dutertre and de Moura. This algorithm works by performing a sequence of local optimization operations. While the algorithm is generally efficient in practice, its local pivoting heuristics lead to slow convergence on some problems. More traditional Simplex algorithms minimize a global criterion to determine the feasibility of the input constraints. We present a novel Simplex-based decision procedure for use in SMT that minimizes the sum of infeasibilities of the constraints. Experimental results show that this new algorithm is comparable with or outperforms Simplex for DPLL(T) on a broad set of benchmarks.

Original languageEnglish (US)
Title of host publication2013 Formal Methods in Computer-Aided Design, FMCAD 2013
Pages189-196
Number of pages8
StatePublished - 2013
Event13th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2013 - Portland, OR, United States
Duration: Oct 20 2013Oct 23 2013

Other

Other13th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2013
CountryUnited States
CityPortland, OR
Period10/20/1310/23/13

Fingerprint

Infeasibility
Modulo
Minimise
Input Constraints
Simplex Algorithm
Local Optimization
Pivoting
Decision Procedures
Reasoning
Heuristics
Benchmark
Integer
Experimental Results

ASJC Scopus subject areas

  • Computer Graphics and Computer-Aided Design
  • Logic

Cite this

King, T., Barrett, C., & Dutertre, B. (2013). Simplex with sum of infeasibilities for SMT. In 2013 Formal Methods in Computer-Aided Design, FMCAD 2013 (pp. 189-196). [6679409]

Simplex with sum of infeasibilities for SMT. / King, Tim; Barrett, Clark; Dutertre, Bruno.

2013 Formal Methods in Computer-Aided Design, FMCAD 2013. 2013. p. 189-196 6679409.

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

King, T, Barrett, C & Dutertre, B 2013, Simplex with sum of infeasibilities for SMT. in 2013 Formal Methods in Computer-Aided Design, FMCAD 2013., 6679409, pp. 189-196, 13th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, United States, 10/20/13.
King T, Barrett C, Dutertre B. Simplex with sum of infeasibilities for SMT. In 2013 Formal Methods in Computer-Aided Design, FMCAD 2013. 2013. p. 189-196. 6679409
King, Tim ; Barrett, Clark ; Dutertre, Bruno. / Simplex with sum of infeasibilities for SMT. 2013 Formal Methods in Computer-Aided Design, FMCAD 2013. 2013. pp. 189-196
@inproceedings{81c818d8e82d4d859d2e82cf4a6366f8,
title = "Simplex with sum of infeasibilities for SMT",
abstract = "The de facto standard for state-of-the-art real and integer linear reasoning within Satisfiability Modulo Theories (SMT) solvers is the Simplex for DPLL(T) algorithm given by Dutertre and de Moura. This algorithm works by performing a sequence of local optimization operations. While the algorithm is generally efficient in practice, its local pivoting heuristics lead to slow convergence on some problems. More traditional Simplex algorithms minimize a global criterion to determine the feasibility of the input constraints. We present a novel Simplex-based decision procedure for use in SMT that minimizes the sum of infeasibilities of the constraints. Experimental results show that this new algorithm is comparable with or outperforms Simplex for DPLL(T) on a broad set of benchmarks.",
author = "Tim King and Clark Barrett and Bruno Dutertre",
year = "2013",
language = "English (US)",
isbn = "9780983567837",
pages = "189--196",
booktitle = "2013 Formal Methods in Computer-Aided Design, FMCAD 2013",

}

TY - GEN

T1 - Simplex with sum of infeasibilities for SMT

AU - King, Tim

AU - Barrett, Clark

AU - Dutertre, Bruno

PY - 2013

Y1 - 2013

N2 - The de facto standard for state-of-the-art real and integer linear reasoning within Satisfiability Modulo Theories (SMT) solvers is the Simplex for DPLL(T) algorithm given by Dutertre and de Moura. This algorithm works by performing a sequence of local optimization operations. While the algorithm is generally efficient in practice, its local pivoting heuristics lead to slow convergence on some problems. More traditional Simplex algorithms minimize a global criterion to determine the feasibility of the input constraints. We present a novel Simplex-based decision procedure for use in SMT that minimizes the sum of infeasibilities of the constraints. Experimental results show that this new algorithm is comparable with or outperforms Simplex for DPLL(T) on a broad set of benchmarks.

AB - The de facto standard for state-of-the-art real and integer linear reasoning within Satisfiability Modulo Theories (SMT) solvers is the Simplex for DPLL(T) algorithm given by Dutertre and de Moura. This algorithm works by performing a sequence of local optimization operations. While the algorithm is generally efficient in practice, its local pivoting heuristics lead to slow convergence on some problems. More traditional Simplex algorithms minimize a global criterion to determine the feasibility of the input constraints. We present a novel Simplex-based decision procedure for use in SMT that minimizes the sum of infeasibilities of the constraints. Experimental results show that this new algorithm is comparable with or outperforms Simplex for DPLL(T) on a broad set of benchmarks.

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

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

M3 - Conference contribution

SN - 9780983567837

SP - 189

EP - 196

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

ER -