# SAT Solver-Prover in Lean 4

The Boolean satisfiability problem (**SAT**) asks whether a finite set of formulas in *Boolean* (i.e., *true* or *false* valued) variables `$P$`

, `$Q$`

,… has a solution. The formulas are built from the variables using logical operations such as `$\vee$`

(and), `$\wedge$`

(or) and `$\neg$`

(not). A *SAT solver* is a program that solves such a problem, returning *sat* with a solution if solutions exists, and *unsat* if no solutions exist, often with some kind of proof that there is no solution in the latter case.

In the case there is no solution, a SAT solver **does not** simply check all possible assignments of boolean values to variables and see that they fail. Instead the solver searches for a *contradiction*, i.e., a deduction of *False*, assuming the existence of a solution.
The deductions may be returned as human readable tree-like structures, as we described in a previous post about implementation of a SAT solver.

I describe here SATurn — a SAT solver-prover I implemented in **Lean 4**. This is a program that outputs one of

- a solution together with a proof that this is a solution, or
- a proof that there is no solution.

Furthermore, the compiler verifies that the program terminates for any valid input, and has correct output of one of the above two forms.

Indeed, the program (once it compiled) ran correctly immediately — something I have never experienced with a program of comparable (or even close to comparable) complexity. In contrast, while attempting computer assisted proofs of any complexity (even in a strongly-typed language like scala) a lot of time and effort spent (and cognitive load) is in checking and debugging.

## Why SAT?

The importance of SAT comes from the Cook-Levine theorem from the early 1970s. This says that if SAT has a polynomial time solution, then *every* problem that is in **NP** can be solved in polynomial time. Indeed every problem in NP can be mapped to a problem in SAT so that a solution of the SAT problem can be transformed in polynomial time to a solution of the original problem. In practice even problems that are not in NP make use of SAT solvers to solve sub-problems.

An additional motivation for considering SAT is that I feel it is a typical algorithmic mathematical problem. Specifically, a solution to SAT involves a smart search, giving a structured mathematical object that is often useful for further work (though in the worst case is too large and complex to comprehend). This proof object maps to an actual proof of a statement, with correctness of the proof depending only on the correct formulation of the statement. Many mathematical algorithms are of this nature, though in general one has to allow *unknown* as an option for the answer.

For instance a search for whether a knot is *slice* can give a bounding disc (showing slice), an obstruction to being slice (showing not slice) or fail to solve (i.e., return *unknown*). In case we get an answer (either a bounding disc or an obstruction), this will be illuminating beyond establishing the truth of the statement.

## Why **Lean 4** for solver-provers?

A *solver-prover* for a mathematical problem is a program that is guaranteed to terminate and return an answer with a proof of its correctness. The proof of correctness should either be in the foundations of a formal system, or should be transformable into such a proof (with a guarantee that the transformation function is correct and terminates). In the case of problems without algorithmic solutions (or with algorithmic solutions but where we may wish to allow a timeout), we can consider *incomplete solver-provers*, which may return *unknown*.

For solver-provers to be possible, useful and practical we need a language with three features, of which the first two are needed even for the possibility of a solver-prover.

- Statements and proofs can be represented in the language so that the compiler can check correctness.
- The language can run efficiently.
- There is a decent mathematics library and community of mathematicians working with the language.

Without the first, clearly the compiler cannot check correctness and termination. Without the second, nobody will be able to run the algorithms – so they will be essentially constructive proofs.

The presence of a mathematical library means that one does not have to start from scratch. More importantly, all algorithms involving (for example) *free groups* uses the same internal representation (that of the library), they will be able to work together. Finally, if solver-provers work well they can contribute to the library.

As far as I know, **Idris** is the first language to meet the first two criteria, and **Lean 4** is (or will soon be) the first to meet all three.

## Using SATurn

I will not discuss here the details of implementation, which closely follows the *scala* implementation described in a previous post. I only describe (some aspects of) how SAT problems and proofs are represented and how SATurn works in some simple examples. This section assumes familiarity with Lean or some similar language such as Agda or Idris.

### Representing SAT

Any SAT problem can be represented in **CNF**. This means that we are given a finite collection of formulas which must be satisfied, each of which is a so called *clause*. A clause is a formula of the form `$l_1\vee\dots\vee l_n$`

, with each `$l_j$`

(called a *literal*) of the form either `$l_j = P$`

or `$l_j = \neg P$`

for a variable `$P$`

.

Note that if both `$P$`

and `$\neg P$`

are present in a clause then it is always true. We omit such clauses. Thus, to specify a clause is equivalent to specifying for each variable `$P$`

which of three possible cases listed below holds. It is natural to associate to the three cases an element in `Option Bool`

.

- If
`$P$`

is present: we associate`some true`

. - If
`$\neg P$`

is present: we associate`some false`

. - Neither
`$P$`

nor`$\neg P$`

are present: we associate`none`

.

We shall use indices from `$0$`

to `$n - 1$`

to represent the variables, where `$n$`

is the number of variables. Thus, a clause is (represented by) a finite sequence of length $n$ with values in `Option Bool`

. A finite sequence with values in a type `$\alpha$`

is in turn represented by a dependent function
`$(j: \textrm{Nat}) \to j < n \to \alpha$`

(I switched to this from `$Fin\ n \to \alpha$`

due to problems with pattern matching since `$Fin\ n$`

is not an indexed inductive type in Lean).

A *valuation*, i.e., an assignment of truth to each variable, clearly corresponds to a finite sequence of booleans of length `$n$`

. It is easy to see that a clause `$c$`

is true at some valuation`$v$`

if and only if, for some `$k$`

with `$0\leq k < n$`

, we have `$c (k) = some (v(k))$`

. Thus, taking witnesses into account, we define propositions `sat`

and `unsat`

depending on a finite sequence of clauses by

```
def sat{dom n: Nat}(clauses : FinSeq dom (Clause (n + 1))) :=
∃ valuat : Valuat (n + 1),
∀ (p : Nat), ∀ pw : p < dom,
∃ (k : Nat), ∃ (kw : k < n + 1),
(clauses p pw k kw) = some (valuat k kw)
```

and

```
def unsat{dom n: Nat}(clauses : FinSeq dom (Clause (n + 1))) :=
∀ valuat : Valuat (n + 1),
Not (
∀ (p : Nat), ∀ pw : p < dom,
∃ (k : Nat), ∃ (kw : k < n + 1),
(clauses p pw k kw) = some (valuat k kw)
)
```

### Examples

We define three clauses `$P \vee Q$`

, `$\neg P$`

and `$\neg Q$`

and two corresponding statements as follows:

```
def cl1 : Clause 2 :=
(some true) +: (some true) +: FinSeq.empty
def cl2 : Clause 2 :=
(some false) +: (none) +: FinSeq.empty
def cl3 : Clause 2 :=
(none) +: (some false) +: FinSeq.empty
def eg1Statement : FinSeq 3 (Clause 2) :=
cl2 +: cl1 +: cl3 +: FinSeq.empty
def eg2Statement := tail eg1Statement
```

Typically one does not know whether the solution is positive or negative. Hence it is best to first find structured solutions using `solve`

and view them. We shall see how to skip this step if desired. Thus we run

```
def eg1Soln := solve (eg1Statement)
def eg2Soln := solve (eg2Statement)
#eval eg1Soln.toString
#eval eg2Soln.toString
```

and obtain the outputs:

- a resolution tree

```
Examples.lean:29:0
"unsat: [none, none] from [(some false), none] & [(some true), none]; using: {[(some false), none]} and {[(some true), none] from [none, (some false)] & [(some true), (some true)]; using: {[none, (some false)]} and {[(some true), (some true)]}}"
```

- a valuation that is a solution

```
Examples.lean:30:0
"sat: [true, false]"
```

We can then obtain the proofs of the appropriate proposition using the `getProof`

function on the structured proof. This depends on the *typeclass* `Prover`

which associates a statement and proof to the structured proof.

```
def eg1 : unsat eg1Statement := getProof eg1Soln
def eg2 : sat eg2Statement := getProof eg2Soln
#check eg1
#check eg2
```

If we specify the type using the incorrect choice between `sat`

and `unsat`

, then we get a compiler error. If we do not specify the type, it is inferred more weakly, so is not
readily usable. A function `proveOrDisprove`

combines `solve`

and `getProof`

in case one wants to directly obtain a proof.

This code has not been tested for performance. Further this is my first serious work with lean, i.e., beyond following along some tutorials. Hence there is a lot of scope for improvement. Suggestions and comments are most welcome.