XORConstraint

formal source

   6namespace SAT
   7
   8/-- An XOR constraint over `n` variables: parity of a variable subset equals `parity`. -/
   9structure XORConstraint (n : Nat) where
  10  vars   : List (Var n)
  11  parity : Bool
  12deriving Repr
  13
  14/-- A system of XOR constraints. -/
  15abbrev XORSystem (n : Nat) := List (XORConstraint n)
  16
  17/-- Compute the XOR (parity) of selected variables of assignment `a`. -/
  18def parityOf {n} (a : Assignment n) (S : List (Var n)) : Bool :=
  19  S.foldl (fun acc v => Bool.xor acc (a v)) false
  20
  21/-- A single XOR constraint is satisfied by `a` iff the parity matches. -/
  22def satisfiesXOR {n} (a : Assignment n) (c : XORConstraint n) : Prop :=
  23  parityOf a c.vars = c.parity
  24
  25/-- An assignment satisfies an XOR system when all constraints hold. -/
  26def satisfiesSystem {n} (a : Assignment n) (H : XORSystem n) : Prop :=
  27  ∀ c ∈ H, satisfiesXOR a c
  28
  29/-! ## XOR Parity Lemmas -/
  30
  31/-- XOR is self-inverse: a ⊕ a = false -/
  32@[simp] lemma Bool.xor_self (a : Bool) : Bool.xor a a = false := by cases a <;> rfl
  33
  34/-- XOR with false is identity -/
  35@[simp] lemma Bool.xor_false' (a : Bool) : Bool.xor a false = a := by cases a <;> rfl
  36
  37/-- false XOR a = a -/
  38@[simp] lemma Bool.false_xor (a : Bool) : Bool.xor false a = a := by cases a <;> rfl
  39