PeelingData
PeelingData encodes an ordered sequence of variables paired with determining constraints that cover exactly the input set for a propagation-complete CNF-XOR instance. Researchers analyzing forced implications in SAT would cite this structure when establishing reachability from a reference assignment. The definition proceeds by specifying lists of variables and constraints together with predicates ensuring distinctness, equal lengths, full coverage, and stepwise mention plus determination properties.
claimLet $n$ be a natural number, $I$ an input set of variables, $a$ a reference assignment, $C$ a CNF formula, and $X$ an XOR system. A peeling data structure consists of lists $v_1, dots, v_m$ and $K_1, dots, K_m$ of equal length with the $v_i$ distinct such that the variables exactly match $I$, and for each index $k$ the constraint $K_k$ mentions $v_k$, mentions none of the later variables, and determines $v_k$ under $a$.
background
The module defines constraints as either CNF clauses or XOR checks. InputSet is the finset of input variables for which the propagation-completeness condition is articulated: for every nonempty $U$ subset of inputs there exists a constraint $K$ and $v$ in $U$ such that $K$ mentions $v$, mentions no other element of $U$, and determines $v$ with respect to the reference assignment. Assignment is the type of boolean functions on the variables, drawn from both the CNF and RSatEncoding modules.
proof idea
The declaration is a structure definition. Its fields directly encode the required properties: distinct variables via Nodup, matching lengths, exact coverage of the input set, and the per-position conditions on mentions and determination. No lemmas are applied; the structure itself serves as the witness.
why it matters in Recognition Science
PeelingData supplies the concrete data for the PeelingWitness proposition, which asserts existence of such a structure. This formalizes forced-implication reachability as a directed arborescence of locally determining constraints from output to every input. In the Recognition Science setting it contributes to encoding propagation completeness for SAT instances that may model aspects of the forcing chain.
scope and limits
- Does not assert existence of a peeling order for every PC instance.
- Does not compute the lists; it only validates a supplied candidate.
- Does not handle empty input sets or other constraint languages.
- Does not incorporate cost measures from the algebra module.
formal statement (Lean)
74structure PeelingData {n : Nat} (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) where
75 vars : List (Var n)
76 constrs : List (Constraint n)
77 nodup : vars.Nodup
78 len_eq : vars.length = constrs.length
79 cover : ∀ v : Var n, v ∈ inputs ↔ v ∈ vars
80 step : ∀ k (hk : k < vars.length),
81 let v := vars.get ⟨k, hk⟩
proof body
Definition body.
82 let K := constrs.get ⟨k, by omega⟩
83 mentionsVar K v = true ∧
84 (∀ w, w ∈ vars.drop k.succ → mentionsVar K w = false) ∧
85 determinesVar aRef K v
86
87/-- Peeling witness (Prop-level): there exists a peeling structure. -/