{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:58Z","timestamp":1776333538230,"version":"3.51.2"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,2,22]],"date-time":"2019-02-22T00:00:00Z","timestamp":1550793600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,2,22]],"date-time":"2019-02-22T00:00:00Z","timestamp":1550793600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["W1255-N23"],"award-info":[{"award-number":["W1255-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1526760"],"award-info":[{"award-number":["CCF-1526760"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,3]]},"DOI":"10.1007\/s10817-019-09516-0","type":"journal-article","created":{"date-parts":[[2019,2,22]],"date-time":"2019-02-22T14:15:14Z","timestamp":1550844914000},"page":"533-554","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Strong Extension-Free Proof Systems"],"prefix":"10.1007","volume":"64","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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7170-9242","authenticated-orcid":false,"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,2,22]]},"reference":[{"key":"9516_CR1","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\u00a02002), pp. 725\u2013730. ACM (2002)","DOI":"10.1145\/513918.514101"},{"key":"9516_CR2","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\u00a02010). AAAI Press (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"9516_CR3","doi-asserted-by":"crossref","unstructured":"Balyo, T., Heule, M.J.H., J\u00e4rvisalo, M.: SAT competition 2016: recent developments. To appear in: Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI\u00a02017). AAAI Press (2017)","DOI":"10.1609\/aaai.v31i1.10641"},{"issue":"1","key":"9516_CR4","doi-asserted-by":"publisher","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. Form. Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Form. Methods Syst. Des."},{"issue":"4","key":"9516_CR5","doi-asserted-by":"publisher","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":"9516_CR6","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\u00a01996), pp. 148\u2013159. Morgan Kaufmann (1996)"},{"key":"9516_CR7","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":"Jo Devriendt","year":"2016","unstructured":"Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static symmetry breaking for SAT. In: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02016). LNCS, vol. 9710, pp. 104\u2013122. Springer, Cham (2016)"},{"key":"9516_CR8","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\u00a02003), pp. 10,886\u201310,891. IEEE Computer Society (2003)"},{"key":"9516_CR9","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. 39, 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"9516_CR10","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H.: Schur number five. In: Proceedings of the 32nd AAAI Conference on Artificial Intelligence (AAAI 2018), pp. 6598\u20136606. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.12209"},{"key":"9516_CR11","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-319-89963-3_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Marijn J. H. Heule","year":"2018","unstructured":"Heule, M.J.H., Biere, A.: What a difference a variable makes. In: Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u00a02018). LNCS, vol. 10806, pp. 75\u201392 . Springer, Cham (2018)"},{"key":"9516_CR12","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1007\/978-3-319-21401-6_40","volume-title":"Automated Deduction - CADE-25","author":"Marijn J. H. Heule","year":"2015","unstructured":"Heule, M.J.H., Hunt\u00a0Jr, W.A., Wetzler, N.D.: Expressing symmetry breaking in DRAT proofs. In: Proceedings of the 25th International Conference on Automated Deduction (CADE-25). LNCS, vol. 9195, pp. 591\u2013606. Springer, Cham (2015)"},{"key":"9516_CR13","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":"Marijn J. H. 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: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02016). LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016)"},{"key":"9516_CR14","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-63046-5_9","volume-title":"Automated Deduction \u2013 CADE 26","author":"Marijn J. H. Heule","year":"2017","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26). LNCS, vol. 10395, pp. 130\u2013147. Springer, Cham (2017a)"},{"key":"9516_CR15","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-319-70389-3_12","volume-title":"Hardware and Software: Verification and Testing","author":"Marijn J. H. Heule","year":"2017","unstructured":"Heule, M.J.H., Kiesl, B., Seidl, M., Biere, A.: PRuning through satisfaction. In: Proceedings of the 13th Haifa Verification Conference (HVC 2017). LNCS, vol. 10629, pp. 179\u2013194. Springer, Cham (2017b)"},{"issue":"3","key":"9516_CR16","doi-asserted-by":"publisher","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":"4","key":"9516_CR17","doi-asserted-by":"publisher","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. Reason. 49(4), 583\u2013619 (2012a)","journal-title":"J. Autom. Reason."},{"key":"9516_CR18","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"Matti J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR\u00a02012). LNCS, vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012b)"},{"key":"9516_CR19","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-319-40229-1_5","volume-title":"Automated Reasoning","author":"Benjamin Kiesl","year":"2016","unstructured":"Kiesl, B., Seidl, M., Tompits, H., Biere, A.: Super-blocked clauses. In: Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR\u00a02016). LNCS, vol. 9706, pp. 45\u201361. Springer, Cham (2016)"},{"key":"9516_CR20","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/978-3-319-94205-6_34","volume-title":"Automated Reasoning","author":"Benjamin Kiesl","year":"2018","unstructured":"Kiesl, B., Rebola-Pardo, A., Heule, M.J.H.: Extended resolution simulates DRAT. In: Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2018). LNCS, vol. 10900, pp. 516\u2013531. Springer, Cham (2018)"},{"issue":"C","key":"9516_CR21","doi-asserted-by":"publisher","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":"9516_CR22","doi-asserted-by":"publisher","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."},{"key":"9516_CR23","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":"Norbert Manthey","year":"2013","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Proceedings of the 8th International Haifa Verification Conference (HVC\u00a02012). LNCS, vol. 7857. Springer, Heidelberg (2013)"},{"issue":"3","key":"9516_CR24","doi-asserted-by":"publisher","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 Appl. Math. 10(3), 287\u2013295 (1985)","journal-title":"Discrete Appl. Math."},{"issue":"18","key":"9516_CR25","doi-asserted-by":"publisher","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."},{"key":"9516_CR26","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. Log. 2, 115\u2013125 (1968)","journal-title":"Stud. Math. Math. Log."},{"issue":"4","key":"9516_CR27","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A Urquhart","year":"1995","unstructured":"Urquhart, A.: The complexity of propositional proofs. Bull. Symb. Log. 1(4), 425\u2013467 (1995)","journal-title":"Bull. Symb. Log."},{"issue":"4","key":"9516_CR28","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s10472-012-9322-x","volume":"65","author":"A Van Gelder","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."},{"issue":"2","key":"9516_CR29","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":"9516_CR30","first-page":"422","volume-title":"Lecture Notes in Computer Science","author":"Nathan Wetzler","year":"2014","unstructured":"Wetzler, N.D., Heule, M.J.H., Hunt\u00a0Jr, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02014). LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-019-09516-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09516-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09516-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T21:53:15Z","timestamp":1694641995000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-019-09516-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,22]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,3]]}},"alternative-id":["9516"],"URL":"https:\/\/doi.org\/10.1007\/s10817-019-09516-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,2,22]]},"assertion":[{"value":"30 January 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 February 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 February 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}