Certified Optimization


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.txt
Then the proof trace is checked by running:
  dres-check clause_def.txt
Constraint 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.

Contact

Graeme Gange

Home