Deciding Effectively Propositional Logic Using DPLL and Substitution Sets

We introduce a DPLL calculus that is a decision procedure for the Bernays-Schönfinkel class, also known as EPR. Our calculus allows combining techniques for efficient propositional search with data-structures, such as Binary Decision Diagrams, that can efficiently and succinctly encode finite sets o...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2010-04, Vol.44 (4), p.401-424
Main Authors: Piskac, Ruzica, de Moura, Leonardo, Bjørner, Nikolaj
Format: Article
Language:English
Subjects:
Artificial Intelligence
Automated reasoning
Calculus
Computer Science
Logic
Mathematical analysis
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Searching
Symbolic and Algebraic Manipulation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We introduce a DPLL calculus that is a decision procedure for the Bernays-Schönfinkel class, also known as EPR. Our calculus allows combining techniques for efficient propositional search with data-structures, such as Binary Decision Diagrams, that can efficiently and succinctly encode finite sets of substitutions and operations on these. In the calculus, clauses comprise of a sequence of literals together with a finite set of substitutions; truth assignments are also represented using substitution sets. The calculus works directly at the level of sets, and admits performing simultaneous constraint propagation and decisions, resulting in potentially exponential speedups over existing approaches.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-009-9161-6