{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T09:40:17Z","timestamp":1759138817591,"version":"3.44.0"},"reference-count":43,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Integration"],"published-print":{"date-parts":[[2002,12]]},"DOI":"10.1016\/s0167-9260(02)00047-0","type":"journal-article","created":{"date-parts":[[2002,12,10]],"date-time":"2002-12-10T17:20:56Z","timestamp":1039540856000},"page":"39-70","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":2,"title":["Minimization of Word-Level Decision Diagrams"],"prefix":"10.1016","volume":"33","author":[{"given":"Rolf","family":"Drechsler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"G\u00fcnther","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"H\u00f6reth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"8","key":"10.1016\/S0167-9260(02)00047-0_BIB1","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for Boolean function manipulation","volume":"35","author":"Bryant","year":"1986","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB2","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1109\/12.73590","article-title":"On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication","volume":"40","author":"Bryant","year":"1991","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB3","doi-asserted-by":"crossref","unstructured":"Y.-T. Lai, S. Sastry, Edge-valued binary decision diagrams for multi-level hierarchical verification, Design Automation Conference, 1992, pp. 608\u2013613.","DOI":"10.1109\/DAC.1992.227813"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB4","doi-asserted-by":"crossref","unstructured":"R. Drechsler, A. Sarabi, M. Theobald, B. Becker, M.A. Perkowski, Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagrams, Design Automation Conference, 1994, pp. 415\u2013419.","DOI":"10.1145\/196244.196444"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB5","unstructured":"E. Clarke, M. Fujita, P. McGeer, K.L. McMillan, J. Yang, X. Zhao, Multi terminal binary decision diagrams: An efficient data structure for matrix representation, International Workshop on Logic Synthesis, 1993, pp. P6a:1\u201315."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB6","doi-asserted-by":"crossref","unstructured":"R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo, F. Somenzi, Algebraic decision diagrams and their application, International Conference on CAD, 1993, pp. 188\u2013191.","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB7","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, Y.-A. Chen, Verification of Arithmetic functions with binary moment diagrams, Design Automation Conference, 1995, pp. 535\u2013541.","DOI":"10.1145\/217474.217583"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB8","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, M. Fujita, X. Zhao, Hybrid decision diagrams\u2014overcoming the limitations of MTBDDs and BMDs, International Conference on CAD, 1995, pp. 159\u2013163.","DOI":"10.1109\/ICCAD.1995.480007"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB9","doi-asserted-by":"crossref","unstructured":"R. Drechsler, B. Becker, S. Ruppertz, K*BMDs: a new data structure for verification, European Design & Test Conference, 1996, pp. 2\u20138.","DOI":"10.1109\/EDTC.1996.494118"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB10","doi-asserted-by":"crossref","unstructured":"L. Arditi, *BMDs can delay the use of theorem proving for verifying arithmetic assembly instructions, FMCAD, 1996, pp. 34\u201348.","DOI":"10.1007\/BFb0031798"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB11","unstructured":"Y.-A. Chen, R.E. Bryant, ACV: an arithmetic circuit verifier, International Conference on CAD, 1996, pp. 389\u2013403."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB12","unstructured":"E.M. Clarke, X. Zhao, Word level symbolic model checking\u2014a new approach for verifying arithmetic circuits, Technical Report CMU-CS-95-161, 1995."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB13","doi-asserted-by":"crossref","unstructured":"Y. Chen, E. Clarke, P. Ho, Y. Hoskote, T. Kam, M. Khaira, J. O\u2019Leary, X. Zhao, Verification of all circuits in a floating-point unit using word-level model checking, FMCAD, 1996, pp. 361\u2013365.","DOI":"10.1007\/BFb0031797"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB14","doi-asserted-by":"crossref","unstructured":"G. Kamhi, O. Weissberg, L. Fix, Automatic Datapath Extraction for Efficient Usage of HDD, Volume 1254 of LNCS, Computer Aided Verification, 1997.","DOI":"10.1007\/3-540-63166-6_12"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB15","unstructured":"M. Fujita, Y. Matsunaga, T. Kakuda, On variable ordering of binary decision diagrams for the application of multi-level synthesis, European Conference on Design Automation, 1991, pp. 50\u201354."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB16","unstructured":"R. Rudell, Dynamic variable ordering for ordered binary decision diagrams, International Conference on CAD, 1993, pp. 42\u201347."},{"issue":"10","key":"10.1016\/S0167-9260(02)00047-0_BIB17","doi-asserted-by":"crossref","first-page":"965","DOI":"10.1109\/43.728917","article-title":"Ordered Kronecker functional decision diagrams\u2014a data structure for representation and manipulation of Boolean functions","volume":"17","author":"Drechsler","year":"1998","journal-title":"IEEE Trans. CAD"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB18","doi-asserted-by":"crossref","unstructured":"S. H\u00f6reth, Implementation of a Multiple-Domain Decision Diagram Package, CHARME, Chapman & Hall, London, 1997, pp. 185\u2013202.","DOI":"10.1007\/978-0-387-35190-2_12"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB19","doi-asserted-by":"crossref","unstructured":"R. Drechsler, S. H\u00f6reth, Manipulation of *BMDs, ASP Design Automation Conference, 1998, pp. 433\u2013438.","DOI":"10.1109\/ASPDAC.1998.669516"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB20","unstructured":"R.E. Bryant, Y.-A. Chen, *PBHD: an efficient graph representation for floating point circuit verification, Technical report, CMU-CS-97-134, 1997."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB21","doi-asserted-by":"crossref","unstructured":"R. Drechsler, W. G\u00fcnther, Using lower bounds during dynamic BDD minimization, Design Automation Conference, 1999, pp. 29\u201332.","DOI":"10.1145\/309847.309858"},{"year":"1998","series-title":"Binary Decision Diagrams\u2014Theory and Implementation","author":"Drechsler","key":"10.1016\/S0167-9260(02)00047-0_BIB22"},{"issue":"9","key":"10.1016\/S0167-9260(02)00047-0_BIB23","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1109\/12.537122","article-title":"Improving the variable ordering of OBDDs in NP-complete","volume":"45","author":"Bollig","year":"1996","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB24","unstructured":"S. Malik, A.R. Wang, R.K. Brayton, A.L. Sangiovanni-Vincentelli, Logic verification using binary decision diagrams in a logic synthesis environment, International Conference on CAD, 1988, pp. 6\u20139."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB25","unstructured":"M. Fujita, H. Fujisawa, N. Kawato, Evaluation and improvements of Boolean comparison method based on binary decision diagrams, International Conference on CAD, 1988, pp. 2\u20135."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB26","doi-asserted-by":"crossref","unstructured":"D.E. Ross, K.M. Butler, R. Kapur, M.R. Mercer, Fast functional evaluation of candidate OBDD variable ordering, European Conference on Design Automation, 1991, pp. 4\u20139.","DOI":"10.1109\/EDAC.1991.206348"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB27","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1109\/43.184839","article-title":"Variable ordering algorithms for binary decision diagrams and their evolution","volume":"12","author":"Fujita","year":"1993","journal-title":"IEEE Trans. CAD"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB28","doi-asserted-by":"crossref","unstructured":"H. Fujii, G. Ootomo, C. Hori, Interleaving based variable ordering methods for ordered binary decision diagrams, International Conference on CAD, 1993 pp. 38\u201341.","DOI":"10.1109\/ICCAD.1993.580028"},{"issue":"47","key":"10.1016\/S0167-9260(02)00047-0_BIB29","doi-asserted-by":"crossref","first-page":"1398","DOI":"10.1109\/12.737685","article-title":"On variable ordering and decomposition type choice in OKFDDs","volume":"12","author":"Drechsler","year":"1998","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB30","unstructured":"S. Panda, F. Somenzi, Who are the variables in your neighborhood, International Conference on CAD, 1995, pp. 74\u201377."},{"issue":"2","key":"10.1016\/S0167-9260(02)00047-0_BIB31","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1109\/43.743706","article-title":"BDD minimization using symmetries","volume":"18","author":"Scholl","year":"1999","journal-title":"IEEE Trans. CAD"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB32","doi-asserted-by":"crossref","unstructured":"S. H\u00f6reth, R. Drechsler, Dynamic minimization of word-level decision diagrams, Design, Automation and Test in Europe, 1998, pp. 612\u2013617.","DOI":"10.1109\/DATE.1998.655921"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB33","doi-asserted-by":"crossref","unstructured":"U. Kebschull, E. Schubert, W. Rosenstiel, Multilevel logic synthesis based on functional decision diagrams, European Conference on Design Automation, 1992, pp. 43\u201347.","DOI":"10.1109\/EDAC.1992.205890"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB34","doi-asserted-by":"crossref","first-page":"1294","DOI":"10.1109\/12.544485","article-title":"Fast OFDD based minimization of fixed polarity Reed-Muller expressions","volume":"45","author":"Drechsler","year":"1996","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB35","doi-asserted-by":"crossref","unstructured":"K.S. Brace, R.L. Rudell, R.E. Bryant, Efficient implementation of a BDD package, Design Automation Conference, 1990, pp. 40\u201345.","DOI":"10.1145\/123186.123222"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB36","doi-asserted-by":"crossref","unstructured":"S. Minato, N. Ishiura, S. Yajima, Shared binary decision diagrams with attributed edges for efficient Boolean function manipulation, Design Automation Conference, 1990, pp. 52\u201357.","DOI":"10.1145\/123186.123225"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB37","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, K.L. McMillan, X. Zhao, M. Fujita, J. Yang, Spectral transforms for large Boolean functions with application to technology mapping, Design Automation Conference, 1993, pp. 54\u201360.","DOI":"10.1145\/157485.164569"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB38","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, Y.-A. Chen, Verification of arithmetic functions with binary moment diagrams, Technical report, CMU-CS-94-160, 1994.","DOI":"10.21236\/ADA281028"},{"issue":"2","key":"10.1016\/S0167-9260(02)00047-0_BIB39","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1023\/A:1008691605584","article-title":"Factored edge-valued binary decision diagrams","volume":"10","author":"Tafertshofer","year":"1997","journal-title":"Formal Methods Syst. Des. Int. J."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB40","unstructured":"R. Enders, Note on the complexity of binary moment diagram representations, IFIP WG 10.5 Workshop on Applications of the Reed-Muller Expansion in circuit Design, 1995, pp. 191\u2013197."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB41","unstructured":"S. Yang, Logic synthesis and optimization benchmarks user guide. Technical report 1\/95, Microelectronic Center of North Carolina, 1991."},{"key":"10.1016\/S0167-9260(02)00047-0_BIB42","doi-asserted-by":"crossref","unstructured":"R. Drechsler, B. Becker, S. Ruppertz, The K*BMD: a verification data structure, IEEE Des. Test Comput. (April-June 1997) 51\u201359.","DOI":"10.1109\/54.587742"},{"key":"10.1016\/S0167-9260(02)00047-0_BIB43","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1016\/0020-0190(96)00119-6","article-title":"On the effect of local changes in the variable ordering of ordered decision diagrams","volume":"59","author":"Bollig","year":"1996","journal-title":"Inf. Proc. lett."}],"container-title":["Integration"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167926002000470?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167926002000470?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T09:11:07Z","timestamp":1759137067000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167926002000470"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12]]},"references-count":43,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2002,12]]}},"alternative-id":["S0167926002000470"],"URL":"https:\/\/doi.org\/10.1016\/s0167-9260(02)00047-0","relation":{},"ISSN":["0167-9260"],"issn-type":[{"type":"print","value":"0167-9260"}],"subject":[],"published":{"date-parts":[[2002,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Minimization of Word-Level Decision Diagrams","name":"articletitle","label":"Article Title"},{"value":"Integration","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S0167-9260(02)00047-0","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Elsevier Science B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}