Constraint
plain-language theorem explainer
The Constraint inductive type classifies mixed SAT constraints as either CNF clauses or XOR parity checks over n variables. Complexity researchers modeling hybrid SAT instances in Recognition Science would reference this when encoding problems that mix disjunctive and parity constraints. The declaration is a straightforward inductive definition with two constructors drawn from the CNF and XOR modules.
Claim. Let $n$ be a natural number. A constraint over $n$ variables is either a CNF clause $C$ (a disjunction of at most three literals) or an XOR constraint $X$ (a parity condition on a subset of the variables).
background
In the Complexity.SAT.PC module, the Constraint type unifies two standard SAT encodings. The CNF.Clause (imported from SAT.CNF) is an abbrev for List (Lit n), a disjunction of literals. The RSatEncoding.Clause structure supplies the concrete 3-SAT form: a list of at most three signed variable indices. The XORConstraint structure (from SAT.XOR) records a list of variables together with a target parity bit.
proof idea
This is the inductive definition itself, introducing the two constructors cnf and xor with no further computation or lemmas applied.
why it matters
Constraint supplies the common carrier type for the PC module's downstream definitions (constraintsOf, mentionsVar, determinesVar, extractFromPC). These in turn appear in LedgerAlgebra.paired_preserves_balance and CrystalSymmetry.LatticeParams, allowing hybrid CNF+XOR instances to be treated uniformly inside the Recognition Science ledger and symmetry constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.