Module proof

Pumpkin supports proof logging for SAT and CP problems. During search, the solver produces a ProofLog, which is a list of deductions made by the solver.

Proof logging for CP is supported in the DRCP format. This format explicitly supports usage where the solver logs a proof scaffold which later processed into a full proof after search has completed. Proof processing is very close to solving, and the rp_engine::RpEngine exposes an API that can be used to process a proof scaffold into a full CP proof.

Modules

• rp_engine
  An API to verify the RP property of clauses.

Structs

• ProofLog
  A proof log which logs the proof steps necessary to prove unsatisfiability or optimality. We allow the following types of proofs:

Enums

• Format
  The format of the proof.