Generalizing DPLL and satisfiability for equalities
Bahareh Badban, van de Jaco Pol, Olga Tveretina, Hans Zantema · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 2004
Abstract. We present GDPLL, a generalization of the DPLL procedure. It solves the satisfiability problem for decidable fragments of quantifierfree first-order logic. Sufficient conditions are identified for proving soundness, termination and completeness of GDPLL. We show how the original DPLL procedure is an instance. Subsequently the GDPLL instances for equality logic, and the logic of equality over infinite ground term algebras are presented. Based on this, we implemented a decision procedure for inductive datatypes. We provide some new benchmarks, in order to compare variants.