Skip to content

Certifying Answers of Boolean SAT-Solvers (with a proof combining Coq and OCaml typecheckers)

License

Notifications You must be signed in to change notification settings

boulme/satans-cert

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

64 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

SatAns-Cert (Certifying Answers of Boolean SAT-Solvers)

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.

Credits

Sylvain Boulmé and Thomas Vandendorpe from Verimag, supported by ERC Stator led by David Monniaux.

Installation

Requirements

  1. ocaml. Tested with versions >= 4.05 and <= 4.07.1. (But other versions should work too).

  2. ocamlbuild. Tested with version 0.12.0 abd 0.14.0. (But other versions should work too).

  3. coq. Tested with versions >= 8.7.2 and <= 8.9.0. Here, other versions are likely to not work !

Compilation of satans-cert

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/

Optional installation of drat-trim

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.

Optional installation of 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.

Usage

    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.

Code Overview

The main code of santans-cert is defined in SatAnsCert.v together with its partial correctness proof, see coq_src/README for details.

About

Certifying Answers of Boolean SAT-Solvers (with a proof combining Coq and OCaml typecheckers)

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published