Deciding effectively propositional logic using DPLL and substitution sets (Q972432)

This paper introduces a DPLL calculus that is a decision procedure for the Bernays-Schönfinkel class, also called EPR. This class of first-order formulas provides a generalization of pure propositional satisfiablility and quantified Boolean formulas. The presented DPLL calculus is complete in EPR and combines techniques for efficient propositional search, such as Binary Decision Diagrams. The calculus works directly at the level of sets and it is opened up to efficient implementations based on data structures, with promising preliminary empirical results.