Deciding effectively propositional logic using DPLL and substitution sets (Q972432)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Deciding effectively propositional logic using DPLL and substitution sets |
scientific article |
Statements
Deciding effectively propositional logic using DPLL and substitution sets (English)
0 references
26 May 2010
0 references
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.
0 references
DPLL
0 references
SAT
0 references
BDDS
0 references
effectively propositional logic
0 references