satisfiesConstraint
plain-language theorem explainer
The definition specifies when an assignment satisfies a mixed constraint that is either a CNF clause or an XOR parity check. Researchers encoding hybrid SAT problems in the Recognition Science complexity layer cite it when establishing variable forcing. The implementation is a direct pattern match on the constraint constructor that routes to evalClause for CNF cases and parityOf for XOR cases.
Claim. For an assignment $a$ to $n$ variables and a constraint $K$, the predicate holds if $K$ is a CNF clause $C$ and $evalClause(a,C)$ equals true, or if $K$ is an XOR constraint $X$ and the parity of the variables in $X$ under $a$ equals the required parity of $X$.
background
Constraints form an inductive type with two constructors: cnf wrapping a Clause and xor wrapping an XORConstraint. An Assignment is a total function from variables (Fin n or Var n) to Bool. The module sets the local context as satisfaction semantics for mixed CNF/XOR constraints in SAT encodings.
proof idea
The definition proceeds by pattern match on the Constraint inductive. The cnf branch reduces directly to evalClause a C = true. The xor branch reduces to parityOf a X.vars = X.parity. No lemmas are invoked; it is the base semantic clause.
why it matters
This definition is the immediate dependency of determinesVar, which captures when a constraint forces a specific variable relative to a reference assignment. It supplies the satisfaction relation required by the PC module for mixed-constraint SAT analysis. In the broader Recognition Science setting it supports encodings that feed into forcing-chain arguments, though no direct link to T0-T8 or RCL is present here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.