clauseUnit

formal source

  63    none
  64
  65/-- If exactly one literal of a clause is unknown and the others are false, return that var and required value. -/
  66def clauseUnit {n} (σ : PartialAssignment n) (C : Clause n) : Option (Var n × Bool) :=
  67  let vals := C.map (valueOfLit σ)
  68  let unknowns := C.zip vals |>.filter (fun ⟨_, o⟩ => o.isNone)
  69  if h1 : unknowns.length = 1 then
  70    if (vals.filter Option.isSome).all (fun o => o.getD false = false) then
  71      let l := unknowns.get ⟨0, by omega⟩
  72      match l.fst with
  73      | .pos v => some (v, true)
  74      | .neg v => some (v, false)
  75    else none
  76  else none
  77
  78/-- A (single) backpropagation step relation with guarded rules. -/
  79inductive BPStep {n} (φ : CNF n) (H : XORSystem n) : BPState n → BPState n → Prop
  80  | xor_push
  81      {s : BPState n}
  82      (X : XORConstraint n)
  83      (v : Var n)
  84      (b : Bool)
  85      (hX : X ∈ H)
  86      (hmiss : xorMissing s.assign X = some (v, b))
  87      : BPStep φ H s { assign := setVar s.assign v b }
  88  | clause_unit
  89      {s : BPState n}
  90      (C : Clause n)
  91      (v : Var n)
  92      (b : Bool)
  93      (hC : C ∈ φ.clauses)
  94      (hmiss : clauseUnit s.assign C = some (v, b))
  95      : BPStep φ H s { assign := setVar s.assign v b }
  96  -- Additional gate placeholders (to be refined with circuit semantics):