{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T18:09:48Z","timestamp":1776881388816,"version":"3.51.2"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319630458","type":"print"},{"value":"9783319630465","type":"electronic"}],"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-63046-5_9","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"130-147","source":"Crossref","is-referenced-by-count":20,"title":["Short Proofs Without New Variables"],"prefix":"10.1007","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Kiesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Meth. Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Formal Meth. Syst. Des."},{"issue":"3","key":"9_CR2","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1016\/j.tcs.2008.03.013","volume":"404","author":"F Ivan\u010di\u0107","year":"2008","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. Theor. Comput. Sci. 404(3), 256\u2013274 (2008)","journal-title":"Theor. Comput. Sci."},{"issue":"C","key":"9_CR3","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/j.artint.2015.03.004","volume":"224","author":"B Konev","year":"2015","unstructured":"Konev, B., Lisitsa, A.: Computer-aided proof of Erd\u0151s discrepancy properties. Artif. Intell. 224(C), 103\u2013118 (2015)","journal-title":"Artif. Intell."},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_15"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"ND Wetzler","year":"2014","unstructured":"Wetzler, N.D., Heule, M.J.H., Hunt Jr., W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). doi: 10.1007\/978-3-319-09284-3_31"},{"key":"9_CR6","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). doi: 10.1007\/978-3-642-31365-3_28"},{"key":"9_CR7","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). doi: 10.1007\/978-3-319-40229-1_5"},{"key":"9_CR8","unstructured":"Kleine B\u00fcning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. IOS Press, pp. 339\u2013401 (2009)"},{"issue":"2","key":"9_CR9","first-page":"89","volume":"1","author":"S Weaver","year":"2006","unstructured":"Weaver, S., Franco, J.V., Schlipf, J.S.: Extending existential quantification in conjunctions of BDDs. JSAT 1(2), 89\u2013110 (2006)","journal-title":"JSAT"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Andersson, G., Bjesse, P., Cook, B., Hanna, Z.: A proof engine approach to solving combinational design automation problems. In: Proceedings of the 39th Annual Design Automation Conference (DAC 2002). ACM, pp. 725\u2013730 (2002)","DOI":"10.1145\/513918.514101"},{"key":"9_CR11","unstructured":"Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: Proceedings of the 5th International Conference on Principles of Knowledge Representation and Reasoning (KR 1996). Morgan Kaufmann, pp. 148\u2013159 (1996)"},{"key":"9_CR12","first-page":"115","volume":"2","author":"GS Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. Stud. Math. Math. Logic 2, 115\u2013125 (1968)","journal-title":"Stud. Math. Math. Logic"},{"key":"9_CR13","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. Theor. Comput. Sci. 39, 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR14","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). AAAI Press (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-39611-3_14","volume-title":"Hardware and Software: Verification and Testing","author":"N Manthey","year":"2013","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 102\u2013117. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39611-3_14"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-319-40970-2_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"J Devriendt","year":"2016","unstructured":"Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static symmetry breaking for SAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 104\u2013122. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_8"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Balyo, T., Heule, M.J.H., J\u00e4rvisalo, M.: SAT competition 2016: recent developments. In: Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI 2017). AAAI Press (2017, to appear)","DOI":"10.1609\/aaai.v31i1.10641"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of the Conference on Design, Automation and Test in Europe (DATE 2003). IEEE Computer Society, pp. 10886\u201310891 (2003)","DOI":"10.1109\/DATE.2003.1253718"},{"issue":"4","key":"9_CR19","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/s10472-012-9322-x","volume":"65","author":"A Gelder Van","year":"2012","unstructured":"Van Gelder, A.: Producing and verifying extremely large propositional refutations. Ann. Math. Artif. Intell. 65(4), 329\u2013372 (2012)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9_CR20","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 Appl. Math. 96\u201397, 149\u2013176 (1999)","journal-title":"Discrete Appl. Math."},{"issue":"4","key":"9_CR21","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1007\/s10817-011-9239-9","volume":"49","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.H.: Simulating circuit-level simplifications on CNF. J. Autom. Reasoning 49(4), 583\u2013619 (2012)","journal-title":"J. Autom. Reasoning"},{"issue":"4","key":"9_CR22","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":"9_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1007\/978-3-319-21401-6_40","volume-title":"Automated Deduction \u2013 CADE-25","author":"MJH Heule","year":"2015","unstructured":"Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Expressing symmetry breaking in DRAT proofs. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 591\u2013606. Springer, Cham (2015). doi: 10.1007\/978-3-319-21401-6_40"},{"issue":"4","key":"9_CR24","doi-asserted-by":"crossref","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A Urquhart","year":"1995","unstructured":"Urquhart, A.: The complexity of propositional proofs. Bull. Symbolic Logic 1(4), 425\u2013467 (1995)","journal-title":"Bull. Symbolic Logic"},{"issue":"18","key":"9_CR25","doi-asserted-by":"crossref","first-page":"1030","DOI":"10.1016\/j.ipl.2009.06.006","volume":"109","author":"J Nordstr\u00f6m","year":"2009","unstructured":"Nordstr\u00f6m, J.: A simplified way of proving trade-off results for resolution. Inf. Process. Lett. 109(18), 1030\u20131035 (2009)","journal-title":"Inf. Process. Lett."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,24]],"date-time":"2023-08-24T11:21:11Z","timestamp":1692876071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}