Lean 4 SAT Solver-Prover

Stream: lean4

[Siddhartha Gadgil]

This is to share a SAT Solver-Prover I wrote in Lean 4 (described below), but also a general question of how to run this usefully. This proves or disproves a SAT statement. It seems that I should implement ToString instances, and then use the result by explicitly specifying the statement type (or make this into tactics.

This was my first work with lean, so the code is suboptimal in many ways. But I really like the idea of being able to compute with proofs of correctness of computation carried along, so thanks a lot for Lean 4.

SATurn : SAT Solver-prover in lean 4

SATurn is a SAT solver-prover in lean 4 based on the DPLL algorithm. Given a SAT problem, we get either a solution or a resolution tree showing why there is no solution. Being written in Lean 4 allows:

• The program generates proofs in the foundations of the lean prover, so these are independently checked (both for existence and non-existence of solutions).
• The program itself is checked by lean, so guaranteed to terminate and give a correct answer.

Proofs can be obtained by using the methods solve and proveOrDisprove in the file DPLL.lean. The former gives an object in a type representing either verified solutions or resolution trees. The latter gives a proof of existence or non-existence verified by the lean prover kernel.

Many improvements are necessary, and some are forthcoming (including convenience is usability.)

[Siddhartha Gadgil]

Sorry, there seems to be a bug found when I found a better way to consider examples. Presumably this is in translating the problem (as everything else is formally verified)

[Siddhartha Gadgil]

A quick update - there are some baby examples at https://github.com/siddhartha-gadgil/Saturn/blob/main/Saturn/Examples.lean

[Siddhartha Gadgil]

A blog post about this is at https://siddhartha-gadgil.github.io/automating-mathematics/posts/sat-prover-lean/. This is mostly a general overview with not many implementation details.

Once more, I would appreciate comments on impoving the code (including pointers to documentation etc).