mentionsVar

formal source

  27  X.vars.any (fun u => decide (u = v))
  28
  29/-- Whether a variable is mentioned in a mixed constraint. -/
  30def mentionsVar {n} (K : Constraint n) (v : Var n) : Bool :=
  31  match K with
  32  | .cnf C => mentionsVarClause C v
  33  | .xor X => mentionsVarXOR X v
  34
  35/-- Satisfaction semantics for mixed constraints. -/
  36def satisfiesConstraint {n} (a : Assignment n) (K : Constraint n) : Prop :=
  37  match K with
  38  | .cnf C => evalClause a C = true
  39  | .xor X => parityOf a X.vars = X.parity
  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`. -/