{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:24:33Z","timestamp":1759332273955,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2005,4,17]],"date-time":"2005-04-17T00:00:00Z","timestamp":1113696000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2005,4,17]]},"DOI":"10.1145\/1057661.1057725","type":"proceedings-article","created":{"date-parts":[[2005,8,3]],"date-time":"2005-08-03T08:31:47Z","timestamp":1123057907000},"page":"264-269","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Utilizing don't care states in SAT-based bounded sequential problems"],"prefix":"10.1145","author":[{"given":"Sean","family":"Safarpour","sequence":"first","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G\u00f6rschwin","family":"Fey","sequence":"additional","affiliation":[{"name":"Bremen University, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Veneris","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[{"name":"Bremen University, Bremen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,4,17]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"e_1_3_2_1_2_1","first-page":"898","volume-title":"Proc. of IEEE DATE","author":"Cabodi G.","year":"2003","unstructured":"G. Cabodi , S. Nocco , S. Quer , \"Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals\" , in Proc. of IEEE DATE , pp. 898 -- 203 , 2003 . G. Cabodi, S. Nocco, S. Quer, \"Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals\", in Proc. of IEEE DATE, pp. 898--203, 2003."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_1_4_1","volume-title":"Chap.3 and Chap. 7","author":"Devadas S.","year":"1994","unstructured":"S. Devadas , A. Ghosh , K. Keutzer , Logic Synthesis , Chap.3 and Chap. 7 , McGraw-Hill , 1994 . S. Devadas, A. Ghosh, K. Keutzer, Logic Synthesis, Chap.3 and Chap. 7, McGraw-Hill, 1994."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277169"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.776040"},{"key":"e_1_3_2_1_7_1","first-page":"206","volume-title":"Proc. of CAV","author":"Gupta A.","year":"2003","unstructured":"A. Gupta , M. Ganai , C. Wang , Z. Yang , P. Ashar , \"Abstraction and BDDs Complement SAT-Based BMC in DiVer\" , Proc. of CAV , pp. 206 -- 209 , 2003 . A. Gupta, M. Ganai, C. Wang, Z. Yang, P. Ashar, \"Abstraction and BDDs Complement SAT-Based BMC in DiVer\", Proc. of CAV, pp. 206--209, 2003."},{"key":"e_1_3_2_1_8_1","volume-title":"Chap. 8","author":"Hachtel G.","year":"2000","unstructured":"G. Hachtel and F. Somenzi , Logic Synthesis and Verification Algorithms , Chap. 8 , Kluwer Academic Publishers , 2000 . G. Hachtel and F. Somenzi, Logic Synthesis and Verification Algorithms, Chap. 8, Kluwer Academic Publishers, 2000."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.108614"},{"key":"e_1_3_2_1_10_1","first-page":"892","volume-title":"Proc. of IEEE DATE","author":"Lu F.","year":"2003","unstructured":"F. Lu , L.-C. Wang , K.-T. Cheng and R. Y.-Y. Huang , \" A Circuit SAT Solver with Signal Correlation Guided Learning ,\" in Proc. of IEEE DATE , pp. 892 -- 897 , 2003 . F. Lu, L.-C. Wang, K.-T. Cheng and R. Y.-Y. Huang, \"A Circuit SAT Solver with Signal Correlation Guided Learning,\" in Proc. of IEEE DATE, pp. 892--897, 2003."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/288548.289053"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277168"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/968878.969032"},{"key":"e_1_3_2_1_15_1","volume-title":"Public software","author":"Somenzi F.","year":"1997","unstructured":"F. Somenzi , \"CUDD : CU decision diagram package \", Public software , Colorado University , Boulder , 1997 . F. Somenzi, \"CUDD: CU decision diagram package\", Public software, Colorado University, Boulder, 1997."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"e_1_3_2_1_17_1","first-page":"145","volume-title":"Proc. of IEEE DATE","author":"Silva P.M.","year":"1999","unstructured":"J. P.M. Silva and T. Glass , \" Combinational Equivalence Checking using Satisfiability and Recursive Learning \", Proc. of IEEE DATE , pp. 145 -- 149 , 1999 . J.P.M. Silva and T. Glass, \"Combinational Equivalence Checking using Satisfiability and Recursive Learning\", Proc. of IEEE DATE, pp. 145--149, 1999."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.826552"}],"event":{"name":"GLSVLSI05: Great Lakes Symposium on VLSI 2005","sponsor":["ACM Association for Computing Machinery","SIGDA ACM Special Interest Group on Design Automation"],"location":"Chicago Illinois USA","acronym":"GLSVLSI05"},"container-title":["Proceedings of the 15th ACM Great Lakes symposium on VLSI"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1057661.1057725","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1057661.1057725","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:26:00Z","timestamp":1750281960000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1057661.1057725"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,4,17]]},"references-count":18,"alternative-id":["10.1145\/1057661.1057725","10.1145\/1057661"],"URL":"https:\/\/doi.org\/10.1145\/1057661.1057725","relation":{},"subject":[],"published":{"date-parts":[[2005,4,17]]},"assertion":[{"value":"2005-04-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}