{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:58:22Z","timestamp":1725533902787},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027765"},{"type":"electronic","value":"9783642027772"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02777-2_16","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T06:58:18Z","timestamp":1245999498000},"page":"147-160","source":"Crossref","is-referenced-by-count":5,"title":["Boundary Points and Resolution"],"prefix":"10.1007","author":[{"given":"Eugene","family":"Goldberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"16_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":"16_CR2","doi-asserted-by":"crossref","unstructured":"Babic, D., Bihgham, J., Hu, A.: Efficient SAT solving: beyond supercubes. In: DAC 2005, pp. 744\u2013749 (2005)","DOI":"10.1109\/DAC.2005.193910"},{"key":"16_CR3","first-page":"19","volume-title":"ch. 2","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) ch. 2, vol.\u00a01, pp. 19\u201399. Elsevier Science Publ., Amsterdam (2001)"},{"key":"16_CR4","first-page":"75","volume":"4","author":"A. Bierre","year":"2008","unstructured":"Bierre, A.: PicoSAT essentials. JSAT\u00a04, 75\u201397 (2008)","journal-title":"JSAT"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Bierre, A., Cimatti, A., Clarke, F.M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: DAC 1999, pp. 317\u2013320 (1999)","DOI":"10.21236\/ADA360973"},{"issue":"6","key":"16_CR6","doi-asserted-by":"publisher","first-page":"1939","DOI":"10.1137\/S0097539798353230","volume":"29","author":"M.L. Bonet","year":"2000","unstructured":"Bonet, M.L., Pitassi, T., Raz, R.: On Interpolation and Automatization for Frege Systems. SIAM J. Comput.\u00a029(6), 1939\u20131967 (2000)","journal-title":"SIAM J. Comput."},{"issue":"7","key":"16_CR7","doi-asserted-by":"publisher","first-page":"1113","DOI":"10.1109\/TCAD.2004.829807","volume":"23","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Gupta, A., Strichman, O.: SAT-based counterexample-guided abstraction refinement. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a023(7), 1113\u20131123 (2004)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"16_CR8","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Longemann, G., Loveland, D.: A Machine program for theorem proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Goldberg, E.: On Bridging Simulation and Formal Verification. In: VMCAI-2008, pp. 127\u2013141 (2008)","DOI":"10.1007\/978-3-540-78163-9_14"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-540-79719-7_11","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"E. Goldberg","year":"2008","unstructured":"Goldberg, E.: A Decision-Making Procedure for Resolution-Based SAT-Solvers. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 119\u2013132. Springer, Heidelberg (2008)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Prasad, M., Brayton, R.: Using Problem Symmetry in Search Based Satisfiability Algorithms. In: DATE 2002, pp. 134\u2013141 (2002)","DOI":"10.1109\/DATE.2002.998261"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: a Fast and Robust SAT-Solver. In: DATE 2002, pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"issue":"5","key":"16_CR14","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1023\/A:1015803927637","volume":"28","author":"E. Goldberg","year":"2002","unstructured":"Goldberg, E.: Proving unsatisfiability of CNFs locally. J. Autom. Reasoning\u00a028(5), 417\u2013434 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K. McMillan","year":"2003","unstructured":"McMillan, K.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC 2001, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"16_CR17","unstructured":"Nadel, A.: Backtrack search algorithms for propositional logic satisfiability: review and innovations. Master Thesis, the Hebrew University (2002)"},{"key":"16_CR18","unstructured":"The siege sat-solver, http:\/\/www.cs.sfu.ca\/~cl\/software\/siege\/"},{"key":"16_CR19","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. Silva","year":"1999","unstructured":"Silva, J., Sakallah, K.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions of Computers\u00a048, 506\u2013521 (1999)","journal-title":"IEEE Transactions of Computers"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/3-540-63104-6_28","volume-title":"Automated Deduction - CADE-14","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T02:57:59Z","timestamp":1558407479000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}