{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T03:31:00Z","timestamp":1752982260172},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208518"},{"type":"electronic","value":"9783540246053"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24605-3_4","type":"book-chapter","created":{"date-parts":[[2010,7,29]],"date-time":"2010-07-29T04:50:35Z","timestamp":1280379035000},"page":"37-52","source":"Crossref","is-referenced-by-count":4,"title":["How Good Can a Resolution Based SAT-solver\u00a0Be?"],"prefix":"10.1007","author":[{"given":"Eugene","family":"Goldberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yakov","family":"Novikov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Bacchus, F.: Exploring the computational tradeoff of more reasoning and less searching. In: Fifth International Symposium on Theory and Applications of Satisfiability Testing, pp. 7\u201316 (2002)"},{"key":"4_CR2","unstructured":"Ben-Sasson, E., Impagliazzo, R., Wigderson, A.: Near optimal separation of Treelike and General resolution. In: SAT 2000: Third Workshop on the Satisfiability Problem (May 2000)"},{"key":"4_CR3","unstructured":"BerkMin web page, \n                  \n                    http:\/\/eigold.tripod.com\/BerkMin.html"},{"issue":"6","key":"4_CR4","doi-asserted-by":"publisher","first-page":"1939","DOI":"10.1137\/S0097539798353230","volume":"29","author":"M. Bonet","year":"2000","unstructured":"Bonet, M., Pitassi, T., Raz, R.: On interpolation and automatization for Frege Systems. SIAM Journal on Computing\u00a029(6), 1939\u20131967 (2000)","journal-title":"SIAM Journal on Computing"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Brand, D.: Verification of large synthesized designs. In: Proceedings of ICCAD 1993, pp. 534\u2013537 (1993)","DOI":"10.1109\/ICCAD.1993.580110"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT-solver. In: Design, Automation, and Test in Europe (DATE 2002), March 2002, pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"4_CR7","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci.\u00a039, 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT-solver. In: Proceedings of DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Razborov, A.: Resolution is not automatizable unless W[p] is tractable. In: Proceedings of FOCS (2001)","DOI":"10.1109\/SFCS.2001.959895"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Sentovich, E., et al.: Sequential circuit design using synthesis and optimization. In: Proceedings of ICCAD, October 1992, pp. 328\u2013333 (1992)","DOI":"10.1109\/ICCD.1992.276282"},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P.M. Silva","year":"1999","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions of Computers\u00a048, 506\u2013521 (1999)","journal-title":"IEEE Transactions of Computers"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivations in propositional calculus. Studies in Mathematics and Mathematical Logic, Part II, Consultants Bureau, New York\/London, 115\u2013125 (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"4_CR13","unstructured":"Zchaff web page, \n                  \n                    http:\/\/ee.princeton.edu\/~chaff\/zchaff.php"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: Proceedings of the International Conference on Automated Deduction, pp. 272\u2013275 (July 1997)","DOI":"10.1007\/3-540-63104-6_28"},{"key":"4_CR15","unstructured":"2clseq web page, \n                  \n                    http:\/\/www.cs.toronto.edu\/~fbacchus\/2clseq.html"},{"key":"4_CR16","unstructured":"http:\/\/www.cbl.ncsu.edu\/CBL_Docs\/lgs91.html"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24605-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T14:49:59Z","timestamp":1548427799000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24605-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208518","9783540246053"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24605-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}