there are 2 different projects named "leansat"

Stream: lean4

[David Renshaw]

I found this to be confusing, so I'm posting here to raise awareness.

There are two distinct projects named "leansat":
https://github.com/JamesGallicchio/LeanSAT
https://github.com/leanprover/leansat

[François G. Dorais]

And neither has much to do with the development of small satellites. :smile:

[James Gallicchio]

Yeah, we did not intend to name clash :joy:

[James Gallicchio]

I may rename mine because it seems the leanprover leansat is going to be actively developed by the FRO

[Patrick Massot]

Aren’t they meant to work together in the end?

[James Gallicchio]

Ours is to do with verified encodings to SAT, the leanprover/leansat is attempting to provide a SAT tactic for expressions over bool and bitvec. Unclear whether they will be merged in the near future because the end user interfaces are so dissimilar. I'm hoping the backend interfaces to SAT solvers will be merged though!

[Kim Morrison]

leanprover/leansat is being actively developed. Currently there is:

1. a frontend that processes a Lean goal and reflects it to a e : BoolExpr, and a proof builder that can prove False given a proof of e.unsat.
2. a translation from BoolExpr to CNF
3. machinery to send that CNF to a SAT solver, and then verify in the kernel the lrat proof produced

(1. and 2. are my work last week, 3. is mostly existing work of Josh Clune's in the leansat repo, which @Henrik Böving has been cleaning up. He's also provided all the necessary glue between 2. and 3.)

It runs. However right now the proofs it produces contain a sorry, because the translation from BoolExpr to CNF is not verified. This should not be particularly difficult, and some combination of @Henrik Böving and I will probably do it soon.

It is quite preliminary, and there are unnecessary bottlenecks at several places in the current implementation.

I've only briefly looked at James' repo. Happy to talk sometime to see if there is something we can incorporate from it. There's also yet another repo doing similar things, but which I think is currently private.

More updates coming soon!

[Mario Carneiro]

Both are being actively developed. It seems like there was a communication failure that lead to the project getting named the same as an existing active project

[Kim Morrison]

Sorry about this. My understanding is that Leo set up the leanprover/leansat to hold Josh's work last year (created June, first real commit November), and I guess wasn't aware of James'.

(And apologies that my message may have implied the other wasn't being actively developed. The leansat one had been motionless until about a week ago: I wanted to make the distinction more between now and last week than between leanprover/leansat and JamesGallichio/leansat!)

[James Gallicchio]

This should not be particularly difficult

I hope this is true... we resorted to the classic "build a bunch of infrastructure" strategy, roughly as follows:

• a state monad (EncCNF) to keep track of the map from (the original) variables to Nat, and the highest number used in the CNF (which grows as auxiliaries are allocated)
• a subtype of these monadic programs (VEncCNF) that states what is being encoded (over the original variables) with some inane verification condition that ensures the CNF is satisfiable iff the formula over the original variables is satisfiable. that way you can generate and use auxiliary variables for e.g. tseitin transformation but they are completely hidden by the signature.

the proofs of those verification conditions have not been too bad, but it still required a surprising amount of infrastructure to finish. let me know if you get something simple working, I'll be very interested to check it out!!

sidenote: VEncCNF is actually a dijkstra monad a la F*, but we have yet to find use for this observation.

[Kim Morrison]

Okay, challenge accepted. :-) I agree I should not say "not particularly difficult" about something that I committed with a sorry. I'm certainly hoping still to be more lightweight here.

[Kim Morrison]

@James Gallicchio, I pushed a tedious but low-tech verification in https://github.com/leanprover/leansat/pull/8. The actually transformation is about 15 lines in LeanSat.Reflect.BoolExpr.Tseitin.Defs, and the proof is 600 lines in ...Lemma.

[Kim Morrison]

I'm pretty unimpressed with how many independent inductions I did over BoolExpr, but it seemed easier to just prove each fact I needed in order, rather than try to combine them.

[Kim Morrison]

The specific encoding I use it profligate with variables, which may hurt: a real SAT solver won't care at all, but the lrat verification step will. I'm hoping that the it's easy enough to post-process this profligacy out on the CNF side.

But it would be great to have comparisons. If you were able to connect your Tseitin transform to our representation of BoolExpr and CNF, we could plug it into the pipeline and see how it runs. I think we will have a benchmark suite soon.

[Kim Morrison]

I heard from @Jeremy Avigad earlier today about some of the leansat work happening at CMU. It would be great if we could have a get together sometime soon to discuss what should live in which repository. I'd propose we schedule around me + @Henrik Böving + @James Gallicchio, but then if there are others at CMU (or elsewhere) everyone is welcome.

Unfortunately 9am-4pm Pittsburgh time I'm usually unavailable, but flexible before or afterwards.

[Jeremy Avigad]

It would be good if @Cayden Codel can join the discussion as well. He and James can explain the project and its goals.

[Mario Carneiro]

I'd also like to attend, I have an alternative encoding proof that I'm hoping to upstream to CMU LeanSAT soon

[Kim Morrison]

Great: we're aiming at 2024-02-27T09:00:00+11:00. I'll send an invite, let me know if that time won't work.

[Henrik Böving]

@Mario Carneiro bonk

[James Gallicchio]

thoughts on renaming my leansat to lean4sat (lean proofs for sat tools) and the FRO's leansat to sat4lean (sat tools for lean proofs)? :stuck_out_tongue:

[James Gallicchio]

it's unfortunate that the language is lean4 because lean4sat can be mis-read as lean4 SAT instead of "Lean for SAT"

[Mario Carneiro]

we call that a pun

[Eric Wieser]

Leaninsat and satinlean?

[Julian Berman]

Satin Lean, the glossiest of Leans.

[Henrik Böving]

While I do like the idea of the pun it seems to me personally like this is just asking for a mixup and potentially confusing google results for either package?

[Mario Carneiro]

to be fair, the names LeanSAT and leansat are not any less mixup-prone

[Henrik Böving]

Don't get me wrong I do think there should be a change, I just think we should nail it the first time and not change more later on.

[Mario Carneiro]

I think James's project could be called sat-tools or sat-encoding