A certified solution and inference checker for CP/LCG logs, plus memory-friendly checkers
for large propositional unsatisfiability proofs.
Compiling `cp_check` requires OCaml (plus Extlib) and Coq. It was developed
with OCaml 4.01 and Coq 8.4; other versions may work, or not.
`dres-check` and `idrup-check` require a C++ compiler supporting C++11.

Each of the proof logs contains several files:

- coq.txt
- - model specification.
- lit_sem.txt
- - mapping of proof variables to model semantics.
- clause_def.txt
- - unsatisfiability proof in dres format.
- sol.txt
- - claimed optimal solution.

The solution and inferences can be checked by running:

cp_check -sol sol.txt -lits lit_sem.txt -trace clause_def.txt coq.txtThen the proof trace is checked by running:

dres-check clause_def.txtConstraint source annotations are recorded as comments in clause_def.txt; so the proof can be run through tracecheck instead by stripping out any deletion directives:

grep -v '^d' | tracecheck

File | Description |
---|---|

checkCP.tar.gz | The certified CP trace checker, with idrup and dres checkers. |

j30.tar.gz | Optimality proofs (in dres format) for the J30 RCPSP instances. |

certcp-instances.tar.gz | Raw data-files for the RCPSP, openshop and jobshop instances. |