pc_implies_forcedArborescence
Propagation completeness for a mixed CNF-XOR SAT instance implies the existence of a forced arborescence on its input variables relative to a reference assignment. Complexity theorists analyzing constraint propagation in SAT solvers would cite this result when reducing local determination properties to global dependency structures. The proof is a one-line wrapper that unfolds the arborescence definition to a peeling witness and invokes the corresponding implication lemma.
claimLet $I$ be a finite set of input variables, $a$ a reference Boolean assignment, $C$ a CNF formula, and $H$ an XOR system. If the propagation-completeness condition holds for $I$, $a$, $C$, and $H$, then the forced-implication reachability property (a directed arborescence of locally determining constraints) holds for the same parameters.
background
In the module treating SAT constraints as either CNF clauses or XOR checks, an InputSet is the finset of variables designated as inputs for the property. The propagation-completeness condition (PC) states that for every nonempty subset $U$ of inputs there exists a constraint $K$ mentioning exactly one variable $v$ in $U$ such that $K$ determines the value of $v$ under the reference assignment. ForcedArborescence is defined to be identical to the PeelingWitness, which supplies a spanning, duplicate-free ordering of variables together with their determining constraints.
proof idea
The proof is a one-line wrapper. It unfolds the definition of ForcedArborescence (which equates it to PeelingWitness) and then applies the lemma pc_implies_peeling to obtain the required witness directly from the PC hypothesis.
why it matters in Recognition Science
This declaration records the direct implication PC implies ForcedArborescence stated in the module doc-comment. It supplies the structural bridge from local propagation completeness to a global arborescence of determining constraints, supporting further analysis of SAT encodings in the Recognition framework even though no downstream uses are recorded yet.
scope and limits
- Does not establish that any concrete SAT instance satisfies the PC condition.
- Does not supply an algorithm to construct or verify the arborescence.
- Does not extend the implication to constraint languages beyond CNF and XOR.
- Does not address the computational complexity of checking either side of the implication.
formal statement (Lean)
267theorem pc_implies_forcedArborescence {n}
268 (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) :
269 PC inputs aRef φ H → ForcedArborescence inputs aRef φ H := by
proof body
Term-mode proof.
270 unfold ForcedArborescence
271 exact pc_implies_peeling inputs aRef φ H
272
273end SAT
274end Complexity
275end IndisputableMonolith