{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T15:10:19Z","timestamp":1731424219382,"version":"3.28.0"},"reference-count":28,"publisher":"Institution of Engineering and Technology (IET)","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IET Comput. Digit. Tech."],"published-print":{"date-parts":[[2008,1,9]]},"DOI":"10.1049\/iet-cdt:20060233","type":"journal-article","created":{"date-parts":[[2008,1,12]],"date-time":"2008-01-12T23:46:37Z","timestamp":1200181597000},"page":"30-39","source":"Crossref","is-referenced-by-count":3,"title":["Decision heuristic for Davis Putnam, Loveland and Logemann algorithm satisfiability solving based on cube subtraction"],"prefix":"10.1049","volume":"2","author":[{"given":"R.","family":"Zuim","sequence":"first","affiliation":[{"name":"Department of Computer Science, UFMG and Pucminas, Brazil"}]},{"given":"J.T.","family":"de Sousa","sequence":"additional","affiliation":[{"name":"INESC-ID Lisboa, TU-Lisbon, Portugal"}]},{"given":"C.N.","family":"Coelho","sequence":"additional","affiliation":[{"name":"Department of Computer Science, UFMG, Brazil"}]}],"member":"265","reference":[{"key":"10.1049\/iet-cdt:20060233_r1","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1109\/DAC.2001.935509","author":"Velev","year":"2001","journal-title":"Proc. 38th Design Automation Conf. (DAC01)"},{"key":"10.1049\/iet-cdt:20060233_r2","first-page":"193","author":"Biere","year":"1999","journal-title":"Proc. Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS99)"},{"key":"10.1049\/iet-cdt:20060233_r3","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","author":"McMillan","year":"2002","journal-title":"Proc. 14th Int. Conf. Computer Aided Verification (CAV2002)"},{"doi-asserted-by":"publisher","key":"10.1049\/iet-cdt:20060233_r4","DOI":"10.1109\/43.536723"},{"unstructured":"SAT contest URL (access: dez\/2006), available at: http:\/\/www.satcompetition.org\/","key":"10.1049\/iet-cdt:20060233_r5"},{"key":"10.1049\/iet-cdt:20060233_r6","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"Davis","year":"1962","ISSN":"http:\/\/id.crossref.org\/issn\/0001-0782","issn-type":"print"},{"key":"10.1049\/iet-cdt:20060233_r7","doi-asserted-by":"crossref","first-page":"530","DOI":"10.1145\/378239.379017","author":"Moskewicz","year":"2001","journal-title":"Proc. 38th Design Automation Conf. (DAC01)"},{"key":"10.1049\/iet-cdt:20060233_r8","first-page":"p. 0142","author":"Novikov","year":"2002","journal-title":"Design, Automation and Test in Europe (DATE02)"},{"key":"10.1049\/iet-cdt:20060233_r9","doi-asserted-by":"crossref","first-page":"743","DOI":"10.1109\/DAC.2002.1012721","author":"Pilarski","year":"2002","journal-title":"Proc. 39th Design Automation Conf. (DAC02)"},{"key":"10.1049\/iet-cdt:20060233_r10","first-page":"272","author":"Zhang","year":"1997","journal-title":"Proc. Int. Conf. Automated Deduction (CADE-97)"},{"key":"10.1049\/iet-cdt:20060233_r11","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"Beame","year":"2004","ISSN":"http:\/\/id.crossref.org\/issn\/1076-9757","issn-type":"print"},{"unstructured":"\u2018Determinization of resolution by an algorithm operating on complete assignments\u2019, Technical Report, CDNL-TR-2006-0110, 2006","key":"10.1049\/iet-cdt:20060233_r12"},{"year":"2005","author":"Dershowitz","journal-title":"Proc. 8th Int. Conf. Theory and Applications of Satisfiability Testing (SAT05)","key":"10.1049\/iet-cdt:20060233_r13"},{"key":"10.1049\/iet-cdt:20060233_r14","first-page":"33","author":"Zuim","year":"2006","journal-title":"Proc. 7th IEEE Latin America Test Workshop LATW06"},{"key":"10.1049\/iet-cdt:20060233_r15","volume":"28","author":"Hong","year":"1979","ISSN":"http:\/\/id.crossref.org\/issn\/0018-9340","issn-type":"print"},{"key":"10.1049\/iet-cdt:20060233_r16","volume":"28","author":"Smith","year":"1979","ISSN":"http:\/\/id.crossref.org\/issn\/0018-9340","issn-type":"print"},{"key":"10.1049\/iet-cdt:20060233_r17","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1109\/TVLSI.2004.825859","volume":"12","author":"Skliarova","year":"2004","ISSN":"http:\/\/id.crossref.org\/issn\/1063-8210","issn-type":"print"},{"key":"10.1049\/iet-cdt:20060233_r18","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1109\/VLSISOC.2006.313213","author":"Zuim","year":"2006","journal-title":"Proc. 14th IFIP WG 10.5 Int. Conf. Very Large Scale Integration and System-on-chip, VLSI-SOC'2006"},{"key":"10.1049\/iet-cdt:20060233_r19","first-page":"220","author":"Marques-Silva","year":"1997","journal-title":"Proc. ACM\/IEEE Int. Conf. Computer-Aided Design"},{"key":"10.1049\/iet-cdt:20060233_r20","first-page":"279","author":"Zhang","year":"2001","journal-title":"Proc. IEEE\/ACM Int. Conf. Computer Aided Design (ICCAD01)"},{"unstructured":"URL(access: dez\/2006), available at: http:\/\/www.princeton.edu\/~chaff\/zchaff.html","key":"10.1049\/iet-cdt:20060233_r21"},{"key":"10.1049\/iet-cdt:20060233_r22","first-page":"502","author":"Ee\u0301n","year":"2003","journal-title":"Proc. Sixth Int. Conf. Theory and Applications of Satisfiability Testing (SAT2003) LNCS 2919"},{"unstructured":"URL (access: dez\/2006), available at: http:\/\/www.haifa.il.ibm.com\/projects\/verification\/RB_Homepage\/bmcbenchmarks.html","key":"10.1049\/iet-cdt:20060233_r23"},{"key":"10.1049\/iet-cdt:20060233_r24","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/11499107_25","author":"Zarpas","year":"2005","journal-title":"Proc. 8th Int. Conf. Theory and Applications of Satisfiability Testing (SAT05)"},{"unstructured":"URL (access: dez\/2006), available at: http:\/\/www.miroslav-velev.com\/sat_benchmarks.html","key":"10.1049\/iet-cdt:20060233_r25"},{"unstructured":"URL (access: dez\/2006), available at: http:\/\/www.satlib.org\/","key":"10.1049\/iet-cdt:20060233_r26"},{"unstructured":"Minisat2 download URL (access: dez\/2006), available at: http:\\\\www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\\MiniSat.html","key":"10.1049\/iet-cdt:20060233_r27"},{"year":"2004","author":"Lynce","journal-title":"Proc. 7th Int. Conf. Theory and Applications of Satisfiability Testing (SAT'04)","key":"10.1049\/iet-cdt:20060233_r28"}],"container-title":["IET Computers & Digital Techniques"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/digital-library.theiet.org\/content\/journals\/10.1049\/iet-cdt_20060233?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:31:03Z","timestamp":1731421863000},"score":1,"resource":{"primary":{"URL":"http:\/\/digital-library.theiet.org\/doi\/10.1049\/iet-cdt%3A20060233"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1,9]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,1,9]]}},"alternative-id":["10.1049\/iet-cdt:20060233"],"URL":"https:\/\/doi.org\/10.1049\/iet-cdt:20060233","relation":{},"ISSN":["1751-8601","1751-861X"],"issn-type":[{"type":"print","value":"1751-8601"},{"type":"electronic","value":"1751-861X"}],"subject":[],"published":{"date-parts":[[2008,1,9]]}}}