{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:57:38Z","timestamp":1764403058331,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720155"},{"type":"electronic","value":"9783030720162"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce , a new proof format for unsatisfiable SAT problems, and its associated toolchain. Compared to , the  format allows solvers to include more information in proofs to reduce the computational cost of subsequent elaboration to . The format is easy to parse forward and backward, and it is extensible to future proof methods. The provision of optional proof steps allows SAT solver developers to balance implementation effort against elaboration time, with little to no overhead on solver time. We benchmark our  toolchain against a comparable  toolchain and confirm &gt;84% median reduction in elaboration time and &gt;94% median decrease in peak memory usage.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_4","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"59-75","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A Flexible Proof Format for SAT Solver-Elaborator Communication"],"prefix":"10.1007","author":[{"given":"Seulkee","family":"Baek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mario","family":"Carneiro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Blanchette, J.C., Fleury, M., Fontaine, P.: Scalable fine-grained proofs for formula processing. Journal of Automated Reasoning pp. 1\u201326 (2019)","DOI":"10.1007\/s10817-018-09502-y"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings 1999 Design Automation Conference (Cat. No. 99CH36361). pp. 317\u2013320. IEEE (1999)","DOI":"10.1145\/309847.309942"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Hunt, W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: International Conference on Automated Deduction. pp. 220\u2013236. Springer (2017)","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Fleury, M.: Optimizing a verified SAT solver. In: Badger, J.M., Rozier, K.Y. (eds.) NFM. LNCS, vol. 11460, pp. 148\u2013165. Springer (2019)","DOI":"10.1007\/978-3-030-20652-9_10"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Fleury, M., Blanchette, J.C., Lammich, P.: A verified SAT solver with watched literals using imperative HOL. In: Andronick, J., Felty, A.P. (eds.) CPP. pp. 158\u2013171. ACM (2018)","DOI":"10.1145\/3167080"},{"key":"4_CR6","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of the conference on Design, Automation and Test in Europe-Volume 1. p. 10886. IEEE Computer Society (2003)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Haken, A.: The intractability of resolution. Theoretical Computer Science 39, 297\u2013308 (1985)","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"4_CR8","unstructured":"Heule, M.J.H.: The DRAT format and DRAT-trim checker. arXiv preprint $${\\rm {arXiv}}$$:1610.06229 (2016)"},{"key":"4_CR9","unstructured":"Heule, M.J.H., Biere, A.: Clausal proof compression. In: International Workshop on the Implementation of Logics (2015)"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt, W.A., Wetzler, N.: Verifying refutations with extended resolution. In: International Conference on Automated Deduction. pp. 345\u2013359. Springer (2013)","DOI":"10.1007\/978-3-642-38574-2_24"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt, W.A., Wetzler, N.: Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test. Verif. Reliab. 24(8), 593\u2013607 (Sep 2014)","DOI":"10.1002\/stvr.1549"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: International Conference on Theory and Applications of Satisfiability Testing. pp. 228\u2013245. Springer (2016)","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR. LNCS, vol.\u00a07364, pp. 355\u2013370. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"4_CR14","unstructured":"Kautz, H., Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search. In: Proceedings of the National Conference on Artificial Intelligence. pp. 1194\u20131201 (1996)"},{"key":"4_CR15","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability. Addison-Wesley Professional (2015)"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Lammich, P.: The GRAT tool chain. In: International Conference on Theory and Applications of Satisfiability Testing. pp. 457\u2013463. Springer (2017)","DOI":"10.1007\/978-3-319-66263-3_29"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Efficient verified (un) SAT certificate checking. Journal of Automated Reasoning pp. 1\u201320 (2019)","DOI":"10.1007\/s10817-019-09525-z"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Mari\u0107, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle\/HOL. Theoretical Computer Science 411(50), 4333\u20134356 (2010)","DOI":"10.1016\/j.tcs.2010.09.014"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Oe, D., Stump, A., Oliver, C., Clancy, K.: versat: A verified modern SAT solver. In: International Workshop on Verification, Model Checking, and Abstract Interpretation. pp. 363\u2013378. Springer (2012)","DOI":"10.1007\/978-3-642-27940-9_24"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Shankar, N., Vaucher, M.: The mechanical verification of a dpll-based satisfiability solver. Electronic Notes in Theoretical Computer Science 269, 3 \u2013 17 (2011), proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop (LSFA 2010)","DOI":"10.1016\/j.entcs.2011.03.002"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05584, pp. 244\u2013257. Springer (2009)","DOI":"10.1007\/978-3-642-02777-2_24"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"S\u00f6rensson, N., Biere, A.: Minimizing learned clauses. In: Kullmann, O. (ed.) Theory and Applications of Satisfiability Testing - SAT 2009. pp. 237\u2013243. Springer Berlin Heidelberg, Berlin, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02777-2_23"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. Formal Methods in System Design 42(1), 91\u2013118 (2013)","DOI":"10.1007\/s10703-012-0163-3"},{"key":"4_CR24","unstructured":"Sutcliffe, G., Zimmer, J., Schulz, S.: Tstp data-exchange formats for automated theorem proving tools. Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems 112, 201\u2013215 (2004)"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Van\u00a0Gelder, A.: Improved conflict-clause minimization leads to improved propositional proof traces. In: Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing. p. 141\u2013146. SAT \u201909, Springer-Verlag, Berlin, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02777-2_15"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: Mechanical verification of SAT refutations with extended resolution. In: International Conference on Interactive Theorem Proving. pp. 229\u2013244. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_18"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T00:05:28Z","timestamp":1616371528000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"141","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}