Module cnf 

Tseitin clausification: a grounded, quantifier-free ProofExpr → CNF over the CDCL core’s Lits (Tseitin, 1968 — the standard linear-size equisatisfiable transform that introduces one auxiliary variable per compound subformula). This is the bridge from the logic-grid encoding (closures, at-most-one, of-pair, clue clauses) to the crate::cdcl SAT engine, giving the Untrusted trust tier: solve premises ∧ ¬goal; UNSAT ⇒ the goal is entailed. The same CNF feeds the RUP checker (the fast trust tier) and is the input an AllDifferent GAC propagator filters.

Structs

Cnf

A CNF formula under construction: a variable table (atoms canonicalised so a = b and b = a share a variable) plus the accumulating clause set. Clone so a prepared premise CNF can be reused per goal — the of-pair Tseitin work is done once, then each cell only adds its ¬goal unit (incremental solving, the IPASIR pattern).

Functions

cdcl_entails

Does premises ⊨ goal (propositionally)? Encodes premises ∧ ¬goal to CNF and runs CDCL: UNSAT ⇒ entailed. None if the problem is not purely propositional over recognisable atoms (caller falls back). This is the Untrusted tier — the verdict with no emitted proof, for the raw-speed comparison against Z3.