Options for running SAT solvers that produce UNSAT proofs.
For higher confidence (at some cost to runtime), some SAT solvers are able to produce UNSAT proofs. Small programs such as drat-trim can check these proofs, to ensure the SAT solver reasoned correctly.
Satlink now includes Perl scripts that can make use of this capability for the Glucose and Riss3g solvers. In particular, see the following scripts:
The general idea of these scripts is, e.g., for Glucose:
All of this works well with Satlink. You can still see the output from the solver and the verifier in real time, interrupt it, etc.
To use these tools, you will need to first:
You can then add the
cd [books]/centaur/satlink/solvers cert.pl test-glucose-cert cert.pl test-riss3g-cert
To use these scripts from Satlink, you can then typically just use a Satlink configuration such as:
(satlink::make-config :cmdline "glucose-cert" ...)
The environment variable SATLINK_TRUST_SOLVER can be set to 1 to suppress proof checking. When this variable is set, we will NOT instruct the solver to produce an UNSAT proof and (of course) will not check the non-existent proof.
We use this feature as follows:
This gives us a good blend of performance and confidence. If the solver
somehow screws up and claims to have proven a theorem that isn't really true,
we may not find out about it until our regression fails. But in exchange, we
can always use