pub fn structured_leaf(clauses: &CanonClauses) -> Option<Route>Expand description
A cofactor is a structured leaf if a decidable specialist refutes it — the full dispatcher
(crate::solve::solve_structured) returns UNSAT via a route that is not raw CDCL or the
certified-no-shortcut Incompressible verdict. So GF(2)/parity (Tseitin), mod-p (mod-p
Tseitin), counting (pigeonhole/exact-cover), 2-SAT, Horn — every nut the paper already cracks —
is a leaf here, certified internally by the route it fired. Returns that route, or None if no
specialist crushes the cofactor (it must be branched, or it is ⊥/satisfiable).