{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:43:36Z","timestamp":1750308216258,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":20,"publisher":"ACM","license":[{"start":{"date-parts":[[2004,6,7]],"date-time":"2004-06-07T00:00:00Z","timestamp":1086566400000},"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":[[2004,6,7]]},"DOI":"10.1145\/996566.996628","type":"proceedings-article","created":{"date-parts":[[2004,7,20]],"date-time":"2004-07-20T15:55:38Z","timestamp":1090338938000},"page":"212-217","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["An efficient finite-domain constraint solver for circuits"],"prefix":"10.1145","author":[{"given":"G.","family":"Parthasarathy","sequence":"first","affiliation":[{"name":"University of California, Santa Barbara, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M. K.","family":"Iyer","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K.-T.","family":"Cheng","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L.-C.","family":"Wang","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2004,6,7]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Digital Systems Testing and Testable Design, 1$^st$ ed","author":"Abramovici M.","year":"1990","unstructured":"Abramovici , M. , Breuer , M. A. , and Friedman , A. D . Digital Systems Testing and Testable Design, 1$^st$ ed . Computer Science Press , 1990 . Abramovici, M., Breuer, M. A., and Friedman, A. D. Digital Systems Testing and Testable Design, 1$^st$ ed. Computer Science Press, 1990."},{"key":"e_1_3_2_1_2_1","series-title":"LNCS","first-page":"187","volume-title":"Proc. of FMCAD","author":"Barett D. L.","year":"1996","unstructured":"C. Barett , D. L. Dill , and J. Levitt . Validity Checking for Combinations of Theories with Equality . In Proc. of FMCAD November 1996 , M. Srivas and A. Camilleri , Eds ., vol. 1166 of LNCS , pp. 187 -- 201 . C. Barett, D. L. Dill, and J. Levitt. Validity Checking for Combinations of Theories with Equality. In Proc. of FMCAD November 1996, M. Srivas and A. Camilleri, Eds., vol. 1166 of LNCS, pp. 187--201."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1145\/277044.277186"},{"key":"e_1_3_2_1_4_1","first-page":"741","volume-title":"Proc. of 15th VLSI Design Conf. (Jan.","author":"Brinkmann R.","year":"2001","unstructured":"Brinkmann , R. , and Dreschler , R . RTL-Datapath Verification using Integer Linear Programming . In Proc. of 15th VLSI Design Conf. (Jan. 2001 ), pp. 741 -- 746 . Brinkmann, R., and Dreschler, R. RTL-Datapath Verification using Integer Linear Programming. In Proc. of 15th VLSI Design Conf. (Jan. 2001), pp. 741--746."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_5_1","DOI":"10.1109\/TC.1986.1676819"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.1016\/0097-3165(73)90004-6"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.1145\/368273.368557"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1145\/321033.321034"},{"key":"e_1_3_2_1_9_1","volume-title":"Germany","author":"Drechsler B.","year":"1995","unstructured":"R. Drechsler , B. Becker , and S. Ruppertz . K*BMDs: a new data structure for verification. In IFI WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods Frankfurt , Germany , October 1995 . R. Drechsler, B. Becker, and S. Ruppertz. K*BMDs: a new data structure for verification. In IFI WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods Frankfurt, Germany, October 1995."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_10_1","DOI":"10.1023\/A:1022323717928"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.1145\/337292.337333"},{"key":"e_1_3_2_1_12_1","first-page":"259","volume-title":"M. A. RACE: A Word-Level ATPG-Based Constraints Solver System For Smart Random Simulation In Proc. of the ITC","author":"Iyer","year":"2003","unstructured":"Iyer , M. A. RACE: A Word-Level ATPG-Based Constraints Solver System For Smart Random Simulation In Proc. of the ITC ( 2003 ), pp. 259 -- 266 . Iyer, M. A. RACE: A Word-Level ATPG-Based Constraints Solver System For Smart Random Simulation In Proc. of the ITC (2003), pp. 259--266."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_13_1","DOI":"10.5555\/996070.1009909"},{"key":"e_1_3_2_1_14_1","volume-title":"et. al","author":"Kelly V.","year":"1996","unstructured":"W. Kelly , V. Maslow , W. Pugh , et. al . The Omega Calculator and Library v1.1.0. Tech. rep., Dept. of CS, University of Maryland, College Park , November 1996 . W. Kelly, V. Maslow, W. Pugh, et. al. The Omega Calculator and Library v1.1.0. Tech. rep., Dept. of CS, University of Maryland, College Park, November 1996."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_15_1","DOI":"10.5555\/996070.1009910"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_16_1","DOI":"10.1109\/12.769433"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_17_1","DOI":"10.1145\/378239.379017"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_18_1","DOI":"10.1016\/0004-3702(77)90029-7"},{"volume-title":"O. On Solving Presburger and Linear Arithmetic with SAT. In Proc. of FMCAD(2002)","author":"Strichman","unstructured":"Strichman , O. On Solving Presburger and Linear Arithmetic with SAT. In Proc. of FMCAD(2002) . Strichman, O. On Solving Presburger and Linear Arithmetic with SAT. In Proc. of FMCAD(2002).","key":"e_1_3_2_1_19_1"},{"key":"e_1_3_2_1_20_1","volume-title":"Proc. of ICCAD (Nov.","author":"Zhang L.","year":"2002","unstructured":"Zhang , L. , Madigan , C. , Moskewicz , M. , and Malik , S . Efficient Conflict Driven Learning in a Boolean Satisfiability Solver . In Proc. of ICCAD (Nov. 2002 ). Zhang, L., Madigan, C., Moskewicz, M., and Malik, S. Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. In Proc. of ICCAD (Nov. 2002)."}],"event":{"sponsor":["ACM Association for Computing Machinery","SIGDA ACM Special Interest Group on Design Automation"],"acronym":"DAC04","name":"DAC04: The 41st Annual Design Automation Conference 2004","location":"San Diego CA USA"},"container-title":["Proceedings of the 41st annual Design Automation Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/996566.996628","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/996566.996628","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:31:11Z","timestamp":1750264271000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/996566.996628"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,6,7]]},"references-count":20,"alternative-id":["10.1145\/996566.996628","10.1145\/996566"],"URL":"https:\/\/doi.org\/10.1145\/996566.996628","relation":{},"subject":[],"published":{"date-parts":[[2004,6,7]]},"assertion":[{"value":"2004-06-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}