# 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.