{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:18:54Z","timestamp":1759331934596},"publisher-location":"Berlin\/Heidelberg","reference-count":42,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354058403X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0016843","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:52:57Z","timestamp":1132732377000},"page":"34-49","source":"Crossref","is-referenced-by-count":35,"title":["Ordered Binary Decision Diagrams and the Davis-Putnam procedure"],"prefix":"10.1007","author":[{"given":"Tom\u00e1s E.","family":"Uribe","sequence":"first","affiliation":[]},{"given":"Mark E.","family":"Stickel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","volume-title":"Technical report","author":"A. Anuchitanukul","year":"1994","unstructured":"Anuchitanukul, A., and Manna, Z. Anti-isomorphic BDDs. Technical report, Computer Science Department, Stanford University, Stanford, CA, June 1994."},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"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\u2013191.","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"4_CR3","unstructured":"Benhamou, F., and Colmerauer, A., Eds. Constraint Logic Programming: Selected Research. MIT Press, 1993."},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"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\u201312.","DOI":"10.1016\/B978-0-444-88771-9.50007-6"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Brace, K. S., Rudell, R. L., and Bryant, R. E. Efficient implementation of a BDD package. In Proc. 27\n                  th\n                Design Automation Conf. (1990), pp. 40\u201345.","DOI":"10.1145\/123186.123222"},{"issue":"8","key":"4_CR6","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"Bryant, R. E. Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Computers 35, 8 (Aug. 1986), 677\u2013691.","journal-title":"IEEE Trans. on Computers"},{"issue":"2","key":"4_CR7","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"R. E. Bryant","year":"1991","unstructured":"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\u2013213.","journal-title":"IEEE Trans. on Computers"},{"issue":"3","key":"4_CR8","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. E. Bryant","year":"1992","unstructured":"Bryant, R. E. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24, 3 (Sept. 1992), 293\u2013318.","journal-title":"ACM Computing Surveys"},{"issue":"2","key":"4_CR9","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., and Hwang, L. J. Symbolic modelchecking: 1020 states and beyond. Information and Computation 98, 2 (June 1992), 142\u2013170.","journal-title":"Information and Computation"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"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\n                  th\n                Design Automation Conf. (1991), pp. 417\u2013420.","DOI":"10.1145\/127601.127705"},{"issue":"2","key":"4_CR11","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/S0747-7171(87)80065-2","volume":"4","author":"W. B\u00fcttner","year":"1987","unstructured":"B\u00fcttner, W., and Simonis, H. Embedding Boolean expressions into logic programming. J. of Symbolic Computation 4, 2 (Oct. 1987), 191\u2013205.","journal-title":"J. of Symbolic Computation"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Chandrasekhar, M. S., Privitera, J. P., and Conradt, K. W. Application of term rewriting techniques to hardware design verification. In Proc. 24\n                  th\n                Design Automation Conf. (1987), pp. 277\u2013282.","DOI":"10.1145\/37888.37930"},{"key":"4_CR13","unstructured":"Claesen, L. J., Ed. Formal VLSI Correctness Verification\u2014VLSI Design Methods, vol. II. Elsevier, 1990. Chap. 2, Efficient Tautology Checking Algorithms."},{"key":"4_CR14","unstructured":"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)."},{"key":"4_CR15","unstructured":"Crawford, J. M., and Auton, L. D. Experimental results on the crossover point in satisfiability problems. In Proc. 11\n                  th\n                Nat. Conf. on AI (1993), pp. 21\u201327."},{"issue":"7","key":"4_CR16","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., and Loveland, D. A machine program for theorem-proving. Comm. ACM 5, 7 (July 1962), 394\u2013397.","journal-title":"Comm. ACM"},{"key":"4_CR17","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., and Putnam, H. A computing procedure for quantification theory. J. ACM 7 (1960), 201\u2013215.","journal-title":"J. ACM"},{"issue":"5","key":"4_CR18","doi-asserted-by":"crossref","first-page":"722","DOI":"10.1109\/43.277617","volume":"12","author":"S. Devadas","year":"1993","unstructured":"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\u2013723.","journal-title":"IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems"},{"issue":"5","key":"4_CR19","doi-asserted-by":"crossref","first-page":"710","DOI":"10.1109\/12.53586","volume":"39","author":"S. J. Friedman","year":"1990","unstructured":"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\u2013713.","journal-title":"IEEE Trans. on Computers"},{"key":"4_CR20","unstructured":"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\u201357."},{"issue":"25","key":"4_CR21","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","volume":"3","author":"J. Hsiang","year":"1985","unstructured":"Hsiang, J. Refutational theorem proving using term-rewriting systems. Artificial Intelligence 3, 25 (Mar. 1985), 255\u2013300.","journal-title":"Artificial Intelligence"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Hu, A. J., and Dill, D. L. Reducing BDD size by exploiting functional dependencies. In Proc. 30\n                  th\n                Design Automation Conf. (1993), pp. 266\u2013271.","DOI":"10.1145\/157485.164888"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"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\u2013420.","DOI":"10.1109\/ICCAD.1992.279335"},{"key":"4_CR24","unstructured":"Joyce, J. J., and Seger, C.-J. H. Linking BDD-based symbolic evaluation to interactive theorem-proving. In 30thDesign Autom. Conf. (1993), pp. 469\u2013474."},{"key":"4_CR25","volume-title":"Technical Report UCB\/ERL M90\/125","author":"T. Y. K. Kam","year":"1990","unstructured":"Kam, T. Y. K., and Brayton, R. K. Multi-valued decision diagrams. Technical Report UCB\/ERL M90\/125, University of California, Berkeley, Dec. 1990."},{"key":"4_CR26","unstructured":"Long, D. E. Model Checking, Abstraction, and Compositional Verification. PhD thesis, School of Computer Science, Carnegie Mellon Univ., July 1993."},{"key":"4_CR27","unstructured":"McCarthy, J. A tough nut for proof procedures. AI Memo 16, Stanford University, July 1964."},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"McMillan, K. L. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"4_CR29","unstructured":"Minato, S. Zero-supressed BDDs for set manipulation in combinatorial problems. In Proc. 30\n                  th\n                Design Automation Conf. (1993), pp. 272\u2013277."},{"key":"4_CR30","volume-title":"Technical Report 84","author":"J. S. Moore","year":"1992","unstructured":"Moore, J. S. Introduction to the OBDD algorithm for the ATP community. Technical Report 84, Computational Logic, Inc., Austin, Texas, Oct. 1992."},{"key":"4_CR31","unstructured":"Rauzy, A. Using enumerative methods for Boolean unification. In [3]. MIT Press, 1993, ch. 13, pp. 237\u2013251."},{"key":"4_CR32","unstructured":"Rauzy, A. Notes on the design of an open Boolean solver. In Proc. Intl. Conf. on Logic Programming (1994). To appear."},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Rudell, R. Dynamic variable ordering for ordered binary decision diagrams. In IEEE Intl. Conf. on Computer-Aided Design (Nov. 1993), pp. 42\u201347.","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"4_CR34","unstructured":"Selman, B., Levesque, H., and Mitchell, D. A new method for solving hard satisfiability problems. In Proc. 10\n                  th\n                Nat. Conf. on AI (July 1992), pp. 440\u2013446."},{"key":"4_CR35","unstructured":"Simonis, H., and Dincbas, M. Propositional calculus problems in CHIP. In [3]. MIT Press, 1993, ch. 15, pp. 269\u2013285."},{"key":"4_CR36","unstructured":"Slaney, J. Finder version 3.0 \u2014 notes and guide. Technical report, Centre for Information Science Research, Australian National University, 1993."},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Slaney, J., Fujita, M., and Stickel, M. Automated reasoning and exhaustive search: Quasigroup existence problems. Computers and Mathematics with Applications. To appear.","DOI":"10.1016\/0898-1221(94)00219-B"},{"key":"4_CR38","volume-title":"PhD thesis","author":"S. Subramanian","year":"1993","unstructured":"Subramanian, S.A Mechanized Framework for Specifying Problem Domains and Verifying Plans. PhD thesis, Dept. of Comp. Science, U. of Texas, Austin, 1993."},{"key":"4_CR39","unstructured":"Wallace, M. Personal communication. ECRC, Munich, Germany, July 1993."},{"key":"4_CR40","unstructured":"Walsh, T. Personal communication. University of Edinburgh, Oct. 1993."},{"key":"4_CR41","first-page":"1","volume":"22","author":"H. S. Zhang","year":"1993","unstructured":"Zhang, H. Sato: A decision procedure for propositional logic. Association for Automated Reasoning Newsletter, 22 (Mar. 1993), 1\u20133.","journal-title":"Association for Automated Reasoning Newsletter"},{"key":"4_CR42","unstructured":"Zhang, H., and Stickel, M. E. Implementing the Davis-Putnam algorithm by tries. Draft manuscript, Mar. 1994."}],"container-title":["Lecture Notes in Computer Science","Constraints in Computational Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0016843.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:37:00Z","timestamp":1607549820000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0016843"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354058403X"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/bfb0016843","relation":{},"subject":[]}}