BPState

formal source

  10abbrev PartialAssignment (n : Nat) := Var n → Option Bool
  11
  12/-- Backward-propagation state over a CNF with XOR constraints. -/
  13structure BPState (n : Nat) where
  14  assign : PartialAssignment n
  15
  16/-- Update a partial assignment at variable `v` to value `b`. -/
  17def setVar {n} (σ : PartialAssignment n) (v : Var n) (b : Bool) : PartialAssignment n :=
  18  fun w => if w = v then some b else σ w
  19
  20@[simp] lemma setVar_same {n} (σ : PartialAssignment n) (v : Var n) (b : Bool) :
  21    setVar σ v b v = some b := by
  22  unfold setVar; simp
  23
  24lemma setVar_ne {n} (σ : PartialAssignment n) (v w : Var n) (b : Bool) (hvw : w ≠ v) :
  25    setVar σ v b w = σ w := by
  26  unfold setVar
  27  simp only [ite_eq_right_iff]
  28  intro heq
  29  exact absurd heq hvw
  30
  31/-- Evaluate a literal under a partial assignment. -/
  32def valueOfLit {n} (σ : PartialAssignment n) : Lit n → Option Bool
  33  | .pos v => σ v
  34  | .neg v => Option.map not (σ v)
  35
  36/-- Evaluate a clause under a partial assignment: returns `some b` if all literals
  37    are known, otherwise none. -/
  38def valueOfClause {n} (σ : PartialAssignment n) (C : Clause n) : Option Bool :=
  39  let vals := C.map (valueOfLit σ)
  40  if vals.all Option.isSome then
  41    some (vals.any fun o => o.getD false)
  42  else
  43    none