{"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":1776881388889,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662488980","type":"print"},{"value":"9783662488997","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_31","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"444-459","source":"Crossref","is-referenced-by-count":5,"title":["Compositional Propositional Proofs"],"prefix":"10.1007","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"31_CR1","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, 103\u2013118 (2015)","journal-title":"Artif. Intell."},{"issue":"1","key":"31_CR2","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1080\/10586458.2008.10129025","volume":"17","author":"M Kouril","year":"2008","unstructured":"Kouril, M., Paul, J.L.: The van der waerden number W(2, 6) is 1132. Exp. Math. 17(1), 53\u201361 (2008)","journal-title":"Exp. Math."},{"key":"31_CR3","doi-asserted-by":"crossref","unstructured":"Kouril, M.: Computing the van der Waerden number $$w(3,4)=293$$ . Integers 12 (2011) Paper A46, 13 p., electronic only","DOI":"10.1515\/integ.2011.112"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"Codish, M., Cruz-Filipe, L., Frank, M., Schneider-Kamp, P.: Twenty-five comparators is optimal when sorting nine inputs (and twenty-nine for ten). In: ICTAI 2014, pp. 186\u2013193. IEEE Computer Society (2014)","DOI":"10.1109\/ICTAI.2014.36"},{"issue":"4","key":"31_CR5","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1038\/scientificamerican1077-108","volume":"237","author":"K Appel","year":"1977","unstructured":"Appel, K., Haken, W.: The solution of the four-color-map problem. Sci. Am. 237(4), 108\u2013121 (1977)","journal-title":"Sci. Am."},{"issue":"2957","key":"31_CR6","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/S0262-4079(14)60350-X","volume":"221","author":"J Aron","year":"2014","unstructured":"Aron, J.: Wikipedia-size maths proof too big for humans to check. New Sci. 221(2957), 11 (2014)","journal-title":"New Sci."},{"key":"31_CR7","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: DATE 2003, pp. 10880\u201310885 (2003)"},{"key":"31_CR8","unstructured":"Goldberg, E.I., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE, pp. 10886\u201310891 (2003)"},{"key":"31_CR9","doi-asserted-by":"crossref","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A., Jr.: 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, Heidelberg (2014)","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"31_CR10","unstructured":"Heule, M.J.H., Hunt, W.A., Jr., Wetzler, N.: Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test. Verification Reliab. (STVR) 24(8), 593\u2013607 (2014)"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Manthey, N., Philipp, T.: Validating unsatisfiability results of clause sharing parallel SAT solvers. In: Pragmatics of SAT, pp. 12\u201325 (2014)","DOI":"10.29007\/6vwg"},{"key":"31_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-34188-5_8","volume-title":"Hardware and Software: Verification and Testing","author":"MJH Heule","year":"2012","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50\u201365. Springer, Heidelberg (2012)"},{"key":"31_CR13","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning 2","author":"GS Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning 2, pp. 466\u2013483. Springer, Heidelberg (1983)"},{"key":"31_CR14","series-title":"Lecture Notes in Computer Science","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, vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"31_CR15","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. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"2\u20134","key":"31_CR16","first-page":"75","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: Picosat essentials. JSAT 4(2\u20134), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"31_CR17","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. LNCS, vol. 7857, pp. 102\u2013117. Springer, Heidelberg (2013)"},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"Van Gelder, A.: Verifying RUP proofs of propositional unsatisfiability. In: ISAIM (2008)","DOI":"10.1007\/978-3-540-72788-0_31"},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt, W.A., Jr., Wetzler, N.: Verifying refutations with extended resolution. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 345\u2013359. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-38574-2_24"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt, W.A., Jr., Wetzler, N.: Expressing symmetry breaking in DRAT proofs. In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction - CADE-25. LNCS, vol. 9195, pp. 591\u2013606. Springer, Heidelberg (2015)","DOI":"10.1007\/978-3-319-21401-6_40"},{"key":"31_CR21","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt, W.A., Jr., Wetzler, N.: Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design, pp. 181\u2013188. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"31_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61\u201375. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T13:28:15Z","timestamp":1748698095000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}