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.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Leonardo Mendonça de Moura, Nikolaj Bjørner
• Keywords: Automated Reasoning, CADE 2008, E-matching Based Smt, Efficient Smt Solvers, Satisfiability Modulo Theories