SAT solving
Proof certificate
A checkable record supporting a solver's result.
Definition
Proof certificate
A proof certificate records derivation steps that a separate checker can validate.
For SAT solving, certificates most often support unsat. The checker need not repeat the solver's search, but it must confirm that each recorded step is allowed.
01
Example
A DRAT certificate lists clause additions and deletions that end with the empty clause.
02
Important distinction
A certificate format does not guarantee that every solver route emits a certificate.
After reading this article, you should be able to
- Define Proof certificate in the sense used on this site.
- Explain why sat and unsat usually require different forms of evidence.