determinesVar
plain-language theorem explainer
determinesVar encodes the condition that constraint K forces the value of variable v under reference assignment aRef: any assignment agreeing with aRef everywhere except possibly at v, and satisfying K, must agree at v as well. Researchers formalizing propagation completeness for mixed CNF-XOR SAT instances cite this when defining variable determination. The definition is a direct universal quantification over alternative assignments that fix all other variables.
Claim. Let $A_n$ be the set of assignments (functions $Var(n) → Bool$). Let $K$ be a constraint (either a CNF clause or an XOR constraint on $n$ variables). Then $determinesVar(aRef, K, v)$ holds when, for every $a' ∈ A_n$, if $a'$ agrees with $aRef$ on all variables except possibly $v$ and $a'$ satisfies $K$, then $a'(v) = aRef(v)$.
background
Constraint(n) is an inductive type whose constructors are cnf(C) for a CNF clause C and xor(X) for an XOR constraint X. Assignment(n) is the type of total Boolean functions on Var(n), where Var(n) ≔ Fin(n). satisfiesConstraint is the predicate that checks whether an assignment meets a given Constraint, defined separately for the CNF and XOR cases. The module states that constraints are either CNF-clauses or XOR-checks, providing the local setting for propagation arguments in SAT encodings.
proof idea
One-line definition that directly unfolds the universal quantification over alternative assignments a' together with the agreement condition on all w ≠ v and the antecedent satisfiesConstraint a' K.
why it matters
This definition is invoked inside the Propagation-Completeness (PC) predicate and inside the PeelingData and PeelingResult structures that witness repeated variable extraction. PC itself requires, for every nonempty U ⊆ inputs, the existence of a K and v ∈ U such that K determines v w.r.t. aRef. The construction supports downstream extraction lemmas that peel variables from CNF+XOR instances while preserving the reference assignment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.