Satisfiability Checking Using Boolean Expression Diagrams

TR-2000-1, Authors: Poul F. Williams, Henrik R. Andersen and Henrik Hulgaard

Poul Frederick Williams
Henrik Reif Andersen
Henrik Hulgaard

October 2000

Abstract

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.
Technical report TR-2000-1 in IT University Technical Report Series, October 2000.

Available as PDF.