		Search-engine friendly clone of the ACL2 documentation.

Sat-solver-options

Unsat-checking

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:

centaur/satlink/solvers/glucose-cert
centaur/satlink/solvers/riss3g-cert

The general idea of these scripts is, e.g., for Glucose:

We first call Glucose to solve the problem;
When Glucose reports SAT, we just exit (because Satlink can check the satisfying assignment itself); or
When Glucose reports UNSAT, we check the proof using the Drat-Trim unsat proof checker. We only print an "s UNSATISFIABLE" line if Drat-Trim says that the proof is ok.

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.

Setup

To use these tools, you will need to first:

Install glucose and/or riss3g as described in sat-solver-options, and
Install the drat-trim program as drat-trim somewhere in your PATH.

You can then add the glucose-cert or riss3g-cert scripts to your PATH. As a quick test to ensure things are working, you can try to certify these books:

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" ...)

Skipping Proof Checking During Development

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:

We generally set SATLINK_TRUST_SOLVER=1 in our startup scripts. This way, when we are working with ACL2 (either interactively, or when rebuilding books), we just trust the solver and avoid the overhead of UNSAT checking.
We set SATLINK_TRUST_SOLVER=0 for our nightly regressions. These are run automatically, overnight, so performance is not very important.

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 glucose-cert with no performance impact on our everyday work.