PDRAT

State-of-the-art SAT solvers are highly tuned systematic-search procedures augmented with formula simplification techniques. They emit unsatisfiability proofs in the DRAT format to guarantee correctness of their answers. However, the DRAT format is inadequate to model some parallel SAT solvers such as the award-winning system plingeling. The parallel DRAT format can be used to certify UNSAT answers from such parallel SAT solvers.

The Datei:Pdratchk.zip program checks whether a given PDRAT proof is correct or not. In the case it accepts a proof together with a formula, the formula is guaranteed to be unsatisfiable.