PC
PC defines the propagation-completeness condition for a hybrid CNF and XOR constraint system on n variables. Researchers analyzing unique-solution SAT instances or building peeling orders for arborescence witnesses cite this definition when proving backpropagation success. It is stated directly as a universal quantification: every nonempty input subset U admits a constraint K that isolates and determines exactly one variable v from U under the reference assignment.
claimLet $I$ be a finite set of input variables, $a$ a reference Boolean assignment, $F$ a CNF formula, and $X$ an XOR system. The propagation-completeness condition holds when, for every nonempty $Usubseteq I$, there exists a constraint $K$ drawn from the clauses of $F$ and the equations of $X$ together with a variable $v in U$ such that $K$ mentions $v$ but no other member of $U$ and $K$ fixes the value of $v$ under $a$.
background
Constraints in this module are formed by mapping CNF clauses or XOR equations into a uniform Constraint type. InputSet n is the Finset of designated input variables (Var n = Fin n). An Assignment n is a total function from variables to Booleans; the reference assignment aRef is assumed unique for the instance. The auxiliary function constraintsOf concatenates the mapped CNF clauses with the XOR constraints.
proof idea
The definition is given directly by the displayed universal quantification over nonempty Finsets U. It requires an existential witness K belonging to constraintsOf φ H and v in U satisfying the three mentions and determines predicates. No upstream lemmas are invoked; the body is the primitive statement of the property.
why it matters in Recognition Science
PC is the hypothesis used by backprop_succeeds_from_PC to conclude BackpropSucceeds once a unique solution exists. It also supplies the inductive step for buildPeelingResult, which constructs the ForcedArborescenceWitness by successive extraction of isolating constraints. The definition therefore closes the semantic link between propagation completeness and forced implication in the SAT encoding layer.
scope and limits
- Does not assert existence or uniqueness of solutions.
- Does not apply to constraint languages beyond CNF and XOR.
- Does not bound the computational cost of verifying the condition.
- Does not extend to infinite or continuous variable domains.
formal statement (Lean)
61def PC {n}
62 (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) : Prop :=
proof body
Definition body.
63 ∀ (U : Finset (Var n)),
64 U ⊆ inputs →
65 U.Nonempty →
66 ∃ (K : Constraint n),
67 K ∈ constraintsOf φ H ∧
68 ∃ v ∈ U,
69 mentionsVar K v = true ∧
70 (∀ w ∈ U, w ≠ v → mentionsVar K w = false) ∧
71 determinesVar aRef K v
72
73/-- Peeling witness structure: a list of variables and constraints meeting the peeling conditions. -/