constraintsOf

formal source

  48    a' v = aRef v
  49
  50/-- Collect all constraints arising from a CNF+XOR instance. -/
  51def constraintsOf {n} (φ : CNF n) (H : XORSystem n) : List (Constraint n) :=
  52  (φ.clauses.map Constraint.cnf) ++ (H.map Constraint.xor)
  53
  54/-- Set of input variables (as a finset) for PC property articulation. -/
  55abbrev InputSet (n : Nat) := Finset (Var n)
  56
  57/-- Propagation-Completeness condition (PC):
  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⟩