| Unknown (2000) | |||||||||||||||||
Abstract | |||||||||||||||||
| In this paper we present a method for determining satis ability of formulae represented by Boolean Expression Diagrams. The method uses the Up One 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. | |||||||||||||||||
Publication details | |||||||||||||||||
| |||||||||||||||||