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.

Datei:Pdratchk.zip contains a Haskell program that 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. To compile it, you need GHC and the stack build tool.

The format is based on the following paper: Tobias Philipp. Certificates for Parallel SAT Solver Portfolios with Clause Sharing and Inprocessing. In: GCAI 2016.