pith. sign in

arxiv: 2401.14996 · v8 · pith:2L5ZTHFTnew · submitted 2024-01-26 · 💻 cs.LO

A Resolution-Based Interactive Proof System for UNSAT

Philipp Czerner , Javier Esparza , Valentin Krasotin , Adrian Krauss This is my paper

Pith reviewed 2026-05-24 04:44 UTC · model grok-4.3

classification 💻 cs.LO
keywords interactive proofsresolutionDavis-Putnam procedurearithmetisationunsatisfiability certificatesSAT solvers
0
0 comments X

The pith

An interactive protocol verifies Davis-Putnam resolution without reading exponential certificates.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves a theorem that reduces the task of building competitive interactive protocols for resolution-based solvers to the problem of finding an arithmetisation of formulas with certain commutativity properties. It then applies the theorem to construct the first such protocol for the Davis-Putnam resolution procedure. In the resulting protocol the overall running time stays linear in the time taken by the resolution procedure itself while the verifier invests only polynomial time in the size of the input formula. This approach addresses the practical limit that unsatisfiability certificates can reach terabyte scale, allowing a weak client to confirm results returned by a powerful server without ever reading or storing the full certificate.

Core claim

A theorem reduces finding competitive interactive protocols to finding arithmetisations of formulas that satisfy commutativity properties; applying the theorem produces the first interactive protocol for the Davis-Putnam resolution procedure whose running time is linear in the procedure's own time and whose verifier runs in time polynomial in the formula size.

What carries the argument

A reduction theorem that converts the search for competitive interactive protocols into the search for an arithmetisation of formulas satisfying commutativity properties.

If this is right

  • The verifier never reads or processes certificates whose size is exponential in the formula.
  • The protocol's total communication and computation remain linear in the runtime of the underlying Davis-Putnam procedure.
  • Interactive certification becomes available for a practical resolution-based algorithm rather than only for BDD-based methods.
  • Clients with limited resources can obtain correctness guarantees from remote solvers without storing terabyte-scale data.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same reduction may be reusable for other variants of resolution or for modern CDCL solvers once suitable arithmetisations are identified.
  • Cloud-based SAT services could adopt interactive verification to let resource-limited users confirm results without downloading full proofs.
  • If arithmetisations with the needed commutativity can be found for QBF or other proof systems, the approach would extend beyond plain SAT.

Load-bearing premise

An arithmetisation of the formulas exists that satisfies the required commutativity properties.

What would settle it

An explicit unsatisfiable formula on which the protocol accepts an incorrect claim of unsatisfiability, or a satisfiable formula on which it rejects a correct claim of satisfiability.

Figures

Figures reproduced from arXiv: 2401.14996 by Adrian Krauss, Javier Esparza, Philipp Czerner, Valentin Krasotin.

Figure 1
Figure 1. Figure 1: (a) Size of instances (number of variables and clauses). Instances solved by icdp within 20 minutes using the greedy variable order (see (b)) are shown as dots, the rest as crosses. (b) Number of instances solved by icdp with different variable orderings. certificate. For time and memory consumption, we present results for Prover and Verifier separately [PITH_FULL_IMAGE:figures/full_fig_p019_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Interactive vs. conventional certification: Time consumption of (a) Prover and (b) Verifier, in seconds. Certification time. We first report on the runtime of Prover. For interactive certification, this is the total time icdp’s Prover needs to both solve the instance using DavisPutnam and interact with Verifier. For conventional certification, Prover’s runtime is given by the runtime of DavisPutnam, becaus… view at source ↗
Figure 3
Figure 3. Figure 3: The memory required to simply start icdp (without performing any computation) is 15 MiB, and for 27 out of our 79 instances these 15 MiB sufficed for both DavisPutnam and the complete protocol (orange dot). In the rest of the instances, the memory overhead of icdp’s Prover is quadratic. The reason is that, while icdp’s Prover computes the formulas φ1, ..., φk (see [PITH_FULL_IMAGE:figures/full_fig_p020_3.png] view at source ↗
Figure 3
Figure 3. Figure 3: Interactive vs. conventional certification: Memory usage of Prover, in kilobytes. [PITH_FULL_IMAGE:figures/full_fig_p021_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Interactive vs. conventional certification: Communication complexity, in kilobytes. reverse order, and so icdp stores the formulas φ1, ..., φk. (For convenience they are stored in RAM, but they could also be stored on disk; one could also recompute them, trading time for space.) On the contrary, at any given time DavisPutnam only needs to store φi and φi+1 for some 1 ≤ i ≤ k − 1. We do not provide quantita… view at source ↗
Figure 5
Figure 5. Figure 5: Interactive certification with icdp vs. conventional certification with kissat and DRAT-trim: Solving time, in seconds. formula for all possible truth assignments. Therefore, with a 20-minute timeout for the Prover, and generously assuming that it can check 107 assignments per second, general-purpose Provers can only certify formulas with at most 33 variables, while icdp’s Prover goes beyond 50. 7.4. icdp … view at source ↗
Figure 6
Figure 6. Figure 6: Interactive certification with icdp vs. conventional certification with kissat and DRAT-trim: Verifier’s time, in seconds. 347ms, while icdp’s Verifier takes at most 0.2ms on the benchmarked instances10. This result is likely due to the theoretical exponential speedup of Verifier compared to conventional certification. Certification space. We omit the experimental results, because they do not add insight: … view at source ↗
Figure 7
Figure 7. Figure 7: Interactive certification with icdp vs. conventional certification with kissat and DRAT-trim: Communication complexity, in kilobytes. 8. Conclusions We have presented the first technique for the systematic derivation of interactive proof systems competitive with a given algorithm for UNSAT. More precisely, we have shown that such systems can be automatically derived from arithmetisations satisfying a few c… view at source ↗
read the original abstract

Modern SAT or QBF solvers are expected to produce correctness certificates. However, certificates have worst-case exponential size (unless NP=coNP), and at recent SAT competitions the largest certificates of unsatisfiability are starting to reach terabyte size. This puts limits to the development of SAT-solving services in which a client with limited computational power sends a formula to a solver running on a powerful server, which returns a certificate to be checked by the client. Recently, Couillard et al. have suggested to replace certificates with interactive proof systems based on the IP=PSPACE 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 competitive with the BDD algorithm for solving QBF. 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 arithmetisation of formulas satisfying certain commutativity properties. (Arithmetisation is the fundamental technique underlying the IP=PSPACE theorem.) Then, we apply the theorem to give the first interactive protocol for the Davis-Putnam resolution procedure. We also report on an implementation and give some experimental results.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper proves a general theorem reducing the existence of competitive interactive protocols (linear prover time, polynomial verifier time) for a proof system to the existence of an arithmetisation of formulas obeying specific commutativity identities. It then applies the theorem to the Davis-Putnam resolution procedure, claiming the first such interactive protocol for resolution-based UNSAT, and reports an implementation together with experimental results.

Significance. If the reduction theorem is correct and the arithmetisation for Davis-Putnam is explicitly constructed and verified to satisfy the required commutativity properties, the result would be significant: it would extend IP-style interactive certification from BDD-based QBF to a core practical SAT algorithm, addressing the terabyte-scale certificate problem for modern resolution solvers.

major comments (2)
  1. [Abstract / Contributions] Abstract and contributions paragraph: the central claim that the theorem yields a protocol for Davis-Putnam rests on the existence of an arithmetisation map on clauses and resolvents that obeys the commutativity identities, yet no definition of this map, no equations showing how resolvents are arithmetised, and no verification that the identities hold are supplied; without these the protocol does not follow from the theorem.
  2. [Theorem statement] The reduction theorem itself is stated at a high level; the manuscript must exhibit the precise commutativity conditions (e.g., which operations must commute with the arithmetisation) and prove they suffice for the interactive protocol to be sound and competitive.
minor comments (1)
  1. [Experiments] The experimental section should report concrete metrics (prover time, verifier time, communication size) relative to the underlying Davis-Putnam solver runtime on the same instances.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and for recognizing the potential significance of extending interactive certification to resolution-based UNSAT. We agree that the submitted manuscript presents the general reduction theorem at a high level and does not supply the explicit arithmetisation construction for Davis-Putnam; we will revise to address both major comments.

read point-by-point responses

  1. Referee: [Abstract / Contributions] Abstract and contributions paragraph: the central claim that the theorem yields a protocol for Davis-Putnam rests on the existence of an arithmetisation map on clauses and resolvents that obeys the commutativity identities, yet no definition of this map, no equations showing how resolvents are arithmetised, and no verification that the identities hold are supplied; without these the protocol does not follow from the theorem.

    Authors: We agree that the explicit arithmetisation map, the equations for resolvents, and the verification of the commutativity identities are required to substantiate the claim. The submitted version omitted these details for brevity after stating the general theorem. In the revision we will add the definition of the map on clauses and resolvents, the explicit equations, and the verification that the required identities hold, thereby making the application of the theorem to Davis-Putnam fully explicit. revision: yes

  2. Referee: [Theorem statement] The reduction theorem itself is stated at a high level; the manuscript must exhibit the precise commutativity conditions (e.g., which operations must commute with the arithmetisation) and prove they suffice for the interactive protocol to be sound and competitive.

    Authors: We accept that the precise commutativity conditions and the argument that they suffice for soundness and competitiveness must be stated explicitly rather than left at a high level. The revision will expand the theorem statement to list the required commutativity identities, and will include a self-contained argument (or detailed sketch) showing that these identities imply both soundness of the resulting interactive protocol and that its complexity remains competitive with the underlying Davis-Putnam procedure. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained via new theorem.

full rationale

The paper proves a new reduction theorem linking competitive interactive protocols to the existence of an arithmetisation with commutativity properties, then states an application to Davis-Putnam resolution. No load-bearing self-citations, no fitted parameters renamed as predictions, and no self-definitional steps appear in the provided text. The central claim rests on the (asserted) existence and verification of the arithmetisation map rather than reducing to prior inputs by construction. This is a standard non-circular structure for a theoretical contribution.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Central claim rests on the IP=PSPACE theorem and the existence of a suitable arithmetisation with commutativity properties for resolution formulas; no free parameters or invented entities are visible from the abstract.

axioms (1)
  • standard math IP=PSPACE theorem
    Basis for replacing certificates with interactive protocols (abstract).

pith-pipeline@v0.9.0 · 5860 in / 1107 out tokens · 26481 ms · 2026-05-24T04:44:54.615185+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

22 extracted references · 22 canonical work pages · 2 internal anchors

  1. [1]

    Computational Complexity - A Modern Approach

    Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach . Cambridge University Press, 2009

    work page 2009

  2. [2]

    Trading group theory for randomness

    L \' a szl \' o Babai. Trading group theory for randomness. In Robert Sedgewick, editor, Proceedings of the 17th Annual ACM Symposium on Theory of Computing, May 6-8, 1985, Providence, Rhode Island, USA , pages 421--429. ACM , 1985. https://doi.org/10.1145/22145.22192 doi:10.1145/22145.22192

    work page doi:10.1145/22145.22192 1985

  3. [3]

    Proof complexity and SAT solving

    Sam Buss and Jakob Nordstr \" o m. Proof complexity and SAT solving. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition , volume 336 of Frontiers in Artificial Intelligence and Applications , pages 233--350. IOS Press, 2021. https://doi.org/10.3233/FAIA200990 doi:10.3233/FAIA200990

    work page doi:10.3233/faia200990 2021

  4. [4]

    Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres N \" o tzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, and Clark W. Barrett. Flexible proof production in an industrial-strength SMT solver. In Jasmin Blanchette, Laura Kov \' a cs, and Dirk Pattinson, editors, Automated R...

    work page doi:10.1007/978-3-031-10769-6 2022

  5. [5]

    Buss and Gy \" o rgy Tur \' a n

    Samuel R. Buss and Gy \" o rgy Tur \' a n. Resolution proofs of generalized pigeonhole principles. Theor. Comput. Sci. , 62(3):311--317, 1988. https://doi.org/10.1016/0304-3975(88)90072-2 doi:10.1016/0304-3975(88)90072-2

    work page doi:10.1016/0304-3975(88)90072-2 1988

  6. [6]

    Making IP = PSPACE practical: Efficient interactive protocols for BDD algorithms

    Eszter Couillard, Philipp Czerner, Javier Esparza, and Rupak Majumdar. Making IP = PSPACE practical: Efficient interactive protocols for BDD algorithms. In Constantin Enea and Akash Lal, editors, Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III , volume 13966 of Lecture Notes in ...

    work page doi:10.1007/978-3-031-37709-9 2023

  7. [7]

    A resolution-based interactive proof system for UNSAT

    Philipp Czerner, Javier Esparza, and Valentin Krasotin. A resolution-based interactive proof system for UNSAT . In Naoki Kobayashi and James Worrell, editors, Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 202...

    work page doi:10.1007/978-3-031-57231-9_6 2024

  8. [8]

    Lu \' s Cruz - Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, and Peter Schneider - Kamp. Efficient certified RAT verification. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings , volume 10395 of Lecture Notes in Computer Sc...

    work page doi:10.1007/978-3-319-63046-5 2017

  9. [9]

    A computing procedure for quantification theory

    Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM , 7(3):201--215, 1960. https://doi.org/10.1145/321033.321034 doi:10.1145/321033.321034

    work page doi:10.1145/321033.321034 1960

  10. [10]

    The knowledge complexity of interactive proof-systems (extended abstract)

    Shafi Goldwasser, Silvio Micali, and Charles Rackoff. The knowledge complexity of interactive proof-systems (extended abstract). In Robert Sedgewick, editor, Proceedings of the 17th Annual ACM Symposium on Theory of Computing, May 6-8, 1985, Providence, Rhode Island, USA , pages 291--304. ACM , 1985. https://doi.org/10.1145/22145.22178 doi:10.1145/22145.22178

    work page doi:10.1145/22145.22178 1985

  11. [11]

    The intractability of resolution

    Armin Haken. The intractability of resolution. Theor. Comput. Sci. , 39:297--308, 1985. https://doi.org/10.1016/0304-3975(85)90144-6 doi:10.1016/0304-3975(85)90144-6

    work page doi:10.1016/0304-3975(85)90144-6 1985

  12. [12]

    Handbook of Practical Logic and Automated Reasoning

    John Harrison. Handbook of Practical Logic and Automated Reasoning . Cambridge University Press, 2009

    work page 2009

  13. [13]

    Marijn J. H. Heule. The DRAT format and drat-trim checker. CoRR , abs/1610.06229, 2016

    work page internal anchor Pith review Pith/arXiv arXiv 2016

  14. [14]

    Marijn J. H. Heule. Proofs of unsatisfiability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition , volume 336 of Frontiers in Artificial Intelligence and Applications , pages 635--668. IOS Press, 2021. https://doi.org/10.3233/FAIA200998 doi:10.3233/FAIA200998

    work page doi:10.3233/faia200998 2021

  15. [15]

    Hunt Jr., Matt Kaufmann, and Nathan Wetzler

    Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, and Nathan Wetzler. Efficient, verified checking of propositional proofs. In Mauricio Ayala - Rinc \' o n and C \' e sar A. Mu \ n oz, editors, Interactive Theorem Proving - 8th International Conference, ITP 2017, Bras \' lia, Brazil, September 26-29, 2017, Proceedings , volume 10499 of Lecture Notes in Com...

    work page doi:10.1007/978-3-319-66107-0 2017

  16. [16]

    In: Proc

    Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Gr \' e goire Sutre, and Westley Weimer. Temporal-safety proofs for systems code. In Ed Brinksma and Kim Guldstrand Larsen, editors, Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings , volume 2404 of Lecture Notes in C...

    work page doi:10.1007/3-540-45657-0 2002

  17. [17]

    Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. CoRR , abs/1605.00723, 2016

    work page internal anchor Pith review Pith/arXiv arXiv 2016

  18. [18]

    Karloff, and Noam Nisan

    Carsten Lund, Lance Fortnow, Howard J. Karloff, and Noam Nisan. Algebraic methods for interactive proof systems. J. ACM , 39(4):859--868, 1992. https://doi.org/10.1145/146585.146605 doi:10.1145/146585.146605

    work page doi:10.1145/146585.146605 1992

  19. [19]

    Search problems in the decision tree model

    L \' a szl \' o Lov \' a sz, Moni Naor, Ilan Newman, and Avi Wigderson. Search problems in the decision tree model. SIAM J. Discret. Math. , 8(1):119--132, 1995. https://doi.org/10.1137/S0895480192233867 doi:10.1137/S0895480192233867

    work page doi:10.1137/s0895480192233867 1995

  20. [20]

    Namjoshi

    Kedar S. Namjoshi. Certifying model checkers. In G \' e rard Berry, Hubert Comon, and Alain Finkel, editors, Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings , volume 2102 of Lecture Notes in Computer Science , pages 2--13. Springer, 2001. https://doi.org/10.1007/3-540-44585-4\_2 doi:10.100...

    work page doi:10.1007/3-540-44585-4 2001

  21. [21]

    George C. Necula. Proof-carrying code. In Peter Lee, Fritz Henglein, and Neil D. Jones, editors, Conference Record of POPL'97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France, 15-17 January 1997 , pages 106--119. ACM Press, 1997. https://doi.org/10.1145/263699.263712 doi:10.114...

    work page doi:10.1145/263699.263712 1997

  22. [22]

    IP = PSPACE

    Adi Shamir. IP = PSPACE . J. ACM , 39(4):869--877, 1992. https://doi.org/10.1145/146585.146609 doi:10.1145/146585.146609

    work page doi:10.1145/146585.146609 1992