Module grid_solver 

A fast, certified finite-domain (logic-grid) solver.

Logic-grid puzzles ground to a quantifier-free clause/rule set; a 4×4 grid is a small SAT(+equality) problem that a determined-CSP solver closes in milliseconds. The wall the previous engine hit was speed: engine::cert_saturate re-saturates O(facts²) at every search node. This module is the incremental replacement — trail-based watched-literal unit propagation + DPLL — that finds the answer fast.

Crucially, certification is DECOUPLED from search (see crate::verify): the solver finds the model/refutation however it likes, then a post-pass emits a DerivationTree from the recorded reasons, reusing the certified inference rules. crate::verify::check_derivation re-checks that tree in the kernel, so the solver sits OUTSIDE the trusted base — a wrong tree yields verified == false, never a false claim.

Build order (see plan): Phase A de-risks the emitter (this file’s tests prove the certified tree SHAPES the solver will produce actually certify), before any search machinery exists.

Functions

grid_prove

Solve a single grid cell by propagation and emit its certified derivation. The premises must be ground (call grounding::ground_problem first). Returns None when the cell is not forced by propagation alone (it needs search — Phase C) or the premises do not classify as a grid.