landscapeDepth_unsat

formal source

  64  · exact Nat.cast_nonneg _
  65
  66/-- For UNSAT formulas, landscape depth is ≥ 1. -/
  67theorem landscapeDepth_unsat {n : ℕ} (f : CNFFormula n) (h : f.isUNSAT) :
  68    1 ≤ LandscapeDepth f := by
  69  unfold LandscapeDepth
  70  have hcard_pos : (0 : ℝ) < (Finset.univ.card (α := Fin n → Bool) : ℝ) := by
  71    exact_mod_cast Finset.card_pos.mpr ⟨fun _ => false, Finset.mem_univ _⟩
  72  rw [le_div_iff₀ hcard_pos]
  73  calc (1 : ℝ) * ↑(Finset.univ.card (α := Fin n → Bool))
  74      = Finset.univ.sum (fun _ : Fin n → Bool => (1 : ℝ)) := by
  75          simp [Finset.sum_const, smul_eq_mul]
  76    _ ≤ Finset.univ.sum (fun a : Fin n → Bool => satJCost f a) := by
  77          apply Finset.sum_le_sum; intro a _
  78          exact unsat_cost_lower_bound f h a
  79
  80/-! ## Certificate -/
  81
  82structure JFrustrationCert where
  83  unsat_ge_one : ∀ (n : ℕ) (f : CNFFormula n), f.isUNSAT → JFrust f ≥ 1
  84  sat_eq_zero : ∀ (n : ℕ) (f : CNFFormula n), f.isSAT → JFrust f = 0
  85  depth_nonneg : ∀ (n : ℕ) (f : CNFFormula n), 0 ≤ LandscapeDepth f
  86  depth_unsat : ∀ (n : ℕ) (f : CNFFormula n), f.isUNSAT → 1 ≤ LandscapeDepth f
  87
  88def jfrustrationCert : JFrustrationCert where
  89  unsat_ge_one := fun n f h => jfrust_unsat_ge_one f h
  90  sat_eq_zero := fun n f h => jfrust_sat_eq_zero f h
  91  depth_nonneg := fun n f => landscapeDepth_nonneg f
  92  depth_unsat := fun n f h => landscapeDepth_unsat f h
  93
  94end -- noncomputable section
  95
  96end JFrustration
  97end Complexity