close
Skip to main content
Springer Nature Link
Log in

A BDD SAT solver for satisfiability testing: An industrial case study

  • Published:
Save article
View saved research
Annals of Mathematics and Artificial Intelligence Aims and scope Submit manuscript

Abstract

The satisfiability problem (SAT) is a fundamental problem in mathematical logic, constraint satisfaction, VLSI engineering, and computing theory. Methods to solve the satisfiability problem play an important role in the development of computing theory and systems. In this paper, we give a BDD (Binary Decision Diagrams) SAT solver for practical asynchronous circuit design. The BDD SAT solver consists of a structural SAT formula preprocessor and a complete, incremental SAT algorithm that is able to find an optimal solution. The preprocessor compresses a large size SAT formula representing the circuit into a number of smaller SAT formulas. This avoids the problem of solving very large SAT formulas. Each small size SAT formula is solved by the BDD SAT algorithm efficiently. Eventually, the results of these subproblems are integrated together that contribute to the solution of the original problem. According to recent industrial assessments, this BDD SAT solver provides solutions to the practical, industrial asynchronous circuit design problems.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+
from $39.99 /Month
  • Starting from 10 chapters or articles per month
  • Access and download chapters and articles from more than 300k books and 2,500 journals
  • Cancel anytime
View plans

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, books and news in related subjects, suggested using machine learning.

References

  1. S.B. Akers, Binary decision diagrams,IEEE Trans. on Computers C-27(6) (1978) 509–516.

    Google Scholar 

  2. C.E. Blair, R.G. Jeroslow and J.K. Lowe, Some results and experiments in programming techniques for propositional logic,Computers and Operations Research 5 (1986) 633–645.

    Google Scholar 

  3. C.A. Brown and P.W. Purdom, An average time analysis of backtracking,SIAM J. Comput. 10(3) (1981) 583–593.

    Google Scholar 

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

    Google Scholar 

  5. K. Bugrara and P. Purdom, Clause order backtracking, Technical Report 311 (1990).

  6. M. Buro and H.K. Buning, Report on SAT competition, University of Paderborn (November, 1992).

  7. Tam-Anh Chu, Synthesis of self-timed VLSI circuits from graph-theoretic specifications, Ph.D. Thesis, Dept. of Electrical Engineering and Computer Science, MIT (June, 1987).

  8. S.A. Cook, The complexity of theorem-proving procedures,Proceedings of the 3rd ACM Symposium on Theory of Computing (1971) pp. 151–158.

  9. M. Davis, G. Logemann and D. Loveland, A machine program for theorem proving,Communications of the ACM 5 (1962) 394–397.

    Google Scholar 

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

    Google Scholar 

  11. S. Even,Graph Algorithms (Computer Science Press, 1979).

  12. M.R. Garey and D.S. Johnson,Computers and Intractability: A Guide to the Theory of NP-Completeness (Freeman, San Francisco, 1979).

    Google Scholar 

  13. J. Gu, TheUniSAT problem models (appendix),IEEE Trans. on Pattern Analysis and Machine Intelligence 14(8) (1992) 865.

    Google Scholar 

  14. J. Gu, Efficient local search for very large-scale satisfiability problem,SIGART Bulletin, ACM Press 3(1) (1992) 8–12.

    Google Scholar 

  15. J. Gu, Local search for satisfiability (SAT) problem,IEEE Trans. on Systems, Man. and Cybernetics 23(4) (1993) 1108–1129.

    Google Scholar 

  16. J. Gu, Global optimization for satisfiability (SAT) problem,IEEE Trans. on Knowledge and Data Engineering 6(3) (1994).

  17. J. Gu, Optimization algorithms for Satisfiability (SAT) problem, in:New Advances in Optimization and Approximation, ed. Ding-Zhu Du (Kluwer Academic Publishers, Boston, MA, Jan. 1994) pp. 72–154.

    Google Scholar 

  18. J. Gu and R. Puri, Asynchronous circuit synthesis with boolean satisfiability,IEEE Trans. on CAD 14(8) (1995) 961–973.

    Google Scholar 

  19. J.N. Hooker, A quantitative approach to logical inference,Decision Support Systems 4 (1988) 45–69.

    Google Scholar 

  20. J.N. Hooker, Resolution vs. cutting plane solution of inference problems: Some computational experience,Operations Research Letter 7(1) (1988) 1–7.

    Google Scholar 

  21. J.E. Hopcroft and J.D. Ullman,Introduction to Automata Theory, Languages, and Computations, Chapter 2 (Addison-Wesley, 1987).

  22. R.G. Jeroslow, Computation-oriented reductions of predicate to propositional logic,Decision Support Systems 4 (1988) 183–197.

    Google Scholar 

  23. A.P. Kamath, N.K. Karmarkar, K.G. Ramakrishnan and M.G.C. Resende, Computational experience with an interior point algorithm on the satisfiability problem,Annals of Operations Research 25 (1990) 43–58.

    Google Scholar 

  24. A.P. Kamath, N.K. Karmarkar, K.G. Ramakrishnan and M.G.C. Resende, Computational experience with an interior point algorithm on the satisfiability problem, Working paper, Mathematical Sciences Research Center, AT&T Bell Laboratories (October, 1989).

  25. T. Larrabee, Test pattern generation using Boolean satisfiability,IEEE Trans. on CAD 11(1) (1992) 4–15.

    Google Scholar 

  26. L. Lavagno, K. Keutzer and A. Sangiovanni-Vincentelli, Algorithms for synthesis of Hazard-free asynchronous circuits,Proc. of 28th ACM/IEEE Design Automation Conference (1991) pp. 302–308.

  27. L. Lavagno, C. Moon, R. Brayton and A. Sangiovanni-Vincentelli, Solving the state assignment problem for signal transition graphs,Proc. of 29th ACM/IEEE Design Automation Conference (1992) pp. 568–572.

  28. C.Y. Lee, Representation of switching circuits by binary decision programs,Bell Systems Technical Journal 38 (July, 1959) 985–999.

    Google Scholar 

  29. K.J. Lin and C.S. Lin, Automatic synthesis of asynchronous circuits,Proc. of 28th ACM/IEEE Design Automation Conference (1991) pp. 296–301.

  30. S. Malik, A. Wang, R. Brayton and A. Sangiovanni-Vincentelli, Logic verification using binary decision diagrams in a logic synthesis environment,Proc. of ACM/IEEE International Conference on CAD (1988).

  31. T. Murata, Petri nets: Properties, analysis and applications,Proc. of the IEEE 77(4) (1989) pp. 541–580.

    Google Scholar 

  32. C. Myers and T.H. Meng, Synthesis of timed asynchronous circuits,IEEE Trans. on VLSI Systems 1(2) (1993) 106–119.

    Google Scholar 

  33. P.M. Pardalos and Y. Li, Integer programming, in:Handbook of Statistics, ed. C.R. Rao (1993) pp. 279–302.

  34. P.W. Purdom, A survey of average time analyses of satisfiability algorithms,J. of Information Processing 13(4) (1990) 449–455.

    Google Scholar 

  35. P.W. Purdom, Search rearrangement backtracking and polynomial average time,Artificial Intelligence 21 (1983) 117–133.

    Google Scholar 

  36. P.W. Purdom and G.N. Haven, Backtracking and probing, Technical Report No. 387, Dept. of Computer Science, Indiana University (August, 1993).

  37. R. Puri and J. Gu, An efficient algorithm for microword length minimization,Local Search for the Satisfiability Problem (Appendix),Proc. of 29th ACM/IEEE Design Automation Conference (1992) pp. 651–656.

  38. R. Puri and J. Gu, An efficient algorithm to search for minimal closed covers in sequential machines,IEEE Transactions on CAD 12(6) (1993) 737–745.

    Google Scholar 

  39. R. Puri and J. Gu, Asynchronous circuit synthesis: Persistency and complete state coding constraints in signal transition graphs,International Journal of Electronics 75(5) (1993) 933–940.

    Google Scholar 

  40. R. Puri and J. Gu, Signal transition graph constraints for speed-independent circuit synthesis,Proc. of IEEE International Circuits and Systems Symposium (1993).

  41. R. Puri and J. Gu, A divide-and-conquer approach for asynchronous interface synthesis,Proc. of 7th ACM/IEEE HLSS (1994) pp. 123–131.

  42. J.A. Robinson, A machine-oriented logic based on the resolution principle,J. of ACM (1965) 23–41.

  43. B. Selman, H. Levesque and D. Mitchell, A new method for solving hard satisfiability problems,Proceedings of AAAI '92 (July, 1992) pp. 440–446.

  44. P.R. Stephan, R.K. Brayton and A. Sangiovanni-Vincentelli, Combinational test generation using satisfiability, Technical Report UCB/ERL M92/112, Dept. of EECS, Univ. of California, Berkeley (October, 1992).

    Google Scholar 

  45. P. Vanbekbergen, G. Goossens, F. Catthoor and H. De Man, Optimized synthesis of asynchronous control circuits from graph-theoretic specifications,IEEE Trans. on CAD 11(11) (1992) 1426–1438.

    Google Scholar 

  46. P. Vanbekbergen, B. Lin, G. Goossens and H. De Man, A generalized state assignment theory for transformations on signal transition graphs,Proc. of ACM/IEEE International Conference on CAD (1992) pp. 112–117.

  47. M.L. Yu and P.A. Subrahmanyam, A new approach for checking the unique state coding property of signal transition graphs,Proc. of ACM/IEEE European Conference on CAD (1992) pp. 312–321.

Download references

Author information

Authors and Affiliations

  1. IBM Thomas J. Watson Research Center, 10598, Yorktown Heights, NY, USA

    Ruchir Puri & Jun Gu

  2. Department of Electrical & Computer Engineering, University of Calgary, T2N 1N4, Calgary, AB, Canada

    Ruchir Puri & Jun Gu

Authors
  1. Ruchir Puri
    View author publications

    Search author on:PubMed Google Scholar

  2. Jun Gu
    View author publications

    Search author on:PubMed Google Scholar

Additional information

This research is supported in part by the 1993 ACM/IEEE Design Automation Award, by the Alberta Microelectronics Graduate Scholarship, by the NSERC research grant OGP0046423, and was supported in part by the NSERC strategic grant MEF0045793.

Presently, Jun Gu is on leave with the Department of Computer Science, Hong Kong University of Science and Technology, Clear Water Bay, Kowloon, Hong Kong.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Puri, R., Gu, J. A BDD SAT solver for satisfiability testing: An industrial case study. Ann Math Artif Intell 17, 315–337 (1996). https://doi.org/10.1007/BF02127973

Download citation

  • Issue date:

  • DOI: https://doi.org/10.1007/BF02127973

Keywords