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