Satisfiability checking using Boolean Expression Diagrams

In this paper we present an algorithm for determining satisfiability of general Boolean formulas which are not necessarily in conjunctive normal form. The algorithm extends the well-known Davis–Putnam algorithm to work on Boolean formulas represented using Boolean Expression Diagrams (BEDs). The BED data structure allows the algorithm to take advantage of the built-in reduction rules and the sharing of sub-formulas. Furthermore, it is possible to combine the algorithm with traditional BDD construction (using Bryant’s Apply-procedure). By adjusting a single parameter to the BedSat algorithm, it is possible to control to what extent the algorithm behaves like the Apply-algorithm or like a SAT-solver. Thus, the algorithm can be seen as bridging the gap between standard SAT-solvers and BDDs. We present promising experimental results for 566 non-clausal formulas obtained from the multi-level combinational circuits in the ISCAS’85 benchmark suite and from performing model checking of a shift-and-add multiplier.