determinesVar

formal source

  40
  41/-- The constraint K determines variable v w.r.t. reference assignment `aRef`:
  42    fixing all non-v variables to `aRef` and requiring `K` forces `v = aRef v`. -/
  43def determinesVar {n}
  44  (aRef : Assignment n) (K : Constraint n) (v : Var n) : Prop :=
  45  ∀ (a' : Assignment n),
  46    (∀ w : Var n, w ≠ v → a' w = aRef w) →
  47    satisfiesConstraint a' K →
  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. -/