{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:13:31Z","timestamp":1760044411155,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572302"},{"type":"electronic","value":"9783031572319"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":96,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Modern SAT or QBF solvers are expected to produce correctness certificates. However, certificates have worst-case exponential size (unless <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{NP}=\\textsf{coNP}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>NP<\/mml:mi>\n                    <mml:mo>=<\/mml:mo>\n                    <mml:mi>coNP<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>), and at recent SAT competitions the largest certificates of unsatisfiability are starting to reach terabyte size.<\/jats:p><jats:p>Recently, Couillard, Czerner, Esparza, and Majumdar have suggested to replace certificates with interactive proof systems based on the <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf {IP}=\\textsf {PSPACE}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>IP<\/mml:mi>\n                    <mml:mo>=<\/mml:mo>\n                    <mml:mi>PSPACE<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> theorem. They have presented an interactive protocol between a prover and a verifier for an extension of QBF. The overall running time of the protocol is linear in the time needed by a standard BDD-based algorithm, and the time invested by the verifier is polynomial in the size of the formula. (So, in particular, the verifier never has to read or process exponentially long certificates). We call such an interactive protocol <jats:italic>competitive<\/jats:italic> with the BDD algorithm for solving QBF.<\/jats:p><jats:p>While BDD-algorithms are state-of-the-art for certain classes of QBF instances, no modern (UN)SAT solver is based on BDDs. For this reason, we initiate the study of interactive certification for more practical SAT algorithms. In particular, we address the question whether interactive protocols can be competitive with some variant of resolution. We present two contributions. First, we prove a theorem that reduces the problem of finding competitive interactive protocols to finding an <jats:italic>arithmetisation<\/jats:italic> of formulas satisfying certain commutativity properties. (Arithmetisation is the fundamental technique underlying the <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf {IP}=\\textsf {PSPACE}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>IP<\/mml:mi>\n                    <mml:mo>=<\/mml:mo>\n                    <mml:mi>PSPACE<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> theorem.) Then, we apply the theorem to give the first interactive protocol for the Davis-Putnam resolution procedure.<\/jats:p>","DOI":"10.1007\/978-3-031-57231-9_6","type":"book-chapter","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T18:01:54Z","timestamp":1712340114000},"page":"116-136","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Resolution-Based Interactive Proof System for UNSAT"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1786-9592","authenticated-orcid":false,"given":"Philipp","family":"Czerner","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9862-4919","authenticated-orcid":false,"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0002-2129-2754","authenticated-orcid":false,"given":"Valentin","family":"Krasotin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"6_CR1","unstructured":"Arora, S., Barak, B.: Computational Complexity: A Modern Approach. Cambridge University Press (2006), https:\/\/theory.cs.princeton.edu\/complexity\/book.pdf"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Babai, L.: Trading group theory for randomness. In: Sedgewick, R. (ed.) Proceedings of the 17th Annual ACM Symposium on Theory of Computing, May 6-8, 1985, Providence, Rhode Island, USA. pp. 421\u2013429. ACM (1985). https:\/\/doi.org\/10.1145\/22145.22192, https:\/\/doi.org\/10.1145\/22145.22192","DOI":"10.1145\/22145.22192"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Reynolds, A., Kremer, G., Lachnitt, H., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Viswanathan, A., Viteri, S., Zohar, Y., Tinelli, C., Barrett, C.W.: Flexible proof production in an industrial-strength SMT solver. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13385, pp. 15\u201335. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_3, https:\/\/doi.org\/10.1007\/978-3-031-10769-6_3","DOI":"10.1007\/978-3-031-10769-6_3"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Buss, S.R., Tur\u00e1n, G.: Resolution proofs of generalized pigeonhole principles. Theor. Comput. Sci. 62(3), 311\u2013317 (1988)","DOI":"10.1016\/0304-3975(88)90072-2"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Couillard, E., Czerner, P., Esparza, J., Majumdar, R.: Making $$\\sf IP=\\sf PSPACE$$ practical: Efficient interactive protocols for BDD algorithms. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III. Lecture Notes in Computer Science, vol. 13966, pp. 437\u2013458. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_21, https:\/\/doi.org\/10.1007\/978-3-031-37709-9_21","DOI":"10.1007\/978-3-031-37709-9_21"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960). https:\/\/doi.org\/10.1145\/321033.321034, https:\/\/doi.org\/10.1145\/321033.321034","DOI":"10.1145\/321033.321034"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Goldwasser, S., Micali, S., Rackoff, C.: The knowledge complexity of interactive proof-systems (extended abstract). In: Sedgewick, R. (ed.) Proceedings of the 17th Annual ACM Symposium on Theory of Computing, May 6-8, 1985, Providence, Rhode Island, USA. pp. 291\u2013304. ACM (1985). https:\/\/doi.org\/10.1145\/22145.22178, https:\/\/doi.org\/10.1145\/22145.22178","DOI":"10.1145\/22145.22178"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297\u2013308 (1985)","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511576430"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Necula, G., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: CAV 02: Computer-Aided Verification, pp. 526\u2013538. Lecture Notes in Computer Science 2404, Springer-Verlag (2002)","DOI":"10.1007\/3-540-45657-0_45"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Heule, M., Jr., W.A.H., Kaufmann, M., Wetzler, N.: Efficient, verified checking of propositional proofs. In: ITP. Lecture Notes in Computer Science, vol. 10499, pp. 269\u2013284. Springer (2017)","DOI":"10.1007\/978-3-319-66107-0_18"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H.: Proofs of unsatisfiability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 635\u2013668. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA200998, https:\/\/doi.org\/10.3233\/FAIA200998","DOI":"10.3233\/FAIA200998"},{"key":"6_CR13","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. CoRR abs\/1605.00723 (2016)","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Lov\u00e1sz, L., Naor, M., Newman, I., Wigderson, A.: Search problems in the decision tree model. SIAM J. Discret. Math. 8(1), 119\u2013132 (1995)","DOI":"10.1137\/S0895480192233867"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Lund, C., Fortnow, L., Karloff, H.J., Nisan, N.: Algebraic methods for interactive proof systems. J. ACM 39(4), 859\u2013868 (1992). https:\/\/doi.org\/10.1145\/146585.146605, https:\/\/doi.org\/10.1145\/146585.146605","DOI":"10.1145\/146585.146605"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.: Certifying model checkers. In: CAV 01: Computer Aided Verification, pp. 2\u201313. Lecture Notes in Computer Science 2102, Springer-Verlag (2001)","DOI":"10.1007\/3-540-44585-4_2"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Necula, G.: Proof-carrying code. In: Principles of Programming Languages. pp. 106\u2013119. ACM Press (1997)","DOI":"10.1145\/263699.263712"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Shamir, A.: IP = PSPACE. J. ACM 39(4), 869\u2013877 (1992). https:\/\/doi.org\/10.1145\/146585.146609, https:\/\/doi.org\/10.1145\/146585.146609","DOI":"10.1145\/146585.146609"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57231-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,3]],"date-time":"2024-05-03T16:03:51Z","timestamp":1714752231000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57231-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572302","9783031572319"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57231-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"6 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","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":"fossacs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/fossacs\/","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":"79","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":"24","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":"0","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":"30% - 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":"9","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)"}}]}}