mentionsVarXOR
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.