jcostEdgeWeight

formal source

  53/-! ## J-Cost Edge Weights -/
  54
  55/-- The J-cost edge weight when flipping bit k. -/
  56def jcostEdgeWeight {n : ℕ} (f : CNFFormula n) (a : Assignment n) (k : Fin n) : ℝ :=
  57  |satJCost f a - satJCost f (flipBit a k)|
  58
  59theorem jcostEdgeWeight_nonneg {n : ℕ} (f : CNFFormula n) (a : Assignment n)
  60    (k : Fin n) : 0 ≤ jcostEdgeWeight f a k :=
  61  abs_nonneg _
  62
  63theorem jcostEdgeWeight_symm {n : ℕ} (f : CNFFormula n) (a : Assignment n)
  64    (k : Fin n) : jcostEdgeWeight f a k = jcostEdgeWeight f (flipBit a k) k := by
  65  unfold jcostEdgeWeight; rw [flipBit_flipBit]; exact (abs_sub_comm _ _).symm
  66
  67theorem jcostEdgeWeight_le_clauses {n : ℕ} (f : CNFFormula n) (a : Assignment n)
  68    (k : Fin n) : jcostEdgeWeight f a k ≤ f.clauses.length := by
  69  unfold jcostEdgeWeight satJCost
  70  have h1 : (↑(f.clauses.filter (fun c => !c.satisfiedBy a)).length : ℝ) ≤
  71             ↑f.clauses.length := Nat.cast_le.mpr (List.length_filter_le _ _)
  72  have h2 : (↑(f.clauses.filter (fun c => !c.satisfiedBy (flipBit a k))).length : ℝ) ≤
  73             ↑f.clauses.length := Nat.cast_le.mpr (List.length_filter_le _ _)
  74  have h1nn : (0 : ℝ) ≤ ↑(f.clauses.filter (fun c => !c.satisfiedBy a)).length :=
  75    Nat.cast_nonneg _
  76  have h2nn : (0 : ℝ) ≤ ↑(f.clauses.filter
  77    (fun c => !c.satisfiedBy (flipBit a k))).length := Nat.cast_nonneg _
  78  rw [abs_le]; constructor <;> linarith
  79
  80/-! ## Tight Variable-Degree Bound -/
  81
  82/-- Whether a clause contains a given variable (in any polarity). -/
  83def containsVar {n : ℕ} (c : Clause n) (j : Fin n) : Bool :=
  84  c.literals.any (fun lit => lit.1 == j)
  85
  86/-- The variable degree: number of clauses containing variable j. -/