- 1.M.R. Garey and D. S. Johnson, Computers and Intractability: A Guide to Theory ofNP-Completeness, W. H. Freeman and Company, 1979. Google ScholarDigital Library
- 2.M. Davis and H. Putnam, "A Computing Procedure for Quantification Theory", Journal of the ACM, vol. 7, pp. 201-215, 1960. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 5.T. Larabee, Efficient Generation of Test Patterns using Sati~fiability, PhD thesis, Dept. of Computer Science, Stanford University, Feb. 1990. Google ScholarDigital Library
- 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 Scholar
- 7.R. Zabih and D. A. McAllester, "A Rearrangement Search Strategy for Determining Propositional Satisfiability", in P~vc. Natl. Conf. on AI, 1988.Google Scholar
- 8.J. Marques-Silva and K. A. Sakallah, "GRASP - A New Search Algorithm for Satisfiability", in ICCAD'96, pp. 220-227, Nov. 1996. Google ScholarDigital Library
- 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 ScholarDigital Library
- 10.R.E. Bryant, "Graph Based Algorithm for Boolean Function Manipulation", IEEE Transactions on Computers, vol. C-35, pp. 677-691, August 1986. Google ScholarDigital Library
- 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 ScholarDigital Library
- 12.P. Ashar and et al., "Boolean Satisfiability and Equivalence Checking using General Binary Decision Diagrams", in Proc. ICCD, 1991. Google ScholarDigital Library
- 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 Scholar
- 14.B. Lin and F. Somenzi, "Minimization of Symbolic Relations", in ICCAD, 90.Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 17.A.J. Hu and D. L. Dill, "Reducing BDD Size by Exploiting Functional Dependencies", in Proc. DAC, pp. 266-271, 93. Google ScholarDigital Library
- 18.A. Narayan and et al., "Partitioned ROBDDs: A Compact Canonical and Efficient Representation for Boolean Functions", in Proc. ICCAD, '96. Google ScholarDigital Library
- 19.R.K. Brayton, C. McMullen, G.D. Hachtel, and A. Sangiovanni-Vincentelli, Logic Minimization Algorithms for VLSI Synthesis, Kluwer Academic Publishers, 1984. Google ScholarDigital Library
- 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 Scholar
- 21.C.L. Huang, "Private Communication", Avery Design Systems, Inc.Google Scholar
- 22.F. Brown, Boolean Reasoning, Kluwer Academic Publishers, 1990.Google Scholar
- 23.G.D. Hachtel and F. Somenzi, Logic Synthesis and Verification Algorithms, Kluwer Academic Publishers, 1996. Google ScholarDigital Library
- 24.G. DeMicheli, Synthesis and Optimization of Digital Circuits, McGraw-Hill, 94.Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
Index Terms
- A BDD-based satisfiability infrastructure using the unate recursive paradigm
Recommendations
WPG-controlled quantum BDD circuits with BDD architecture on GaAs-based hexagonal nanowire network structure
Special issue on 1D Nanomaterials 2011One-dimensional nanowire quantum devices and basic quantum logic AND and OR unit on hexagonal nanowire units controlled by wrap gate (WPG) were designed and fabricated on GaAs-based one-dimensional electron gas (1-DEG) regular nanowire network with ...
Size-energy tradeoffs for unate circuits computing symmetric Boolean functions
A unate gate is a logical gate computing a unate Boolean function, which is monotone in each variable. Examples of unate gates are AND gates, OR gates, NOT gates, threshold gates, etc. A unate circuit C is a combinatorial logic circuit consisting of ...
Biconditional BDD: a novel canonical BDD for logic synthesis targeting XOR-rich circuits
DATE '13: Proceedings of the Conference on Design, Automation and Test in EuropeWe present a novel class of decision diagrams, called Biconditional Binary Decision Diagrams (BBDDs), that enable efficient logic synthesis for XOR-rich circuits. BBDDs are binary decision diagrams where the Shannon's expansion is replaced by the ...
Comments