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.
@techreport{SimplexDPLLT,
AUTHOR = {Bruno Dutertre and Leonardo de Moura},
INSTITUTION = {{SRI International}},
TITLE = {{Integrating Simplex with DPLL(T)}},
YEAR = 2006,
NUMBER = {SRI-CSL-06-01}
}