UniqueSolutionXOR
UniqueSolutionXOR defines the property that a CNF paired with an XOR system has exactly one satisfying assignment. Completeness proofs for backpropagation in SAT encodings cite this uniqueness to establish that determined values match the solution. The definition directly encodes the joint satisfaction condition using existential uniqueness over CNF evaluation and XOR parity checks.
claimGiven a structure ψ consisting of a CNF formula φ and an XOR system H over n variables, the predicate holds precisely when there exists a unique assignment a such that evalCNF(a, φ) equals true and a satisfies every constraint in H.
background
In the SAT.XOR module an XOR constraint records that the parity of a variable subset equals a target boolean. CNFWithXOR is the structure that pairs a standard CNF φ with such an XORSystem H without rewriting the parity constraints into disjunctive normal form. Assignment denotes a total function from the n variables to booleans; evalCNF returns true exactly when every clause of φ is satisfied; satisfiesSystem returns true when every XOR constraint in H holds under the assignment.
proof idea
The declaration is a direct one-line definition that packages the existential-uniqueness quantifier over the conjunction of CNF satisfaction and XOR-system satisfaction. No lemmas or tactics are invoked; the body simply writes the joint predicate.
why it matters in Recognition Science
The predicate supplies the semantic uniqueness hypothesis required by backprop_succeeds_of_unique and determined_values_correct in the Completeness module, and it is exactly the definition of isolates in the Isolation module. It therefore closes the reduction from arbitrary SAT instances to unique-solution instances under the cost-algebra H, supporting the completeness argument that backpropagation recovers the sole satisfying assignment.
scope and limits
- Does not assert existence of a unique solution for any given CNFWithXOR.
- Does not supply an algorithm or decision procedure for locating the assignment.
- Does not encode any concrete backpropagation step semantics.
- Does not invoke the functional equation for H beyond the shared notation.
Lean usage
theorem backprop_succeeds_of_unique {n} (φ : CNF n) (H : XORSystem n) (huniq : UniqueSolutionXOR { φ := φ, H := H }) : BackpropSucceeds φ H := by intro s0; rcases huniq with ⟨x, hx, _⟩; refine ⟨completeStateFrom x, ?_, ?_⟩formal statement (Lean)
104def UniqueSolutionXOR {n} (ψ : CNFWithXOR n) : Prop :=
proof body
Definition body.
105 ∃! a : Assignment n, evalCNF a ψ.φ = true ∧ satisfiesSystem a ψ.H
106
107end SAT
108end Complexity
109end IndisputableMonolith