Using SAT inside Lean as a computational tool

Stream: general

[Aatman Supkar]

Hi!
Like LeanSAT, do we have features in Lean which let me call a SAT solver to solve a given boolean expression? I want it to work like a function which takes a given expression and returns SAT or UNSAT, and not as a tactic in a proof (like bv_decide). The goal here is to build a solver for a specific problem with help from the SAT solver, and prove its correctness. How do I go about achieving this, exactly?

[Henrik Böving]

LeanSAT already has all of the machinery you are asking for under the hood, what kind of application are you building exactly?

[Aatman Supkar]

I expect to write the input as a structure in the file (a graph G in my case), write a function which answers a query about a certain graph parameter w.r.t. G, and return true/false. I then also want to prove the correctness of said function.

[Henrik Böving]

Well in principle you can find all infrastructure for working with SAT related datastructures here: https://github.com/leanprover/lean4/tree/master/src/Std/Sat. Example use case for how to implement bitblasting with it here https://github.com/leanprover/lean4/tree/master/src/Std/Tactic/BVDecide/Bitblast. Recovering proof certificates here https://github.com/leanprover/lean4/tree/master/src/Std/Tactic/BVDecide/LRAT. And the code to both hook that up with the real world SAT solvers (and also the for your uninteresting part for hooking it up to the tactic world) here https://github.com/leanprover/lean4/tree/master/src/Lean/Elab/Tactic/BVDecide. Do note that apart from Std.Sat we do not provide stability guarantees for any of these APIs though

[Aatman Supkar]

Okay, I'll need some time to go through this and get back to you. Thanks! By the way, what is bitblasting?

[James Gallicchio]

I think bitblasting = treating fixed-width integer arithmetic as a SAT problem, with one (boolean) variable for each bit of your integer variables?

[Henrik Böving]

We don't really use a notion of integers here, it's just BitVec which can be interpreted in both a signed and an unsigned fashion depending on the operations you run on them. But the basic idea is corret yes.

[Henrik Böving]

I mostly posted the bitblasting because it's currently the only thing that translates a higher level description into an AIG in a performant and verified manner

[James Gallicchio]

RE your original question, we have been developing a Lean library called trestle which has a bunch of utilities for writing "formally verified encodings" to SAT. We have some examples for graph problems -- graph coloring and Keller graphs.

Trestle is designed for formally verifying math theorems which were proven by reduction to CNF that is machine-checked to be UNSAT. We have utilities for exporting CNFs and calling solvers, but those utilities are functionally equivalent to those in Std.Sat. So, depending on your use case, the bv_decide machinery may be a better fit.

[Aatman Supkar]

Ah, thanks for the heads up! I'll check it out. I'm working on graph boxicity in particular, and I wanted to design tools which could provide computational aid, so stuff like testing what happens on some specific graph as opposed to proving theorems. Nonetheless, this looks interesting, so I'll check it out, thanks!