We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Satisfiability checking using Boolean Expression Diagrams.
- Authors
Williams, Poul F.; Andersen, Henrik R.; Hulgaard, Henrik
- Abstract
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.
- Subjects
ALGORITHMS; GRAPHIC methods; DATA structures; ELECTRONIC data processing; ELECTRONIC file management; COMPUTER programming; BOOLEAN expressions
- Publication
International Journal on Software Tools for Technology Transfer, 2003, Vol 5, Issue 1, p4
- ISSN
1433-2779
- Publication type
Article
- DOI
10.1007/s10009-002-0102-5