satJCost

formal source

  78/-- The J-cost of a formula under an assignment.
  79    J = 0 iff all clauses are satisfied (zero defect = satisfying assignment).
  80    J = (number of unsatisfied clauses) > 0 iff UNSAT under this assignment. -/
  81noncomputable def satJCost {n : ℕ} (f : CNFFormula n) (a : Assignment n) : ℝ :=
  82  (f.clauses.filter (fun c => !c.satisfiedBy a)).length
  83
  84/-- J-cost is nonneg (number of unsatisfied clauses ≥ 0). -/
  85theorem satJCost_nonneg {n : ℕ} (f : CNFFormula n) (a : Assignment n) :
  86    0 ≤ satJCost f a := by
  87  unfold satJCost; exact_mod_cast Nat.zero_le _
  88
  89/-- J-cost = 0 iff the assignment satisfies all clauses. -/
  90theorem satJCost_zero_iff {n : ℕ} (f : CNFFormula n) (a : Assignment n) :
  91    satJCost f a = 0 ↔ f.satisfiedBy a = true := by
  92  unfold satJCost CNFFormula.satisfiedBy
  93  constructor
  94  · intro h
  95    have hlen : (f.clauses.filter (fun c => !c.satisfiedBy a)).length = 0 := by exact_mod_cast h
  96    have hfilt : (f.clauses.filter (fun c => !c.satisfiedBy a)) = [] :=
  97      List.eq_nil_iff_length_eq_zero.mpr hlen
  98    rw [List.all_eq_true]
  99    intro c hc
 100    by_contra hc2
 101    push_neg at hc2
 102    have hmem : c ∈ f.clauses.filter (fun c => !c.satisfiedBy a) := by
 103      simp only [List.mem_filter]
 104      exact ⟨hc, by simp [hc2]⟩
 105    rw [hfilt] at hmem
 106    simp at hmem
 107  · intro h
 108    rw [List.all_eq_true] at h
 109    have hfilt : (f.clauses.filter (fun c => !c.satisfiedBy a)) = [] := by
 110      rw [List.filter_eq_nil_iff]
 111      intro c hc