How we logically assume that the SAT solver's claims of unsat are correct.

The whole point of Satlink is to be able to call an external SAT solver, written in C or C++, and trust its results. Here, we explain exactly how we do that.

Our assumptions about the SAT solver will be expressed as constraints about
a new function,

(satlink-run-fn config formula env$) → (status env$)

- Inputs
config is a config-p that says which SAT solver to run and how to run it.formula is the cnf formula to solve.env$ is env$, a bit array that will be used to store the satisfying assignment from the SAT solver, in the SAT case.- Outputs
status is the answer we get back from the SAT solver; in practice it will either be:sat or:unsat , or perhaps:failed if we run into some kind of gross error—for instance, perhaps the SAT solver produces output that we weren't expecting, like "Segmentation fault" or "Killed".env$ is the updated env$ bit array; in the:sat case it should contain the satisfying assignment.lrat-proof will be NIL unlessconfig.lrat-check is true. In that case, it is expected that the solver will write a file "[input-filename].lrat" containing an LRAT proof; see "projects/sat/lrat/README".

We use ACL2's partial-encapsulate feature to assume that the function satisfies certain constraints.

To make our story as tight as possible, we would like to assume very little
about

**Theorem: **

(defthm true-listp-of-satlink-run-fn (true-listp (satlink-run-fn config formula env$)) :rule-classes :type-prescription)

**Theorem: **

(defthm len-of-satlink-run-fn (equal (len (satlink-run-fn config formula env$)) 3))

The final constraint is the real one. The idea here is to express:

if

then the formula evaluates to false under every environment.

However, we don't even need to assume that if our solver outputs an LRAT
proof that can be checked by the LRAT checker in "projects/sat/lrat". So if
the configuration option

But the quantification here isn't quite right for a rewrite rule, so instead we assume the contrapositive:

if NOT(the formula evaluates to false under every environment),

and we are not checking an LRAT proof,

then NOT(

Which simplifies down to:

if the formula evaluates to true under any environment,

and we are not checking an LRAT proof,

then

So the real constraint looks like this:

**Theorem: **

(defthm satlink-run-fn-unsat-claim (implies (and (equal (eval-formula formula arbitrary-env) 1) (not (config->lrat-check config))) (not (equal (mv-nth 0 (satlink-run-fn config formula env$)) :unsat))))

And that's it. We don't need to assume anything about what happens in the

- Satlink-run-impl
- Core function used to run the SAT solver.
- Satlink-run
- Connection between the implementation and the logical story.