Anzeige
Erschienen in:
2006 | OriginalPaper | Buchkapitel
A Fast Linear-Arithmetic Solver for DPLL(T)
verfasst von : Bruno Dutertre, Leonardo de Moura
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.