We provide an OCaml wrapper certified in Coq to check answers of state-of-the-art SAT-solvers. On UNSAT answers, our wrapper checks LRAT certificates generated by drat-trim. Actually, we have been inspired by the "Efficient Certified RAT Verification" paper.
Our main contribution is to base the design of our certified checker on a parametricity property of ML polymorphic types, in order to keep the Coq code as lightweight as possible.
See details in our slides from the Coq workshop 2018.
This technique is provided by our Impure library located here at coq_src/Impure/ as a git-subrepo. Actually, we wish to put this Impure library as a true separate library. But this would currently be rather inconvenient because of the lack of a "Separate Extraction" in Coq that is truly compatible with OCaml separate compilation, see feature wish coq#8042.
See our draft paper on this work.
Sylvain Boulmé and Thomas Vandendorpe from Verimag, supported by ERC Stator led by David Monniaux.
-
ocaml. Tested with versions >= 4.05 and <= 4.07.1. (But other versions should work too).
-
ocamlbuild. Tested with version 0.12.0 abd 0.14.0. (But other versions should work too).
-
coq. Tested with versions >= 8.7.2 and <= 8.9.0. Here, other versions are likely to not work !
From the root of the repository, simply run:
make -C ocaml/
NB: this first compiles the Coq sources and extract them in ocaml/coq_extracted before running ocamlbuild.
Then, if you want to test than everything is ok, run:
make -C examples/
Simply clone and make the drat-trim repository.
Then make drat-trim executable known from your PATH.
NB: drat-trim is needed to produce LRAT proofs from DRAT proofs produced by state-of-the-art SAT-solvers.
We have tried several state-of-the-art SAT-solvers like CaDiCaL, CryptoMinisat 4.5.3, CryptoMinisat 5, Glucose 4 or Riss 4.27.
The simplest way is to download directly the source of such SAT solvers from the SAT competition pages, like the SAT Competition 2018 page. Then make these executables known from your PATH.
NB: in our experiments, CryptoMinisat 4.5.3 and Riss 4.27 have been the only solvers to produce non-RUP RAT clauses. All others have only produced DRUP proofs.
satans-cert <input.cnf> [ <OPTION> ... ]
where <input.cnf> is a file in DIMACS format
-l [LRAT_FILE] just check LRAT_FILE
-s [SOLVER] where SOLVER is the command running the solver:
solver's input is given on standard input (in DIMACS format)
solver's answer has to be on standard output (in DIMACS format)
solver's DRAT proof has to be in a file named "proof.out"
or which named is given with -drat-file option
NB: if SOLVER is the empty string (default case) then DRATTRIM is attempted on DRAT_FILE
-outfile [DIMACS_OUT_FILE] name of the auxiliary DIMACS FILE OUTPUT from the sat solver
-d [DRATTRIM] where DRATTRIM is the command running drat-trim (default is "drat-trim")
-drat-file [DRAT_FILE] name of the auxiliary DRAT_FILE
-lrat-file [LRAT_FILE] name of the auxiliary LRAT_FILE
-f force recomputation and remove generated auxiliary files (default)
-lazy skip recomputation if auxiliary file exists, and preserve these files anyway
-help Display this list of options
See also bash scripts in bin/ to wrap a given sat solver, or direct invocations in bug_examples/ and examples/Makefile.
The main code of santans-cert is defined in SatAnsCert.v together with its partial correctness proof, see coq_src/README for details.
-
coq_src/ contains all our Coq sources, including the Impure library as a subdirectory and the OCaml oracles of this library.
-
ocaml/ contains our OCaml oracles for
satans-cert. -
bug_examples/ contains examples using
satans-cert. -
examples/ contains other CNF examples in DIMACS format. Moreover, file sudoku9-s1.out gives the model (in DIMACS format) of sudoku9-s1.cnf found by CaDiCaL. At last, file sudoku9-1.lrat gives a UNSAT proof (in LRAT format) of sudoku9-1.cnf found from the DRAT proof of CaDiCaL by drat-trim.
-
bin/ contains scripts to wrap
satans-certoptions.