PC

formal source

  58    For every nonempty U ⊆ inputs, there exists a constraint K and v ∈ U such that
  59    (i) K mentions v, (ii) K mentions no other element of U, and (iii) K determines v
  60    with respect to the unique reference assignment `aRef`. -/
  61def PC {n}
  62  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) : Prop :=
  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. -/
  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⟩
  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. -/
  88def PeelingWitness {n}
  89  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) : Prop :=
  90  Nonempty (PeelingData inputs aRef φ H)
  91