{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:39:22Z","timestamp":1778297962287,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540601050","type":"print"},{"value":"9783540494355","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0015246","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T06:40:23Z","timestamp":1131864023000},"page":"218-233","source":"Crossref","is-referenced-by-count":8,"title":["Differential BDDs"],"prefix":"10.1007","author":[{"given":"Anuchit","family":"Anuchitanukul","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zohar","family":"Manna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1s E.","family":"Uribe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"issue":"27","key":"14_CR1","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"6","author":"S. Akers","year":"1978","unstructured":"Akers, S.. Binary decision diagrams. IEEE Transactions on Computers 6, 27 (June 1978), 509\u2013516.","journal-title":"IEEE Transactions on Computers"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Ashar, P., Ghosh, A., and Devadas, S. Boolean satisfiability and equivalence checking using general binary decision diagrams. In IEEE International Conf. on Computer Design: VLSI in Computers and Processors (1991), pp. 259\u2013264.","DOI":"10.1109\/ICCD.1991.139893"},{"key":"14_CR3","unstructured":"Bani-Eqbal, B. Exclusive normal form of boolean circuits. Tech. Rep. UMCS-92-4-1, Department of Computer Science, University of Manchester, 1992."},{"key":"14_CR4","unstructured":"Becker, B., Bryant, R., Coudert, O., and Meinel, C., Eds. Report on the Third Workshop on Computer Aided Design and Test (Feb. 1995). http: \/\/www. informatik. uni-trier. de\/Design_and_Test\/."},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Becker, B., Drechsler, R., and Theobald, M. OKFDDs versus OBDDs and OFDDs. In International Colloquium on Automata, Languages and Programming (July 1995), LNCS. To appear.","DOI":"10.1007\/3-540-60084-1_98"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Bern, J., Meinel, C., and Slobodov\u00e1, A. Efficient OBDD-based boolean manipulation in CAD beyond current limits. In 32ndDesign Automation Conf. (1995).","DOI":"10.1145\/217474.217563"},{"key":"14_CR7","unstructured":"Bitner, J., Jain, J., Abadir, M., Abraham, J., and Fussell, D. Efficient algorithmic computation using indexed BDDs. In 24thIntl. Symposium on Fault-Tolerant Computing (1994), pp. 266\u2013275."},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Brace, K. S., Rudell, R. L., and Bryant, R. E. Efficient implementation of a BDD package. In 27thDesign Automation Conf. (1990), pp. 40\u201345.","DOI":"10.1145\/123186.123222"},{"issue":"8","key":"14_CR9","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":"14_CR10","doi-asserted-by":"publisher","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":"14_CR11","doi-asserted-by":"publisher","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"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Bryant, R. E., And Chen, Y.-A. Verification of arithmetic circuits with Binary Moment Diagrams. In 32nd Design Automation Conf. (June 1995). To appear.","DOI":"10.1145\/217474.217583"},{"issue":"2","key":"14_CR13","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. Burch","year":"1992","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., and Hwang, L. Symbolic modelchecking: 1020 states and beyond. Information and Computation 98, 2 (June 1992), 142\u2013170.","journal-title":"Information and Computation"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., McMillan, K., Zhao, X., Fujita, M., and Yang, J. Spectral transforms for large Boolean functions with applications to technology mapping. In 30thDesign Automation Conf. (June 1993).","DOI":"10.1145\/157485.164569"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Jeong, S., Plessier, B., Hachtel, G., and Somenzi, F. Extended BDD's: Trading off canonicity for structure in verification algorithms. In IEEE Intl. Conf. on Computer-Aided Design (1991), pp. 464\u2013467.","DOI":"10.1109\/ICCAD.1991.185305"},{"key":"14_CR16","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":"14_CR17","unstructured":"Karplus, K. Using if-then-else DAGs for multi-level logic minimization. In Advance Research in VLSI (1989), C. Seitz, Ed., MIT Press, pp. 101\u2013118."},{"key":"14_CR18","unstructured":"Lai, Y.-T., AND Sastry, S. Edge-valued binary decision diagrams for multi-level hierarchical verification. In 29thDesign Automation Conf. (1992), pp. 608\u2013613."},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Madre, J., and Billon, J. Proving circuit correctness using formal comparison between expected and extracted behaviour. In 25thDesign Automation Conf. (June 1988), pp. 205\u2013210.","DOI":"10.1109\/DAC.1988.14759"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"McMillan, K. L. Hierarchical representations of discrete functions, with application to model checking. In Proc. 6th Intl. Conf. on Computer-Aided Verification (June 1994), vol. 818 of LNCS, Springer-Verlag, pp. 41\u201354.","DOI":"10.1007\/3-540-58179-0_42"},{"key":"14_CR21","unstructured":"Minato, S. Zero-supressed BDDs for set manipulation in combinatorial problems. In 30thDesign Automation Conf. (1993), pp. 272\u2013277."},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Minato, S., Ishiura, N., and Jajima, S. Shared binary decision diagram with attributed edges for efficient boolean function manipulation. In 27thDesign Automation Conf. (1990), pp. 52\u201357.","DOI":"10.1145\/123186.123225"},{"key":"14_CR23","unstructured":"Possega, J., AND Lud\u00e4scher, B. Towards first-order deduction based on Shannon graphs. In Proc. 16thGerman Conf. on AI (GWAI-92) (1992), vol. 671 of LNAI, Springer-Verlag, pp. 67\u201376."},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Sieling, D., AND Wegener, I. Graph driven BDDs\u2014a new data structure for boolean functions. Theoretical Comput. Sci. 141, 2 (Apr. 1995).","DOI":"10.1016\/0304-3975(94)00078-W"},{"key":"14_CR25","first-page":"34","volume":"845","author":"T. E. Uribe","year":"1994","unstructured":"Uribe, T. E., and Stickel, M. E. Ordered binary decision diagrams and the Davis-Putnam procedure. In Proc. 1 st Intl. Conf. on Constraints in Computational Logics(Sept. 1994), vol. 845 of LNCS, pp. 34\u201349","journal-title":"LNCS"}],"container-title":["Lecture Notes in Computer Science","Computer Science Today"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0015246","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T13:03:50Z","timestamp":1736082230000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0015246"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540601050","9783540494355"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0015246","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}