Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Resolution-Based Interactive Proof System for UNSAT

Philipp Czerner, Javier Esparza, Valentin Krasotin, Adrian Krauss

TL;DR

The paper tackles the challenge of verifying UNSAT efficiently when certificates can be prohibitively large. It develops an interactive proof framework grounded in the IP=PSPACE theorem and introduces a non-standard arithmetisation that makes a Davis-Putnam-like UNSAT procedure competitive with interactive verification. The authors prove correctness and competitiveness, implement an interactive certifier (icdp), and experimentally compare it against conventional certification and DRAT-based certificates, showing dramatic reductions in Verifier time and communication at the cost of Prover overhead. This work highlights a principled pathway to scalable, server-assisted SAT solving with verifiable unsatisfiability proofs and opens questions about extending these ideas to more modern solving paradigms. The findings have practical implications for building certified solving services where verification is lightweight for clients but provably reliable.

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.

A Resolution-Based Interactive Proof System for UNSAT

TL;DR

The paper tackles the challenge of verifying UNSAT efficiently when certificates can be prohibitively large. It develops an interactive proof framework grounded in the IP=PSPACE theorem and introduces a non-standard arithmetisation that makes a Davis-Putnam-like UNSAT procedure competitive with interactive verification. The authors prove correctness and competitiveness, implement an interactive certifier (icdp), and experimentally compare it against conventional certification and DRAT-based certificates, showing dramatic reductions in Verifier time and communication at the cost of Prover overhead. This work highlights a principled pathway to scalable, server-assisted SAT solving with verifiable unsatisfiability proofs and opens questions about extending these ideas to more modern solving paradigms. The findings have practical implications for building certified solving services where verification is lightweight for clients but provably reliable.

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.
Paper Structure (30 sections, 16 theorems, 10 equations, 7 figures, 4 tables, 1 algorithm)

This paper contains 30 sections, 16 theorems, 10 equations, 7 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Multisets.
  4. Formulas, CNF, and resolution.
  5. Resolution.
  6. Polynomials.
  7. Interactive Proof Systems
  8. Competitive Interactive Protocols
  9. The Davis-Putnam Resolution Procedure
  10. Constructing Competitive Interactive Protocols for UNSAT
  11. Interactive Protocol
  12. The interactive protocol is correct and competitive with $\textit{Alg}$
  13. An Interactive Proof System Competitive with the Davis-Putnam Resolution Procedure
  14. An arithmetisation compatible with $R_x$ and $C_x$
  15. $\mathcal{B}$ is compatible with $R_x$.
  16. ...and 15 more sections

Key Result

Lemma 2.2

Let $p_1, p_2$ be distinct univariate polynomials over $\mathbb{F}$ of degree at most $d \geq 0$. Let $r$ be selected uniformly at random from $\mathbb{F}$. The probability that $p_1(r) = p_2(r)$ holds is at most $d /\mathopen|\mathbb{F}\mathclose|$.

Figures (7)

  • 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.
  • Figure 2: Interactive vs. conventional certification: Time consumption of (a) Prover and (b) Verifier, in seconds.
  • Figure 3: Interactive vs. conventional certification: Memory usage of Prover, in kilobytes.
  • Figure 4: Interactive vs. conventional certification: Communication complexity, in kilobytes.
  • Figure 5: Interactive certification with icdp vs. conventional certification with kissat and DRAT-trim: Solving time, in seconds.
  • ...and 2 more figures

Theorems & Definitions (43)

  • Remark 2.1
  • Lemma 2.2: Schwartz-Zippel Lemma
  • proof
  • Definition 4.1
  • Example 4.2
  • Lemma 4.3
  • proof
  • Lemma 4.4
  • proof
  • Theorem 4.5
  • ...and 33 more