determinesVar
determinesVar encodes the property that constraint K fixes variable v to the value given by reference assignment aRef: any assignment agreeing with aRef on all other variables, if it satisfies K, must match aRef at v. Analysts of propagation-complete SAT and XOR encodings cite this when checking that individual constraints isolate variable values during peeling constructions. The definition expands directly to a universal quantifier over agreeing assignments together with the satisfiesConstraint predicate.
claimLet $a$ be an assignment to $n$ variables, $K$ a constraint, and $v$ a variable. Then $K$ determines $v$ with respect to $a$ if, for every assignment $a'$ that agrees with $a$ on all variables other than $v$ and satisfies $K$, one has $a'(v) = a(v)$.
background
Constraints are defined inductively as either CNF clauses or XOR constraints. An Assignment is a total function from variables (Fin n) to Bool, with evaluation of literals and clauses defined in the CNF and RSatEncoding modules. The module states that constraints are either CNF-clauses or XOR-checks, and the satisfiesConstraint predicate combines the two cases. Upstream results supply the Assignment type and the notion of a variable being mentioned in a literal or clause, which are used to interpret the agreement condition in the definition.
proof idea
The definition is a direct expansion into a universal quantifier: it ranges over all alternative assignments a' that agree with aRef on every variable except v, then requires that satisfaction of K by a' forces a' v to equal aRef v. No lemmas are invoked; the body is the primitive statement of the determination relation.
why it matters in Recognition Science
This definition is the core predicate inside the Propagation-Completeness (PC) condition, which asserts that every nonempty subset U of input variables admits a constraint K and v in U such that K determines v with respect to aRef and mentions no other element of U. It is invoked by extractFromPC, PeelingData, and PeelingResult to build explicit peeling witnesses. In the broader Recognition Science setting it supplies the variable-isolation step needed for complexity bounds on encodings that arise from the phi-ladder and eight-tick structures.
scope and limits
- Does not compute or search for a determining constraint K.
- Does not require that K mentions v.
- Does not extend the property to sets of several variables at once.
- Does not address satisfiability of the full instance.
Lean usage
have hDet : determinesVar aRef K v := by ... ; exact hDetformal statement (Lean)
43def determinesVar {n}
44 (aRef : Assignment n) (K : Constraint n) (v : Var n) : Prop :=
proof body
Definition body.
45 ∀ (a' : Assignment n),
46 (∀ w : Var n, w ≠ v → a' w = aRef w) →
47 satisfiesConstraint a' K →
48 a' v = aRef v
49
50/-- Collect all constraints arising from a CNF+XOR instance. -/