about `bv_decide`

Stream: new members

[Asei Inoue]

I don't understand how to usebv_decide.

I hear bv_decide calls fast SAT solver internally, so I can solve SAT problem by using by_decide?
But I cannot use by_decide to solve a SAT problem.

import Std.Tactic.BVDecide

example : ∃ x1 x2 x3 x4 x5 : Bool,
  (x1 || ! x5 || x4) &&
  (! x1 || x5 || x3 || x4) &&
  (! x3 || ! x4) := by
  /- None of the hypotheses are in the supported BitVec fragment after applying preprocessing. -/
  bv_decide

[Asei Inoue]

the docstring of grind says:

grind is not designed for goals whose search space explodes combinatorially, think large pigeonhole instances, graph‑coloring reductions, high‑order N‑queens boards, or a 200‑variable Sudoku encoded as Boolean constraints. Such encodings require thousands (or millions) of case‑splits that overwhelm grind’s branching search.

For bit‑level or combinatorial problems, consider using bv_decide. bv_decide calls a state‑of‑the‑art SAT solver (CaDiCaL) and then returns a compact, machine‑checkable certificate.

[Asei Inoue]

so using bv_decide, can I solve Sudoku or N-queens problem?

[Aaron Liu]

you need to phrase it in terms of docs#BitVec I think

[Aaron Liu]

oh you want an exists goal

[Aaron Liu]

bv_decide handles forall goals

[Asei Inoue]

so using bv_decide, can I solve Sudoku or N-queens problem?

how about this?

[Henrik Böving]

bv_decide reasons in the logic of quantifier free bitvector theory. What this means is you can use it to prove sentences of the form forall x1 x2 x3, bitvec_expr_containing x1 x2 x3. In particular if a sentence is wrong it will provide you with a counter example. So if you want to use it to solve problems for you what you can do is ask it to prove forall x1 x2 x3, ~problem x1 x2 x3 and if there is an assignment of x1, x2, x3 that satisfies the problem it will tell you about it. Applied to your case:

import Std.Tactic.BVDecide

example : ∀ x1 x2 x3 x4 x5 : Bool, !(
  (x1 || ! x5 || x4) &&
  (! x1 || x5 || x3 || x4) &&
  (! x3 || ! x4)) := by
  intros
  bv_decide

yields:

x1✝ = false
x5✝ = false
x4✝ = false
x3✝ = false

note that x2 is not included in this model because it doesn't occur in your formula. In principle the translation from existential to universally quantified problem could be made automatic but proving existentials is not the primary use case so I didn't do that.

Aaron Liu said:

you need to phrase it in terms of docs#BitVec I think

No, bv_decide handles BitVec, Bool, enumeration types, UIntX and IntX as well as structures of finite types with invariants.

Asei Inoue said:

so using bv_decide, can I solve Sudoku or N-queens problem?

how about this?

If you formulate the problem in the same way I described above you can totally do that yes. But again this is not the primary use case, the primary use case is proving. If you don't know how that works: If you want to prove a property P using a SAT solver you instead ask it to search for an assignment of ~P, if it cannot find this assignment it will return UNSAT. Luckily for us a modern SAT solver is going to accompany this UNSAT with a description of how it arrived at this conclusion. bv_decide is capable of turning this description into a Lean proof, thus demonstrating that ~~P which is equivalent to P.

[Asei Inoue]

@Henrik Böving Thank you!