satJCost_zero_iff

formal source

  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
 112      have hsat := h c hc
 113      simp [hsat]
 114    simp [hfilt]
 115
 116/-! ## Part 1: Satisfiable → Zero Cost (O(n) recognition steps) -/
 117
 118/-- **THEOREM**: For a satisfiable formula, R̂ finds zero-cost assignment in O(n) steps.
 119    The constructive proof: if f.isSAT, then there exists a in 2^n candidates
 120    with satJCost f a = 0. R̂ evaluates this assignment directly.