Invoking the SAT solver from a metaprogram

Stream: general

[Daniel Weber]

From what I understand, Lean has a SAT solver built in to it used for implementing bv_decide. Is there any documentation/examples for how to invoke it from meta code? I'm interested in the part of finding a counterexample, I don't care about verifying the proof

[Kim Morrison]

The module doc in src/Lean/Elab/Tactic/BVDecide.lean may help you.

[Henrik Böving]

The SAT solver is just a binary of CaDiCal that can either be in your Lean installation or pointed to elswhere by configuration options. You just call it like you would call any other process https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/BVDecide/External.lean. But there is of course a much larger work involved in getting a counter example from a SAT solver. You'll need to provide a reduction from your actual problem to CNF (which is what most of bv_decide is busy with) and then based on a model that the solver provides be able to recover an assignment for your variables in the non reduced part (the recovery is in this file https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean).

What kind of problem are you looking into?

[Daniel Weber]

I'm curious about using it to produce counterexamples for #Equational, but perhaps it's better to do that outside Lean

[Henrik Böving]

Afaict that project is essentially interested in quantified EUF logic. A SAT solver is not the right tool to operate in this logic. For the quantifier free fragment you can implement something like congruence closure using a union-find or even an e-graph (or do what is about to follow). For the fragment with quantifiers you will probably want to use a fully fledged SMT solver like Z3 or CVC5 or other first order logic systems like superposition provers.

[Henrik Böving]

https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Running.20the.20.60vampire.60.20solver.20on.20all.20of.20the.20equations/near/473149546 that's what i'm talking about (vampire is superposition)^^

[Eric Wieser]

I'm slightly surprised to see CaDiCaL run as a subprocess and not linked into the Lean binary. Was this just easier, or are the reasons to actively prefer it this way?

[Henrik Böving]

It does allow a few things that would otherwise not easily be possible. For one users can supply their own solver instead, for example they could use kissat instead of cadical (though Bituwlza reports that kissat has not yet managed to achieve speedups in bitblasting SMTCOMP but Armin's group says it is faster in SATCOMP so it might be relevant) or other SAT solvers (or if they don't support LRAT, wrappers around SAT solvers) as a drop in replacement.

Furthermore it allows us to provide a better story for interactivity. If a user is editing a file and there is a bv_decide invocation below it will be called and then interrutped and called and interrupted again etc. With the model as an external process this is completely fine: We can have a loop that polls every n milliseconds whether the interruption token has been set (or the solver is done) and if it has been set terminate the solving process. If we had linked cadical in instead our Lean process would call into cadical and then not be able to even check the cancellation token anymore. Of course we could maybe have another thread and introduce a primitive to kill that thread and whatnot but that's not really in the spirit of cooperative cancellation with Tasks.

Lastly the profiling data shows that serializing and deserializing the CNF to a file is a basically free operation when compared to the time that the solver actually spends "thinking" so it would be a miniscule speedup at best. The things that will make bv_decide perform noticably faster for users are going to be improving the preprocessing capabilities to get on a level with what Bitwuzla does, as well as improving the AIG optimizations and potentially the circuit encodings themselves as well.

[Eric Wieser]

One other consideration in favor of the separate binary is that crashes in cadical (which upon preliminary inspection seems to invoke undefined behavior at times) do not take down the lean server.