A Resolution-Based Interactive Proof System for UNSAT

Philipp Czerner, Javier Esparza, Valentin Krasotin +1

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…