Abstract
In this paper we present an algorithm for determining satisfiability of general Boolean formulas which are not necessarily on 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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
P. A. Abdulla, P. Bjesse, and N. EĂ©n. Symbolic reachability analysis based on SAT solvers. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2000.
H. R. Andersen and H. Hulgaard. Boolean expression diagrams. Information and Computation. (To appear).
H. R. Andersen and H. Hulgaard. Boolean expression diagrams. In IEEE Symposium on Logic in Computer Science (LICS), July 1997.
A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. ACM/IEEE Design Automation Conference (DAC), 1999.
A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1579 of Lecture Notes in Computer Science. Springer-Verlag, 1999.
A. Biere, E. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a PowerPC microprocessor using symbolic model checking without BDDs. In Computer Aided Verification (CAV), volume 1633 of Lecture Notes in Computer Science. Springer-Verlag, 1999.
P. Bjesse. SAT-based verification without state space traversal. In Proc. Formal Methods in Computer-Aided Design, Third International Conference, FMCAD’00, Austin, Texas, USA, Lecture Notes in Computer Science, November 2000.
F. Brglez and H. Fujiware. A neutral netlist of 10 combinational benchmarks circuits and a target translator in Fortran. In Special Session International Symposium on Circuits and Systems (ISCAS), 1985.
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677–691, August 1986.
R. E. Bryant. Binary decision diagrams and beyond: Enabling technologies forformal verification. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 236–243, November 1995.
M. Davis, G. Longemann, and D. Loveland. A machine program for theoremproving. Communications of the ACM, 5(7):394–397, July 1962.
M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:201–215, 1960.
E. Giunchiglia and R. Sebastiani. Applying the Davis-Putnam procedure to non-clausal formulas. In Proc. Italian National Conference on Artificial Intelligence, volume 1792 of Lecture Notes in Computer Science, Bologna, Italy, September 1999. Springer-Verlag.
Holger H. Hoos and Thomas Sttzle. SATLIB-the satisfiability library. http://aida.intellektik.informatik.tu-darmstadt.de/~hoos/SATLIB/.
H. Hulgaard, P. F. Williams, and H. R. Andersen. Equivalence checking of combinational circuits using boolean expression diagrams. IEEE Transactions on Computer Aided Design, July 1999.
W. Kunz and D. K. Pradhan. Recursive learning: A new implication technique for efficient solutions to CAD problems-test, verification, and optimization. IEEE Transactions on Computer Aided Design, 13(9):1143–1158, September 1994.
J. P. Marques-Silva and K. A. Sakallah. GRASP: A search algorithm for propositional satistability. IEEE Transactions on Computers, 48, 1999.
R. Rudell. Dynamic variable ordering for ordered binary decision diagrams. In Proc. International Conf. Computer-Aided Design (ICCAD), pages 42–47, 1993.
R. Sebastiani. Applying GSAT to non-clausal formulas. Journal of Artificial Intelligence Research (JAIR), 1:309–314, January 1994.
B. Selman, H. J. Levesque, and D. Mitchell. A new method for solving hard satistability problems. In P. Rosenbloom and P. Szolovits, editors, Proc. Tenth National Conference on Artificial Intelligence, pages 440–446, Menlo Park, California, 1992. American Association for Artificial Intelligence, AAAI Press.
M. Sheeran and G. Stå lmarck. A tutorial on Stålmarck’s proof procedure for propositional logic. In G. Gopalakrishnan and P. J. Windley, editors, Proc. Formal Methods in Computer-Aided Design, Second International Conference, FMCAD’98, Palo Alto/CA, USA, volume 1522 of Lecture Notes in Computer Science, pages 82–99, November 1998.
C.A.J. van Eijk. Sequential equivalence checking without state space traversal. In Proc. International Conf. on Design Automation and Test of Electronic-based Systems (DATE), 1998.
P. F. Williams. Formal Verification Based on Boolean Expression Diagrams. PhD thesis, Dept. of Information Technology, Technical University of Denmark, Lyngby, Denmark, August 2000. ISBN 87-89112-59-8.
P. F. Williams, A. Biere, E. M. Clarke, and A. Gupta. Combining decision diagrams and SAT procedures for efficient symbolic model checking. In Computer Aided Verification (CAV), volume 1855 of Lecture Notes in Computer Science, pages 124–138, Chicago, U.S.A., July 2000. Springer-Verlag.
H. Zhang. SATO: An efficient propositional prover. In William McCune, editor, Proceedings of the 14th International Conference on Automated deduction, volume 1249 of Lecture Notes in Artificial Intelligence, pages 272–275, Berlin, July 1997. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Williams, P.F., Andersen, H.R., Hulgaard, H. (2001). Satisfiability Checking Using Boolean Expression Diagrams. In: Margaria, T., Yi, W. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001. Lecture Notes in Computer Science, vol 2031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45319-9_4
Download citation
DOI: https://doi.org/10.1007/3-540-45319-9_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41865-8
Online ISBN: 978-3-540-45319-2
eBook Packages: Springer Book Archive