Verifying SAT formula

Stream: lean4

[Chase Norman]

I am looking to verify a result that was proven with a SAT solver. The SAT formula was generated with a moderately complex python script, making it difficult to ascertain whether unsatisfiability result corresponds to the desired theorem.

Ideally, the proof of the theorem would be entirely self contained—including the generation of the SAT formula and the call to the SAT solver. However, it appears that Lean does not have direct integration with SAT solvers (although Isabelle appears to have such capability?). The next best thing would be to write a program in Lean (or Coq?) that generates the SAT formula and then use program verification to show that the unsatisfiability of the formula implies the impossibility theorem. Presumably this would be done by defining a type for CNF formulae and writing the program to generate an instance of that type. The SAT formula and the data used to construct it are quite lengthy, so I am unsure if Lean program verification would be the best approach. I see that there is a #Program verification channel but I can seem to find little information online about how to properly verify programs in Lean.

So, in short, how would you suggest going about the verification of such a result? Are there existing (verified) tools that unroll finite quantifiers in Lean to produce SAT formulae?

Thanks.

[Mario Carneiro]

how large is the sat formula?

[Mario Carneiro]

and how large is the program that generates it

[Mario Carneiro]

and how large is the proof that it is unsat

[Wojciech Nawrocki]

@Chase Norman the verified encodings project of @Cayden Codel sounds relevant.

[James Gallicchio]

I’ve also been working on integrating SAT solvers with Lean, including verifying DRAT proofs, but there’s a lot of code to write…

[Chase Norman]

@Mario Carneiro the largest of the SAT formulas has an UNSAT core of length 9,297. The CNF file is about 8 megabytes. The program is a few hundred lines long, but most of it is just about generating the set of examples that demonstrate the impossibility result. If these can be given as “input” to the Lean program then it is not necessary to include this in the code. Without that it would be about 50 lines maximum.

[Henrik Böving]

James Gallicchio said:

I’ve also been working on integrating SAT solvers with Lean, including verifying DRAT proofs, but there’s a lot of code to write…

We do have that in mathlib4 already iirc.

[James Gallicchio]

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Sat/FromLRAT.lean Aha! Very good :)

[James Gallicchio]

@Chase Norman I have a working FFI integration with CaDiCaL, I could probably clean it up and put it in a library, and add support for hooking into the LRAT proof checker.

[James Gallicchio]

but that only solves the back half of your problem; proving the encoding correct is entirely Cayden’s domain.

[Cayden Codel]

Indeed, my research project hopes to verify that common SAT encodings are correct. I'd be interested to hear more about your use-case. Is your encoding built up of smaller, more common "atoms" such as cardinality constraints, or is it highly personalized for the problem at hand? Feel free to PM me

[Chase Norman]

@James Gallicchio I have completed the construction of a cnf formula with Cayden's formalism. Does the machinery exist to prove the unsatisfiability of such a formula within Lean 3? For reference, the CNF has 2864 variables and 10889 clauses.

[James Gallicchio]

Mm, that's definitely pushing the limits. I think mathlib has an LRAT proof checker, but I don't think it generates an actual Lean proof term of unsat for the cnf formula. My impression is Mario experimented with trying to generate the proof terms and it was not feasible (the proof terms have very bad kernel performance).

[James Gallicchio]

I'm putting together Lean bindings for provers and for drat-trim in LeanSAT, but it's not done yet & obviously isn't verified :) I'll likely just introduce an axiom that drat-trim's output is correct.

[James Gallicchio]

(oh, I missed the part about Lean 3 -- I think most of this machinery is and will be developed in Lean 4, mainly because it has a better experience for programmers)

[Mario Carneiro]

James Gallicchio said:

Mm, that's definitely pushing the limits. I think mathlib has an LRAT proof checker, but I don't think it generates an actual Lean proof term of unsat for the cnf formula. My impression is Mario experimented with trying to generate the proof terms and it was not feasible (the proof terms have very bad kernel performance).

It does generate such a proof. It's not so much that the proof terms have bad performance but you hit on implementation limits fairly soon

[James Gallicchio]

Good to know :0