PeelingWitness
plain-language theorem explainer
The peeling witness predicate asserts the existence of a structure that orders input variables and pairs each with a locally determining constraint drawn from CNF clauses or XOR checks. Researchers establishing propagation completeness in SAT encodings would invoke this predicate to link local determination to global implication reachability. The definition reduces directly to the non-emptiness of the associated data type for the given inputs, reference assignment, formula and system.
Claim. Let $I$ be a finite set of input variables, $a$ a reference Boolean assignment, $C$ a CNF formula over $n$ variables, and $H$ an XOR system. The predicate holds precisely when the type of peeling data for $I$, $a$, $C$ and $H$ is inhabited.
background
In this module constraints are formalized as either CNF clauses or XOR checks. The InputSet abbreviation denotes the finite collection of input variables to which the propagation-completeness condition applies. Upstream, an Assignment is a total function from the variable set to Boolean values, as defined in both the RSatEncoding and CNF modules.
proof idea
The declaration is a one-line wrapper that states the predicate as the non-emptiness of the PeelingData type instantiated at the supplied inputs, reference assignment, CNF formula and XOR system.
why it matters
This predicate forms the common definition underlying the equivalence between peeling and forced arborescence. It is invoked directly in the theorems arborescence_implies_peeling and peeling_implies_arborescence, and supplies the target for the inductive construction in pc_implies_peeling. Within the Recognition Science development it supplies the abstract graph-theoretic object needed to equate the local PC condition with the existence of a spanning arborescence of determining implications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.