  Modern SAT or QBF solvers are expected to produce correctness certificates.
However, certificates have worst-case exponential size (unless
$\textsf{NP}=\textsf{coNP}$), and at recent SAT competitions the largest
certificates of unsatisfiability are starting to reach terabyte size.
  Recently, Couillard, Czerner, Esparza, and Majumdar have suggested to replace
certificates with interactive proof systems based on the
$\textsf{IP}=\textsf{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 $\textsf{IP}=\textsf{PSPACE}$ theorem.)
Then, we apply the theorem to give the first interactive protocol for the
Davis-Putnam resolution procedure.
