{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T07:21:46Z","timestamp":1777965706693,"version":"3.51.4"},"reference-count":37,"publisher":"Institution of Engineering and Technology (IET)","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IET Comput. Digit. Tech."],"published-print":{"date-parts":[[2008,5]]},"DOI":"10.1049\/iet-cdt:20060221","type":"journal-article","created":{"date-parts":[[2008,4,17]],"date-time":"2008-04-17T23:07:52Z","timestamp":1208473672000},"page":"214-229","source":"Crossref","is-referenced-by-count":13,"title":["Efficient, scalable hardware engine for Boolean satisfiability and unsatisfiable core extraction"],"prefix":"10.1049","volume":"2","author":[{"given":"K.","family":"Gulati","sequence":"first","affiliation":[{"name":"Department of ECE, Texas A and M University, College Station, TX 77843, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Waghmode","sequence":"additional","affiliation":[{"name":"Magma Design Automation, Inc., Santa Clara, CA 95054, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.P.","family":"Khatri","sequence":"additional","affiliation":[{"name":"Department of ECE, Texas A and M University, College Station, TX 77843, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"W.","family":"Shi","sequence":"additional","affiliation":[{"name":"Department of ECE, Texas A and M University, College Station, TX 77843, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"265","reference":[{"key":"10.1049\/iet-cdt:20060221_r1","first-page":"151","author":"Cook","year":"1971","journal-title":"Proc. 3rd ACM Symp. Theory of Computing"},{"key":"10.1049\/iet-cdt:20060221_r2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(88)90042-6"},{"key":"10.1049\/iet-cdt:20060221_r3","author":"Lynce","year":"2004","journal-title":"Int. Conf., Theory and Applications of Satisfiability Testing"},{"key":"10.1049\/iet-cdt:20060221_r4","doi-asserted-by":"crossref","unstructured":"Gu, J., Purdom, P., Franco, J., and Wah, B.: \u2018Algorithms for the satisfiability (SAT) problem: a survey\u2019, (American Mathematical Society 1997),35, DIMACS Series in Discrete Math. and Theoretical Computer Science, p. 19\u2013151","DOI":"10.1090\/dimacs\/035\/02"},{"key":"10.1049\/iet-cdt:20060221_r5","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1109\/ICCAD.1996.569607","author":"Silva","year":"1996","journal-title":"Proc. Int. Conf. Computer-Aided Design (ICCAD)"},{"key":"10.1049\/iet-cdt:20060221_r6","author":"Moskewicz","year":"2001","journal-title":"Proc. Design Automation Conf."},{"key":"10.1049\/iet-cdt:20060221_r7","first-page":"142","author":"Goldberg","year":"2002","journal-title":"Proc., Design, Automation and Test in Europe (DATE) Conf."},{"key":"10.1049\/iet-cdt:20060221_r8","first-page":"519","author":"Jin","year":"2004"},{"key":"10.1049\/iet-cdt:20060221_r9","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2004.102"},{"key":"10.1049\/iet-cdt:20060221_r10","author":"Kautz","year":"1992","journal-title":"Proc., 10th European Conf. Artificial Intelligence"},{"key":"10.1049\/iet-cdt:20060221_r11","author":"Nam","year":"1999","journal-title":"Proc. Int. Symp. FPGAs"},{"key":"10.1049\/iet-cdt:20060221_r12","author":"McMillan","year":"2003","journal-title":"Proc. Computer Aided Verification"},{"key":"10.1049\/iet-cdt:20060221_r13","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1109\/ISSS.2001.957949","author":"Zhao","year":"2001","journal-title":"Proc. Int. Symp. System Synthesis (ISSS)"},{"key":"10.1049\/iet-cdt:20060221_r14","first-page":"447","author":"Zhao","year":"2001","journal-title":"Proc. Int. Conf. Computer Design (ICCD)"},{"key":"10.1049\/iet-cdt:20060221_r15","first-page":"194","author":"Zhong","year":"1998","journal-title":"Proc. Design Automation Conf."},{"key":"10.1049\/iet-cdt:20060221_r16","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1109\/FPGA.1998.707896","author":"Zhong","year":"1998","journal-title":"Proc., IEEE Symp. FPGAs for Custom Computing Machines"},{"key":"10.1049\/iet-cdt:20060221_r17","first-page":"147","author":"Pagarani","year":"2000","journal-title":"Proc. IEEE Custom Integrated Circuits Conf. (CICC)"},{"key":"10.1049\/iet-cdt:20060221_r18","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1007\/3-540-63465-7_250","author":"Abramovici","year":"1997","journal-title":"Proc., Int. Workshop on Field Programmable Logic and Applications"},{"key":"10.1049\/iet-cdt:20060221_r19","doi-asserted-by":"publisher","DOI":"10.1109\/92.920826"},{"key":"10.1049\/iet-cdt:20060221_r20","first-page":"684","author":"Abramovici","year":"1999","journal-title":"Proc. Design Automation Conf. (DAC)"},{"key":"10.1049\/iet-cdt:20060221_r21","author":"de Souza","year":"2001","journal-title":"IEEE Symp. FPGAs for Custom Computing Machines"},{"key":"10.1049\/iet-cdt:20060221_r22","author":"Reis","year":"2002","journal-title":"Proc. 10th Annual IEEE Symp. Field-Programmable Custom Computing Machines"},{"key":"10.1049\/iet-cdt:20060221_r23","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/S0166-218X(00)00245-6","volume":"107","author":"Buning","year":"2000","ISSN":"https:\/\/2.zoppoz.workers.dev:443\/https\/id.crossref.org\/issn\/0166-218X","issn-type":"print"},{"key":"10.1049\/iet-cdt:20060221_r24","first-page":"229","volume":"23","author":"Davydov","year":"1998"},{"key":"10.1049\/iet-cdt:20060221_r25","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/S0304-3975(01)00337-1","volume":"289","author":"Fleischner","year":"2002","ISSN":"https:\/\/2.zoppoz.workers.dev:443\/https\/id.crossref.org\/issn\/0304-3975","issn-type":"print"},{"key":"10.1049\/iet-cdt:20060221_r26","author":"Bruni","year":"2001","journal-title":"In LICS Workshop Theory and Applications of Satisfiability Testing"},{"key":"10.1049\/iet-cdt:20060221_r27","first-page":"10886","author":"Goldberg","year":"2003","journal-title":"Proc., Design and Test in Europe Conf."},{"key":"10.1049\/iet-cdt:20060221_r28","author":"Oh","year":"2004","journal-title":"Proc., Design Automation Conf."},{"key":"10.1049\/iet-cdt:20060221_r29","author":"Zhang","year":"2003","journal-title":"Proc., Design and Test in Europe Conf."},{"key":"10.1049\/iet-cdt:20060221_r30","author":"Huang","year":"2005","journal-title":"Proc. 10th Asia and South Pacific Design Automation Conf."},{"key":"10.1049\/iet-cdt:20060221_r31","author":"Waghmode","year":"2006","journal-title":"Proc. Int. Conf. Computer Design (ICCD)"},{"key":"10.1049\/iet-cdt:20060221_r32","unstructured":"DIMACS challenge \u2013 satisfiability. Available at: ftp:\/\/dimacs.rutgers.edu\/pub\/challenge\/satisfiability\/. The DIMACS ftp site"},{"key":"10.1049\/iet-cdt:20060221_r33","unstructured":"Karypis, G., and Kumar, V.: \u2018A software package for partitioning unstructured graphs, partitioning meshes and computing fill-reducing orderings of sparse matrices.\u2019 https:\/\/2.zoppoz.workers.dev:443\/http\/www-users.cs.umn.edu\/karypis\/metis, September 1998"},{"key":"10.1049\/iet-cdt:20060221_r34","unstructured":"The SAT'04 Competition, available at: \u2018https:\/\/2.zoppoz.workers.dev:443\/http\/www.lri.fr\/~simon\/contest04\/results\/\u2019"},{"key":"10.1049\/iet-cdt:20060221_r35","unstructured":"Nagel, L., \u2018Spice: a computer program to simulate computer circuits,\u2019 inUniversity of California, Berkeley UCB\/ERL Memo M520, May 1995"},{"key":"10.1049\/iet-cdt:20060221_r36","unstructured":"Een N., S\u00f6rensson N.: The MiniSAT Page. Available at: \u2018https:\/\/2.zoppoz.workers.dev:443\/http\/www.cs.chalmers.se\/cs\/research\/formalmethods\/minisat\/main.html\u2019."},{"key":"10.1049\/iet-cdt:20060221_r37","first-page":"331","author":"Zheng","year":"2002","journal-title":"ACSC '02: Proc. 25th Australasian Conf. Computer science"}],"container-title":["IET Computers & Digital Techniques"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/digital-library.theiet.org\/content\/journals\/10.1049\/iet-cdt_20060221?crawler=true&mimetype=application\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T14:32:59Z","timestamp":1731421979000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/digital-library.theiet.org\/doi\/10.1049\/iet-cdt%3A20060221"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,5]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,5]]}},"alternative-id":["10.1049\/iet-cdt:20060221"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1049\/iet-cdt:20060221","relation":{},"ISSN":["1751-8601","1751-861X"],"issn-type":[{"value":"1751-8601","type":"print"},{"value":"1751-861X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,5]]}}}