A Fast Linear-Arithmetic Solver for DPLL(T)

---

In: Proceedings of Computer-Aided Verification, CAV '2006.

Authors

Bruno Dutertre, and Leonardo de Moura.

Abstract

We present a new Simplex-based linear arithmetic solver that can be integrated efficiently in the DPLL(T) framework. The new solver improves over existing approaches by enabling fast backtracking, supporting a priori simplification to reduce the problem size, and providing an efficient form of theory propagation. We also present a new and simple approach for solving strict inequalities. Experimental results show substantial performance improvements over existing tools that use other Simplex-based solvers in DPLL(T) decision procedures. The new solver is even competitive with state-of-the-art tools specialized for the difference logic fragment.

Download: PDF

BibTeX Entry

@inproceedings{DdM:06,
  TITLE = {{A Fast Linear-Arithmetic Solver for DPLL(T)}},
  AUTHOR = {Bruno Dutertre and Leonardo de Moura},
  BOOKTITLE = "Proceedings of the 18th Computer-Aided Verification conference",
  SERIES="LNCS",
  PAGES = {81--94}, 
  EDITORS={T. Ball and R. B. Jones},
  VOLUME=4144,
  PUBLISHER = {Springer-Verlag},
  YEAR = 2006,
}

---

Leonardo de Moura: demoura@csl.sri.com