		Search-engine friendly clone of the ACL2 documentation.

Satlink

Logical-story

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. Informally, the idea behind this function is that it will have the following signature:

(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 unless config.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".

Axiomatization

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 satlink-run-fn. It turns out we only need three constraints, with the first two constraints just saying that the function returns three values:

Theorem: true-listp-of-satlink-run-fn

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

Theorem: len-of-satlink-run-fn

(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 satlink-run-fn returns :unsat,
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 lrat-check is set to true, then we don't assume this. If lrat-check is NIL, then we'll just assume the solver is correct.

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( satlink-run-fn returns :unsat )

Which simplifies down to:

if the formula evaluates to true under any environment,
and we are not checking an LRAT proof,
then satlink-run-fn does not return :unsat

So the real constraint looks like this:

Theorem: satlink-run-fn-unsat-claim

(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 :sat case or the case where we're checking LRAT proofs, because our top-level sat wrapper will verify those answers.

Subtopics

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