valueOfXOR

formal source

  44
  45/-- Evaluate an XOR constraint under a partial assignment: returns `some b` if all
  46    vars are known, else none. -/
  47def valueOfXOR {n} (σ : PartialAssignment n) (X : XORConstraint n) : Option Bool :=
  48  if X.vars.all (fun v => (σ v).isSome) then
  49    some (X.vars.foldl (fun acc v => Bool.xor acc ((σ v).getD false)) false)
  50  else
  51    none
  52
  53/-- If exactly one variable of an XOR constraint is unknown, return that variable and the
  54    value needed to satisfy the parity given the known variables. -/
  55def xorMissing {n} (σ : PartialAssignment n) (X : XORConstraint n) : Option (Var n × Bool) :=
  56  let unknowns := X.vars.filter (fun v => (σ v).isNone)
  57  if h : unknowns.length = 1 then
  58    let v := unknowns.get ⟨0, by omega⟩
  59    let knownParity := X.vars.foldl (fun acc w =>
  60      if (σ w).isSome then Bool.xor acc ((σ w).getD false) else acc) false
  61    some (v, Bool.xor X.parity knownParity)
  62  else
  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