Producing and verifying extremely large propositional refutations (Q694550)

Most high-performance satisfiability solvers and special-theory decision procedures are unable to provide a proof of unsatisfiability. Since bugs have been discovered in many such programs long after being put into service, an uncheckable decision poses a significant problem if important economic or safety decisions are to be based upon it. The thesis of the paper is that decision procedures can and should be designed to be able to output an easily verifiable certificate (i.e., proof), then that certificate can be verified without addressing the issue of whether the program is bug-free. The standard proposed is that the language of certificates should be recognizable in deterministic log-space. Intuitively, an algorithm to recognize a log-space language may re-read the input as often as desired, but can only write into working storage consisting of a fixed number of registers, each able to store \(O(\log L)\) bits, for inputs of length \(L\). An explicit resolution proof is one of the suitable certificates. A detailed specification for an explicit resolution derivation is called the \%RES format. The author of the paper has developed a verifier for the \%RES format (named checker 3) that is able to handle proofs with lengths in the thousands of gigabytes on certain available computer servers. But the leading solvers develop a conflict graph as the basis for deriving new clauses and use much more compact formats for derivations. This paper provides the in-depth comparison of various formats. One of these compact formats, called \%RUP (reverse unit propagation), states the derived clauses but does not provide any information about how each was derived. This language has little hope for log-space recognition. However, \%RUP is useful as an intermediate format that can be post-processed into the \%RES format for final checking by an independent checker. The question of whether \%RUP proofs can viably be post-processed into an explicit resolution format is discussed in detail. The author of the paper developed a program rupToRes to expand a \%RUP proof into an explicit \%RES proof, as well as specified both formats for other developers to use. The primary advantage of the \%RUP format is its ease of implementation inside a solver. The work described in this paper has made it possible for developers to add \%RUP output routines with relative ease to their favorite solvers and enter them in the ``verified unsatisfiable'' track of the annual SAT Solver Competitions.