Distributed SAT / SMT backend

Stream: general

[Dominik Schreiber]

Hello there! I'm Dominik (Schreiber), young investigator @ KIT (Karlsruhe, Germany). I'm researching parallel and distributed SAT and SMT solving and am the main author of the state-of-the-art distributed automated reasoning platform Mallob, which supports proofs of unsatisfiability and which we're currently beginning to extend towards SMT solving.

I've heard that LEAN has some degree of SAT/SMT integration and so I wanted to ask whether there is perhaps some interest to explore a connection of our system as an alternative/additional SAT/SMT backend system to LEAN. Specifically, I'm currently preparing a research proposal and consider mentioning mathematical theorem proving à la LEAN as a potential application sub-topic. So this is something that may not happen immediately (also depending on your requirements) but that we could have a chat about and then explore some time down the line. I'd be happy if you could let me know what you think!

[Shreyas Srinivas]

@Henrik Böving is the right person to ask. Lean ships with cadical 2 which is exposed to lean users through the bv_decide tactic

[Shreyas Srinivas]

You can see more documentation here : https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/#tactic-ref-sat

[Henrik Böving]

Dominik Schreiber said:

Hello there! I'm Dominik (Schreiber), young investigator @ KIT (Karlsruhe, Germany). I'm researching parallel and distributed SAT and SMT solving and am the main author of the state-of-the-art distributed automated reasoning platform Mallob, which supports proofs of unsatisfiability and which we're currently beginning to extend towards SMT solving.

I've heard that LEAN has some degree of SAT/SMT integration and so I wanted to ask whether there is perhaps some interest to explore a connection of our system as an alternative/additional SAT/SMT backend system to LEAN. Specifically, I'm currently preparing a research proposal and consider mentioning mathematical theorem proving à la LEAN as a potential application sub-topic. So this is something that may not happen immediately (also depending on your requirements) but that we could have a chat about and then explore some time down the line. I'd be happy if you could let me know what you think!

Hi, nice to see you here! We met in 2023 in Wiesbaden if you remember. We would definitely be interested in integrating other solvers with the bv_decide tactic of Lean. Looking at the code base of Mallob you already seem to have support for LRAT? That would be just perfect, bv_decide currently operates on LRAT proofs produced by CaDiCaL so integrating other LRAT producing solvers with it should be pretty easy.

[Dominik Schreiber]

Henrik Böving said:

Hi, nice to see you here! We met in 2023 in Wiesbaden if you remember. We would definitely be interested in integrating other solvers with the bv_decide tactic of Lean. Looking at the code base of Mallob you already seem to have support for LRAT? That would be just perfect, bv_decide currently operates on LRAT proofs produced by CaDiCaL so integrating other LRAT producing solvers with it should be pretty easy.

Hi Henrik! Oh yes, cool! Sure, Mallob supports LRAT (or more specifically the LRUP subset). Depending on how your LRUP parser and checker is implemented, there might be some bumps with large proofs (clause IDs up to 2^63 bits and large gaps between them, also potentially very large active clause sets), but we could just see how it works out!

[Henrik Böving]

The parser and infrastructure can in principle deal with large clause IDs, I'm not quite sure the checker is able to handle gaps but that can be changed. One issue is that in the current setup bv_decide is not able to check a proof step by step but parses everything upfront, then starts to check. This is due to technical constraints in Lean's architecture when generating proofs that the kernel accepts. So if the certificates are too large we might end up running out of RAM. I think this is something that can be engineered as well though.

[Dominik Schreiber]

Ohh yes, reading the whole proof into RAM can be an issue, especially once you start going distributed (say 100s-1000s of solvers). In case you're interested, here's some experimental results on that (p.22 Tab. 7, at wallclock solving times of ≤300s). Anyways, sounds like a cool project if you're also interested! :)