{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:22:49Z","timestamp":1742912569898,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642195822"},{"type":"electronic","value":"9783642195839"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-19583-9_12","type":"book-chapter","created":{"date-parts":[[2011,3,9]],"date-time":"2011-03-09T04:16:56Z","timestamp":1299644216000},"page":"93-111","source":"Crossref","is-referenced-by-count":1,"title":["SAT-Solving Based on Boundary Point Elimination"],"prefix":"10.1007","author":[{"given":"Eugene","family":"Goldberg","sequence":"first","affiliation":[]},{"given":"Panagiotis","family":"Manolios","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"12_CR1","doi-asserted-by":"publisher","first-page":"1347","DOI":"10.1137\/06066850X","volume":"38","author":"M. Alekhnovich","year":"2008","unstructured":"Alekhnovich, M., Razborov, A.: Resolution is not automatizable unless w[p] is tractable. SIAM J. Comput.\u00a038(4), 1347\u20131363 (2008)","journal-title":"SIAM J. Comput."},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I ch. 2, pp. 19\u201399. North-Holland, Amsterdam (2001)"},{"issue":"8","key":"12_CR3","doi-asserted-by":"publisher","first-page":"1059","DOI":"10.1109\/43.85742","volume":"10","author":"L. Berman","year":"1991","unstructured":"Berman, L.: Circuit width, register allocation, and ordered binary decision diagrams. IEEE Trans. on CAD of Integr. Circ. and Syst.\u00a010(8), 1059\u20131066 (1991)","journal-title":"IEEE Trans. on CAD of Integr. Circ. and Syst."},{"issue":"2-4","key":"12_CR4","first-page":"75","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: Picosat essentials. JSAT\u00a04(2-4), 75\u201397 (2008)","journal-title":"JSAT"},{"issue":"7","key":"12_CR5","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"issue":"3","key":"12_CR6","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Dechter, R., Rish, I.: Directional resolution: The davis-putnam procedure, revisited. In: KR, pp. 134\u2013145 (1994)","DOI":"10.1016\/B978-1-4832-1452-8.50109-3"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-02777-2_16","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"E. Goldberg","year":"2009","unstructured":"Goldberg, E.: Boundary points and resolution. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 147\u2013160. Springer, Heidelberg (2009)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"654","DOI":"10.1007\/978-3-642-04244-7_51","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"K. Pipatsrisawat","year":"2009","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers with restarts. In: Gent, I.P. (ed.) CP 2009. LNCS, vol.\u00a05732, pp. 654\u2013668. Springer, Heidelberg (2009)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Sakallah, K.: Grasp\u2014a new search algorithm for satisfiability. In: ICCAD 1996, Washington, DC, USA, pp. 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: DAC 2001, New York, NY, USA, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"12_CR12","unstructured":"Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: IJCAI, pp. 1173\u20131178 (2003)"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: ICCAD, pp. 442\u2013449 (2002)","DOI":"10.1145\/774572.774637"},{"key":"12_CR14","unstructured":"http:\/\/eigold.tripod.com\/benchmarks\/narrow_formulas.tar.gz"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19583-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,3]],"date-time":"2025-03-03T22:06:44Z","timestamp":1741039604000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19583-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642195822","9783642195839"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19583-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}