pub fn parity_exactly_one(n: usize) -> (DimacsCnf, ExpectedVerdict)Expand description
Coupled exactly-one + parity — a scalable MIXED family that needs BOTH structures at once. The
selectors x₀…x_{n-1} are constrained to exactly one true (an at-most-one clique + an at-least-one
clause — a cardinality covering) AND to even total parity ⊕ xᵢ = 0 (a GF(2) system, encoded by a
width-3 prefix-XOR chain with auxiliaries sᵢ = ⊕_{j≤i} xⱼ plus the unit s_{n-1} = 0). Exactly-one
forces an ODD selector count, the parity forces EVEN — UNSAT, yet neither substructure alone is
(the parity chain is satisfiable, exactly-one is satisfiable). The canonical shape for the fused
parity+cardinality route (crate::lyapunov::fused_parity_cardinality_decide); 2n variables.