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.

Structs

ConstraintTag

An identifier for constraints, which is used to relate constraints from the model to steps in the proof. Under the hood, a tag is just a NonZero<u32>. The underlying integer can be obtained through the Into implementation.

InferenceCode

An inference code is a combination of a constraint tag with an inference label. Propagators associate an inference code with every propagation to identify why that propagation happened in terms of the constraint and inference that identified it.

ProofLog

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

Traits

InferenceLabel

A label of the inference mechanism that identifies a particular inference. It is combined with a ConstraintTag to create an InferenceCode.