17.3. What grind is not.

grind is not designed for goals whose search space explodes combinatorially—think large‑n 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.

• Bit‑level or pure Boolean combinatorial problems → use bv_decide. The bv_decide tactic calls a state‑of‑the‑art SAT solver (e.g. CaDiCaL or Kissat) and then returns a compact, machine‑checkable certificate. All heavy search happens outside Lean; the certificate is replayed and verified inside Lean, so trust is preserved (verification time scales with certificate size).

• Full SMT problems that need substantial case analysis across multiple theories (arrays, bit‑vectors, rich arithmetic, quantifiers, …) → use the forthcoming lean‑smt tactic—a tight Lean front‑end for CVC5 that replays unsat cores or models inside Lean.