TY - RPRT
T1 - Satisfiability Checking Using Boolean Expression Diagrams
AU - Williams, Poul Frederick
AU - Andersen, Henrik Reif
AU - Hulgaard, Henrik
PY - 2000/10
Y1 - 2000/10
N2 - In this paper we present a method for determining satisfiability of formulae represented by Boolean Expression Diagrams. The method uses the upone algorithm for splitting on variables and rewriting rules instead of unit propagation. We show how to combine the method with BDD construction. In this way our method can be seen as bridging the gap between standard SAT-solvers and BDD construction.
AB - In this paper we present a method for determining satisfiability of formulae represented by Boolean Expression Diagrams. The method uses the upone algorithm for splitting on variables and rewriting rules instead of unit propagation. We show how to combine the method with BDD construction. In this way our method can be seen as bridging the gap between standard SAT-solvers and BDD construction.
M3 - Report
T3 - IT University Technical Report Series
BT - Satisfiability Checking Using Boolean Expression Diagrams
PB - IT-Universitetet i København
CY - Copenhagen
ER -