{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T21:08:32Z","timestamp":1725916112954},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319703886"},{"type":"electronic","value":"9783319703893"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-70389-3_12","type":"book-chapter","created":{"date-parts":[[2017,11,11]],"date-time":"2017-11-11T14:42:30Z","timestamp":1510411350000},"page":"179-194","source":"Crossref","is-referenced-by-count":14,"title":["PRuning Through Satisfaction"],"prefix":"10.1007","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"Kiesl","sequence":"additional","affiliation":[]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,11,12]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning SAT solvers. In: Proceedings of the 24th AAAI Conference on Artificial Intelligence (AAAI 2010), pp. 15\u201320. AAAI Press (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"12_CR2","unstructured":"Biere, A.: Splatz, lingeling, plingeling, treengeling, YalSAT entering the SAT Competition 2016. In: Proceedings of SAT competition 2016 \u2013 Solver and Benchmark Descriptions. Dep. of Computer Science Series of Publications B, vol. B-2016-1, pp. 44\u201345. University of Helsinki (2016)"},{"issue":"4","key":"12_CR3","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1145\/1008335.1008338","volume":"8","author":"SA Cook","year":"1976","unstructured":"Cook, S.A.: A short proof of the pigeon hole principle using extended resolution. SIGACT News 8(4), 28\u201332 (1976)","journal-title":"SIGACT News"},{"key":"12_CR4","doi-asserted-by":"crossref","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. Theoretical Computer Science 39, 297\u2013308 (1985)","journal-title":"Theoretical Computer Science"},{"key":"12_CR5","unstructured":"Heule, M.J.H., Biere, A.: Proofs for satisfiability problems. In: All about Proofs, Proofs for All (APPA), Math. Logic and Foundations, vol. 55. College Pub (2015)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-63046-5_9","volume-title":"Automated Deduction \u2013 CADE 26","author":"MJH Heule","year":"2017","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 130\u2013147. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_9"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_28"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-319-40229-1_5","volume-title":"Automated Reasoning","author":"B Kiesl","year":"2016","unstructured":"Kiesl, B., Seidl, M., Tompits, H., Biere, A.: Super-blocked clauses. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 45\u201361. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_5"},{"key":"12_CR9","unstructured":"Kleine B\u00fcning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Handbook of Satisfiability, pp. 339\u2013401. IOS Press (2009)"},{"key":"12_CR10","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics 96\u201397, 149\u2013176 (1999)","journal-title":"Discrete Applied Mathematics"},{"issue":"5","key":"12_CR11","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques Silva","year":"1999","unstructured":"Marques Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Computers"},{"issue":"3","key":"12_CR12","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0166-218X(85)90050-2","volume":"10","author":"B Monien","year":"1985","unstructured":"Monien, B., Speckenmeyer, E.: Solving satisfiability in less than $$2^n$$ steps. Discrete Applied Mathematics 10(3), 287\u2013295 (1985)","journal-title":"Discrete Applied Mathematics"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"issue":"3","key":"12_CR14","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/2815493.2815497","volume":"2","author":"J Nordstr\u00f6m","year":"2015","unstructured":"Nordstr\u00f6m, J.: On the interplay between proof complexity and SAT solving. SIGLOG News 2(3), 19\u201344 (2015)","journal-title":"SIGLOG News"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"C Sinz","year":"2005","unstructured":"Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827\u2013831. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11564751_73"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/11753728_60","volume-title":"Computer Science \u2013 Theory and Applications","author":"C Sinz","year":"2006","unstructured":"Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 600\u2013611. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11753728_60"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-02777-2_23","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"N S\u00f6rensson","year":"2009","unstructured":"S\u00f6rensson, N., Biere, A.: Minimizing learned clauses. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 237\u2013243. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_23"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning: 2: Classical Papers on Computational Logic 1967\u20131970, pp. 466\u2013483. Springer, Heidelberg (1983)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"12_CR19","unstructured":"Urquhart, A.: The complexity of propositional proofs. In: Current Trends in Theoretical Computer Science, pp. 332\u2013342. World Scientific (2001)"}],"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-319-70389-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,28]],"date-time":"2023-08-28T11:03:41Z","timestamp":1693220621000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70389-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319703886","9783319703893"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70389-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}