skip to main content
10.1145/343647.343769acmconferencesArticle/Chapter ViewAbstractPublication PagesdateConference Proceedingsconference-collections
Article
Free Access

A BDD-based satisfiability infrastructure using the unate recursive paradigm

Authors Info & Claims
Published:01 January 2000Publication History
First page image

References

  1. 1.M.R. Garey and D. S. Johnson, Computers and Intractability: A Guide to Theory ofNP-Completeness, W. H. Freeman and Company, 1979. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. 2.M. Davis and H. Putnam, "A Computing Procedure for Quantification Theory", Journal of the ACM, vol. 7, pp. 201-215, 1960. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. 3.C.E. Blair and et al., "Some Results and Experiments in Programming Techniques for Propositional Logic", Comp. and Opel: Res., vol. 13, pp. 633-645, 1986. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. 4.J.W. Freeman, "Improvements to Propositional Satisfiability Search Algorithms", Ph.D. Dissertation, Dept. of Comp. and Inf. Sc., Univ. of Penn., vol., May 1995. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. 5.T. Larabee, Efficient Generation of Test Patterns using Sati~fiability, PhD thesis, Dept. of Computer Science, Stanford University, Feb. 1990. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. 6.P.R. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Combinational Test Generation using Satisfiability", Technical Report UCB/ERL M92/112, Dept. of EECS., Univ. of California at Berkeley, Oct. 1992.Google ScholarGoogle Scholar
  7. 7.R. Zabih and D. A. McAllester, "A Rearrangement Search Strategy for Determining Propositional Satisfiability", in P~vc. Natl. Conf. on AI, 1988.Google ScholarGoogle Scholar
  8. 8.J. Marques-Silva and K. A. Sakallah, "GRASP - A New Search Algorithm for Satisfiability", in ICCAD'96, pp. 220-227, Nov. 1996. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. 9.L.G. Silva, L. M. Silvera, and J. Marques-Silva, "Algorithms for Solving Boolean Satisfiability in Combinational Circuits", in Proc. DATE, pp. 526-530, March 1999. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. 10.R.E. Bryant, "Graph Based Algorithm for Boolean Function Manipulation", IEEE Transactions on Computers, vol. C-35, pp. 677-691, August 1986. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. 11.K. S. Brace, R. Rudell, and R. E. Bryant, "Efficient Implementation of the BDD Package", Proceedings of the Design Automation Conference, vol. , pp. 40-45, 1990. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. 12.P. Ashar and et al., "Boolean Satisfiability and Equivalence Checking using General Binary Decision Diagrams", in Proc. ICCD, 1991. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. 13.S. Jeong and F. Somenzi, "A New Algorithm for the Binate Covering Problem and its Application to the Minimization of Boolean Relations", in ICCAD, 92.Google ScholarGoogle Scholar
  14. 14.B. Lin and F. Somenzi, "Minimization of Symbolic Relations", in ICCAD, 90.Google ScholarGoogle Scholar
  15. 15.T. Villa and et al., "Explicit and Implicit Algorithms for Binate Covering Problems", IEEE Trans. CAD, vol. Vol. 16, pp. 677-691, July 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. 16.A.J. Hu, G. York, and D. L. Dill, "New Techniques for Efficient Verification with Implicitly Conjoined BDDs", in Proc. DAC, pp. 276-282, 1994. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. 17.A.J. Hu and D. L. Dill, "Reducing BDD Size by Exploiting Functional Dependencies", in Proc. DAC, pp. 266-271, 93. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. 18.A. Narayan and et al., "Partitioned ROBDDs: A Compact Canonical and Efficient Representation for Boolean Functions", in Proc. ICCAD, '96. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. 19.R.K. Brayton, C. McMullen, G.D. Hachtel, and A. Sangiovanni-Vincentelli, Logic Minimization Algorithms for VLSI Synthesis, Kluwer Academic Publishers, 1984. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. 20.R. Rudell and A. Sangiovanni-Vincentelli, "Multiple-valued Minimization for PLA Optimization", IEEE T~: on CAD, vol. CAD-6, pp. 727-750, Sept. 1987.Google ScholarGoogle Scholar
  21. 21.C.L. Huang, "Private Communication", Avery Design Systems, Inc.Google ScholarGoogle Scholar
  22. 22.F. Brown, Boolean Reasoning, Kluwer Academic Publishers, 1990.Google ScholarGoogle Scholar
  23. 23.G.D. Hachtel and F. Somenzi, Logic Synthesis and Verification Algorithms, Kluwer Academic Publishers, 1996. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. 24.G. DeMicheli, Synthesis and Optimization of Digital Circuits, McGraw-Hill, 94.Google ScholarGoogle Scholar
  25. 25.G. Cabodi and et al., "Disjunctive Partitioning and Partial Iterative Squaring: An Effective Approach for Symbolic Traversal of Large Circuits", in Proc. DAC, '97. Google ScholarGoogle ScholarDigital LibraryDigital Library
  26. 26.F. Fallah, S. Devadas, and K. Keutzer, "Functional Vector Generation for HDL models using Linear Programming and 3-Satisfiability", in Proc. DAC, '97. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. A BDD-based satisfiability infrastructure using the unate recursive paradigm

        Recommendations

        Comments

        Login options

        Check if you have access through your login credentials or your institution to get full access on this article.

        Sign in
        • Published in

          cover image ACM Conferences
          DATE '00: Proceedings of the conference on Design, automation and test in Europe
          January 2000
          707 pages
          ISBN:1581132441
          DOI:10.1145/343647

          Copyright © 2000 ACM

          Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

          Publisher

          Association for Computing Machinery

          New York, NY, United States

          Publication History

          • Published: 1 January 2000

          Permissions

          Request permissions about this article.

          Request Permissions

          Check for updates

          Qualifiers

          • Article

          Acceptance Rates

          Overall Acceptance Rate518of1,794submissions,29%

        PDF Format

        View or Download as a PDF file.

        PDF

        eReader

        View online with eReader.

        eReader