valueOfClause

formal source

  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
  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)