Ordered Binary Decision Diagrams and the Davis-Putnam procedure

1. Anuchitanukul, A., and Manna, Z. Anti-isomorphic BDDs. Technical report, Computer Science Department, Stanford University, Stanford, CA, June 1994.

   Google Scholar 

2. Bahar, R. I., Frohm, E. A., Gaona, C. M., Hachtel, G. D., Mach, E., Pardo, A., and Somenzi, F. Algebraic decision diagrams and their applications. In IEEE Intl. Conf. on Computer-Aided Design (Nov. 1993), pp. 188–191.

   Google Scholar 

3. Benhamou, F., and Colmerauer, A., Eds. Constraint Logic Programming: Selected Research. MIT Press, 1993.

   Google Scholar 

4. Boy de la Tour, T., and Chaminade, G. The use of renaming to improve the efficiency of clausal theorem proving. In Art. Int. IV: Methodology, Systems, Applications (1990), P. Jorrand and V. Sgurev, Eds., Elsevier, pp. 3–12.

   Google Scholar 

5. Brace, K. S., Rudell, R. L., and Bryant, R. E. Efficient implementation of a BDD package. In Proc. 27^thDesign Automation Conf. (1990), pp. 40–45.

   Google Scholar 

6. Bryant, R. E. Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Computers 35, 8 (Aug. 1986), 677–691.

   Google Scholar 

7. Bryant, R. E. On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Trans. on Computers 40, 2 (Feb. 1991), 205–213.

   Google Scholar 

8. Bryant, R. E. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24, 3 (Sept. 1992), 293–318.

   Google Scholar 

9. Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., and Hwang, L. J. Symbolic modelchecking: 10²⁰ states and beyond. Information and Computation 98, 2 (June 1992), 142–170.

   Google Scholar 

10. Butler, K. M., Ross, D. E., Kapur, R., and Mercer, M. R. Heuristics to compute variable ordering for efficient manipulation of ordered binary decision diagrams. In Proc. 28^thDesign Automation Conf. (1991), pp. 417–420.

    Google Scholar 

11. Büttner, W., and Simonis, H. Embedding Boolean expressions into logic programming. J. of Symbolic Computation 4, 2 (Oct. 1987), 191–205.

    Google Scholar 

12. Chandrasekhar, M. S., Privitera, J. P., and Conradt, K. W. Application of term rewriting techniques to hardware design verification. In Proc. 24^thDesign Automation Conf. (1987), pp. 277–282.

    Google Scholar 

13. Claesen, L. J., Ed. Formal VLSI Correctness Verification—VLSI Design Methods, vol. II. Elsevier, 1990. Chap. 2, Efficient Tautology Checking Algorithms.

    Google Scholar 

14. Clarke, E. M., Fujita, M., McGeer, P. C., McMillan, K., Yang, J. C.-Y., and Zhao, X. Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. In Proc. Intl. Workshop on Logic Synthesis (May 1993).

    Google Scholar 

15. Crawford, J. M., and Auton, L. D. Experimental results on the crossover point in satisfiability problems. In Proc. 11^thNat. Conf. on AI (1993), pp. 21–27.

    Google Scholar 

16. Davis, M., Logemann, G., and Loveland, D. A machine program for theorem-proving. Comm. ACM 5, 7 (July 1962), 394–397.

    Google Scholar 

17. Davis, M., and Putnam, H. A computing procedure for quantification theory. J. ACM 7 (1960), 201–215.

    Google Scholar 

18. Devadas, S. Comparing two-level and ordered binary decision diagram representations of logic functions. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems 12, 5 (May 1993), 722–723.

    Google Scholar 

19. Friedman, S. J., and Supowitz, K.J. Finding the optimal variable ordering for binary decision diagrams. IEEE Trans. on Computers 39, 5 (May 1990), 710–713.

    Google Scholar 

20. Fujita, M., Slaney, J., and Bennett, F. Automatic generation of some results in finite algebra. In Proc. 14th Intl. Joint Conf. on AI (1993), pp. 52–57.

    Google Scholar 

21. Hsiang, J. Refutational theorem proving using term-rewriting systems. Artificial Intelligence 3, 25 (Mar. 1985), 255–300.

    Google Scholar 

22. Hu, A. J., and Dill, D. L. Reducing BDD size by exploiting functional dependencies. In Proc. 30^thDesign Automation Conf. (1993), pp. 266–271.

    Google Scholar 

23. Jeong, S.-W., and Somenzi, F. A new algorithm for the binate covering problem and its application to the minimization of Boolean relations. In IEEE Intl. Conf. on Computer-Aided Design (1992), pp. 417–420.

    Google Scholar 

24. Joyce, J. J., and Seger, C.-J. H. Linking BDD-based symbolic evaluation to interactive theorem-proving. In 30^thDesign Autom. Conf. (1993), pp. 469–474.

    Google Scholar 

25. Kam, T. Y. K., and Brayton, R. K. Multi-valued decision diagrams. Technical Report UCB/ERL M90/125, University of California, Berkeley, Dec. 1990.

    Google Scholar 

26. Long, D. E. Model Checking, Abstraction, and Compositional Verification. PhD thesis, School of Computer Science, Carnegie Mellon Univ., July 1993.

    Google Scholar 

27. McCarthy, J. A tough nut for proof procedures. AI Memo 16, Stanford University, July 1964.

    Google Scholar 

28. McMillan, K. L. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

    Google Scholar 

29. Minato, S. Zero-supressed BDDs for set manipulation in combinatorial problems. In Proc. 30^thDesign Automation Conf. (1993), pp. 272–277.

    Google Scholar 

30. Moore, J. S. Introduction to the OBDD algorithm for the ATP community. Technical Report 84, Computational Logic, Inc., Austin, Texas, Oct. 1992.

    Google Scholar 

31. Rauzy, A. Using enumerative methods for Boolean unification. In [3]. MIT Press, 1993, ch. 13, pp. 237–251.

    Google Scholar 

32. Rauzy, A. Notes on the design of an open Boolean solver. In Proc. Intl. Conf. on Logic Programming (1994). To appear.

    Google Scholar 

33. Rudell, R. Dynamic variable ordering for ordered binary decision diagrams. In IEEE Intl. Conf. on Computer-Aided Design (Nov. 1993), pp. 42–47.

    Google Scholar 

34. Selman, B., Levesque, H., and Mitchell, D. A new method for solving hard satisfiability problems. In Proc. 10^thNat. Conf. on AI (July 1992), pp. 440–446.

    Google Scholar 

35. Simonis, H., and Dincbas, M. Propositional calculus problems in CHIP. In [3]. MIT Press, 1993, ch. 15, pp. 269–285.

    Google Scholar 

36. Slaney, J. Finder version 3.0 — notes and guide. Technical report, Centre for Information Science Research, Australian National University, 1993.

    Google Scholar 

37. Slaney, J., Fujita, M., and Stickel, M. Automated reasoning and exhaustive search: Quasigroup existence problems. Computers and Mathematics with Applications. To appear.

    Google Scholar 

38. Subramanian, S.A Mechanized Framework for Specifying Problem Domains and Verifying Plans. PhD thesis, Dept. of Comp. Science, U. of Texas, Austin, 1993.

    Google Scholar 

39. Wallace, M. Personal communication. ECRC, Munich, Germany, July 1993.

    Google Scholar 

40. Walsh, T. Personal communication. University of Edinburgh, Oct. 1993.

    Google Scholar 

41. Zhang, H. Sato: A decision procedure for propositional logic. Association for Automated Reasoning Newsletter, 22 (Mar. 1993), 1–3.

    Google Scholar 

42. Zhang, H., and Stickel, M. E. Implementing the Davis-Putnam algorithm by tries. Draft manuscript, Mar. 1994.

    Google Scholar 

Download references