Engineering DPLL(T) + Saturation

9 years 10 months ago
Engineering DPLL(T) + Saturation
Satisfiability Modulo Theories (SMT) solvers have proven highly scalable, efficient and suitable for integrated theory reasoning. The most efficient SMT solvers rely on refutationally incomplete methods for incorporating quantifier reasoning. We describe a calculus and a system that tightly integrates Superposition and DPLL(T). In the calculus, all non-unit ground clauses are delegated to the DPLL(T) core. The integration is tight, dependencies on case splits are tracked as hypotheses in the saturation engine. The hypotheses are discharged during backtracking. The combination is refutationally complete for first-order logic, and its implementation is competitive in performance with E-matching based SMT solvers on problems they are good at.
Leonardo Mendonça de Moura, Nikolaj Bj&osla
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Leonardo Mendonça de Moura, Nikolaj Bjørner
Comments (0)