mentionsVarXOR
The definition checks whether a given variable index occurs in the support list of an XOR constraint. Researchers handling mixed CNF-XOR SAT instances in complexity reductions would cite it when decomposing constraints for uniform processing. It is realized as a direct list scan that applies the .any combinator to the vars field of the input structure.
claimLet $X$ be an XOR constraint over $n$ variables, given by a list of indices together with a parity bit. For a variable index $v$, the predicate mentionsVarXOR$(X,v)$ returns true precisely when $v$ appears in the variable list of $X$.
background
The module treats constraints as either CNF clauses or XOR checks. Var $n$ is the type Fin $n$ of variable indices for a problem of size $n$. XORConstraint $n$ is the structure whose fields are a list of such indices and a Boolean parity value.
proof idea
This is a one-line wrapper that applies the list membership test .any to the vars field of the supplied XORConstraint, using decide on equality with the target variable.
why it matters in Recognition Science
It supplies the XOR case for the mixed-constraint predicate mentionsVar, which dispatches on Constraint to either clause or XOR inspection. The definition therefore supports uniform variable tracking across hybrid constraint systems in the SAT.PC module.
scope and limits
- Does not evaluate the parity bit of the constraint.
- Does not decide satisfiability of the constraint.
- Does not apply to CNF clauses.
- Does not alter or construct new constraints.
Lean usage
match K with | .xor X => mentionsVarXOR X vformal statement (Lean)
26def mentionsVarXOR {n} (X : XORConstraint n) (v : Var n) : Bool :=
proof body
Definition body.
27 X.vars.any (fun u => decide (u = v))
28
29/-- Whether a variable is mentioned in a mixed constraint. -/