JFrust

formal source

  31
  32/-- J-Frustration of a CNF formula.
  33    Binary classification: 0 for SAT, 1 for UNSAT. -/
  34def JFrust {n : ℕ} (f : CNFFormula n) : ℝ :=
  35  haveI := Classical.propDecidable f.isSAT
  36  if f.isSAT then 0 else 1
  37
  38theorem jfrust_unsat_ge_one {n : ℕ} (f : CNFFormula n) (h : f.isUNSAT) :
  39    JFrust f ≥ 1 := by
  40  unfold JFrust
  41  haveI := Classical.propDecidable f.isSAT
  42  have hns : ¬f.isSAT := by
  43    intro ⟨a, ha⟩; exact absurd ha (by simp [h a])
  44  simp [hns]
  45
  46theorem jfrust_sat_eq_zero {n : ℕ} (f : CNFFormula n) (h : f.isSAT) :
  47    JFrust f = 0 := by
  48  unfold JFrust
  49  haveI := Classical.propDecidable f.isSAT
  50  simp [h]
  51
  52/-! ## Landscape Depth -/
  53
  54/-- The average J-cost across all assignments. -/
  55def LandscapeDepth {n : ℕ} (f : CNFFormula n) : ℝ :=
  56  Finset.univ.sum (fun a : Fin n → Bool => satJCost f a) /
  57  (Finset.univ.card (α := Fin n → Bool) : ℝ)
  58
  59theorem landscapeDepth_nonneg {n : ℕ} (f : CNFFormula n) :
  60    0 ≤ LandscapeDepth f := by
  61  unfold LandscapeDepth
  62  apply div_nonneg
  63  · exact Finset.sum_nonneg (fun a _ => satJCost_nonneg f a)
  64  · exact Nat.cast_nonneg _