refactor(FineGrained,MCSP): extract general exp/exhaustive reductions and trim PermutationIndependentSet (#884)

Complexity.lean

@@ -743,6 +743,7 @@ public import Complexity.Computability.Complexity.Fagin.Verifier
 public import Complexity.Computability.Complexity.FineGrained
 public import Complexity.Computability.Complexity.FineGrained.Assignment
 public import Complexity.Computability.Complexity.FineGrained.BruteForce
+public import Complexity.Computability.Complexity.FineGrained.ExhaustiveSearch
 public import Complexity.Computability.Complexity.FineGrained.Exponents
 public import Complexity.Computability.Complexity.FineGrained.GraphProblems
 public import Complexity.Computability.Complexity.FineGrained.OrthogonalVectors

Complexity/Computability/Complexity/FineGrained/BruteForce.lean

@@ -8,25 +8,20 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Complexity.FineGrained.Assignment
+public import Complexity.Computability.Complexity.FineGrained.ExhaustiveSearch
 import Complexity.Computability.Complexity.Problems.SAT.PolyTime
-import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Binary
-import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
-import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
-import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain
 
 /-!
 # Exhaustive search for satisfiability
 
 Exhaustive search decides `SAT` by trying the `2 ^ n` numbered assignments of the `n` distinct
-variables of a formula (`Cslib.Logic.PL.CNF.satisfiable_iff_exists_bitsAssignment`). It iterates a
-polynomial-time step `2 ^ n` times with a binary counter
-(`Turing.MultiTapeTM.ComputableTidilyInO.iterate`), so it runs within time `2 ^ n` times a
-polynomial in the length of the encoded formula
-(`Cslib.Complexity.BruteForce.exists_computableInO_search`). Hence `SAT`, and every
-`k`-SAT, is decidable within time `2 ^ n` times a polynomial
+variables of a formula (`Cslib.Logic.PL.CNF.satisfiable_iff_exists_bitsAssignment`). By
+`Cslib.Complexity.DecidableInExpTime.of_exhaustiveSearch`, iterating the polynomial-time evaluation
+step (`Cslib.Complexity.computableInPolyTime_eval_bitsAssignment`) `2 ^ n` times decides `SAT`, and
+every `k`-SAT, within time `2 ^ n` times a polynomial in the length of the encoded formula
 (`Cslib.Complexity.SAT_decidableInExpTime_one`, `Cslib.Complexity.KSAT_decidableInExpTime_one`).
 
 ## Main definitions
@@ -35,8 +30,9 @@ polynomial in the length of the encoded formula
 
 ## Main results
 
+* `Cslib.Complexity.exists_le_mul_two_pow_of_polyBounded`: combining `2 ^ μ a + 1` rounds of a
+  polynomial with a polynomial into `2 ^ μ a` times a polynomial.
 * `Cslib.Complexity.BruteForce.search_eq_true_iff`: exhaustive search decides `SAT`.
-* `Cslib.Complexity.BruteForce.exists_computableInO_search`: its running time.
 * `Cslib.Complexity.SAT_decidableInExpTime_one`, `Cslib.Complexity.KSAT_decidableInExpTime_one`:
   `SAT` and `k`-SAT are decidable within time `2 ^ n` times a polynomial.
 
@@ -81,164 +77,47 @@ namespace BruteForce
 
 /-! ### The search -/
 
-/-- The state of exhaustive search: the formula, its distinct variables, the number of the next
-assignment to try, and whether a satisfying assignment was found. -/
-abbrev State : Type := (CNF ℕ × List ℕ) × (ℕ × Bool)
-
-/-- States encoded as framed tuples. -/
-private abbrev encState : State ↪ List Bool :=
-  encPair (encPair encCNF (encList encNat)) (encPair encNat encBool)
-
-/-- Try the next numbered assignment. -/
-def step (s : State) : State :=
-  (s.1, (s.2.1 + 1, s.2.2 || s.1.1.eval (bitsAssignment s.1.2 s.2.1)))
-
-/-- The initial state: no assignment tried yet. -/
-def init (φ : CNF ℕ) : State := ((φ, φ.distinctVars), (0, false))
-
 /-- **Exhaustive search**: try the `2 ^ n` assignments numbered by `i < 2 ^ n` on the `n` distinct
 variables of the formula. -/
-def search (φ : CNF ℕ) : Bool := (step^[2 ^ φ.distinctVars.length] (init φ)).2.2
-
-private theorem iterate_step_init (φ : CNF ℕ) (k : ℕ) :
-    step^[k] (init φ) = ((φ, φ.distinctVars),
-      (k, (List.range k).any fun i => φ.eval (bitsAssignment φ.distinctVars i))) := by
-  induction k with
-  | zero => rfl
-  | succ k ih =>
-    rw [Function.iterate_succ_apply', ih, step, List.range_succ, List.any_append]
-    simp
+def search (φ : CNF ℕ) : Bool :=
+  (List.range (2 ^ φ.distinctVars.length)).any fun i => φ.eval (bitsAssignment φ.distinctVars i)
 
 /-- **Exhaustive search decides `SAT`.** -/
 theorem search_eq_true_iff (φ : CNF ℕ) : search φ = true ↔ φ ∈ SAT := by
-  rw [search, iterate_step_init, mem_SAT,
+  rw [search, mem_SAT,
     CNF.satisfiable_iff_exists_bitsAssignment fun v hv => CNF.mem_distinctVars.mpr hv]
   simp
 
-/-! ### Running time -/
-
-open ComputableTidilyInPolyTime in
-/-- A step of exhaustive search is polynomial-time. -/
-private theorem computableTidilyInPolyTime_step
-    : ComputableTidilyInPolyTime step encState encState := by
-  have h : ComputableTidilyInPolyTime (fun s : State => s.1.1.eval (bitsAssignment s.1.2 s.2.1))
-      encState encBool :=
-    computableInPolyTime_eval_bitsAssignment.tidy.comp
-      (show ComputableTidilyInPolyTime (fun s : State => (s.1, s.2.1)) encState
-        (encPair (encPair encCNF (encList encNat)) encNat) by fun_prop)
-  unfold step
-  fun_prop
-
-attribute [local fun_prop] ComputableInPolyTime.tidy in
-open ComputableTidilyInPolyTime in
-/-- The initial state is computed in polynomial time. -/
-private theorem computableTidilyInPolyTime_init
-    : ComputableTidilyInPolyTime init encCNF encState := by
-  have hvars := SAT.computableInPolyTime_distinctVars.tidy
-  unfold init
-  fun_prop
-
-attribute [local fun_prop] ComputableInPolyTime.tidy in
-open ComputableTidilyInPolyTime in
-/-- The number `2 ^ n` of rounds is computed in binary in polynomial time. -/
-private theorem computableTidilyInPolyTime_count :
-    ComputableTidilyInPolyTime (fun φ => 2 ^ φ.distinctVars.length) encCNF encNat := by
-  fun_prop
-
-/-- **The running time of exhaustive search**: within time `2 ^ n` times a polynomial in the
-length of the encoded formula, on formulas with `n` variables. -/
-theorem exists_computableInO_search : ∃ e, ComputableInO search encCNF encBool
-    (fun φ => 2 ^ φ.numVars * ((encCNF φ).length + 1) ^ e)
-    fun φ => 2 ^ φ.numVars * ((encCNF φ).length + 1) ^ e := by
-  have this : ∃ e, ComputableTidilyInO search encCNF encBool
-      (fun φ => 2 ^ φ.numVars * ((encCNF φ).length + 1) ^ e) fun φ => 2 ^ φ.numVars *
-      ((encCNF φ).length + 1) ^ e := by
-    obtain ⟨d, _, hstep⟩ := computableTidilyInPolyTime_step.exists_degree
-    obtain ⟨d₀, _, hinit⟩ := computableTidilyInPolyTime_init.exists_degree
-    obtain ⟨d₁, _, hcount⟩ := computableTidilyInPolyTime_count.exists_degree
-    obtain ⟨d₂, _, hans⟩ :=
-      (show ComputableTidilyInPolyTime (fun s : State => s.2.2) encState encBool
-      by fun_prop).exists_degree
-    obtain ⟨cv, dv, hvs⟩ :=
-      SAT.computableInPolyTime_distinctVars.tidy.polyBounded_length.exists_le
-    set size : CNF ℕ → ℕ := fun φ => (encCNF φ).length
-    set B : CNF ℕ → ℕ := fun φ => (2 * cv + 13) * (size φ + 1) ^ (dv + 1)
-    have hn (φ : CNF ℕ) : φ.distinctVars.length ≤ size φ := by
-      rw [CNF.length_distinctVars]
-      exact φ.numVars_le_length_vars.trans (SAT.length_vars_le φ)
-    have hstate : ∀ φ, ∀ k ≤ 2 ^ φ.distinctVars.length,
-        (encState (step^[k] (init φ))).length ≤ B φ := by
-      intro φ k hk
-      have hK := ComputableTidilyInO.length_encNat_mono hk
-      rw [encNat_two_pow] at hK
-      have hV := hvs φ
-      have h₁ : size φ + 1 ≤ (size φ + 1) ^ (dv + 1) := by
-        simpa using Nat.pow_le_pow_right (Nat.succ_pos (size φ)) (Nat.le_add_left 1 dv)
-      have h₂ : (size φ + 1) ^ dv ≤ (size φ + 1) ^ (dv + 1) :=
-        Nat.pow_le_pow_right (Nat.succ_pos _) (Nat.le_succ dv)
-      have h₃ := Nat.mul_le_mul_left cv h₂
-      have h₄ := hn φ
-      rw [iterate_step_init]
-      simp only [List.length_append, List.length_replicate, List.length_singleton] at hK
-      simp only [encState, length_encPair, encBool_apply, List.length_singleton, B, size]
-        at hV h₁ h₃ h₄ ⊢
-      nlinarith
-    have hiter := ComputableTidilyInO.iterate hcount.inO hinit.inO hstep.inO
-      (R := fun φ => (B φ + 1) ^ d) (Q := fun φ => (B φ + 1) ^ d) (B := B)
-      (fun φ k hk => Nat.pow_le_pow_left (Nat.add_le_add_right (hstate φ k hk) 1) d)
-      (fun φ k hk => Nat.pow_le_pow_left (Nat.add_le_add_right (hstate φ k hk) 1) d) hstate
-    have h := hans.inO.comp hiter
-    have hB : PolyBounded size B := .of_forall_le (2 * cv + 13) (dv + 1) fun φ => le_rfl
-    have hpow (j : ℕ) : PolyBounded size fun φ => (B φ + 1) ^ j :=
-      ((PolyBounded.of_polynomiallyBounded id (bound := fun x => (x + 1) ^ j) (by fun_prop)).comp
-        hB).mono fun φ => le_rfl
-    have hL (j : ℕ) : PolyBounded size fun φ => (size φ + 1) ^ j :=
-      .of_forall_le 1 j fun φ => by simp
-    obtain ⟨c, e, hT⟩ := exists_le_mul_two_pow_of_polyBounded (size := size) (μ := CNF.numVars)
-      ((hpow d).add (hB.add (.of_forall_le 4 2 fun φ => le_rfl)))
-      ((hL d₁).add ((hL d₀).add (hpow d₂)))
-      (T := fun φ => ((encCNF φ).length + 1) ^ d₁ + ((encCNF φ).length + 1) ^ d₀ +
-        (2 ^ φ.distinctVars.length + 1) * ((B φ + 1) ^ d + B φ +
-          ((encNat (2 ^ φ.distinctVars.length)).length + 1) ^ 2) +
-        ((encState (step^[2 ^ φ.distinctVars.length] (init φ))).length + 1) ^ d₂)
-      (fun φ => by
-        have hK : ((encNat (2 ^ φ.distinctVars.length)).length + 1) ^ 2 ≤
-            4 * (size φ + 1) ^ 2 := by
-          rw [encNat_two_pow]
-          simp only [List.length_append, List.length_replicate, List.length_singleton]
-          calc (φ.distinctVars.length + 1 + 1) ^ 2 ≤ (2 * (size φ + 1)) ^ 2 :=
-                Nat.pow_le_pow_left (by have := hn φ; omega) 2
-            _ = 4 * (size φ + 1) ^ 2 := by ring
-        have hS := Nat.pow_le_pow_left (Nat.add_le_add_right (hstate φ _ le_rfl) 1) d₂
-        rw [CNF.length_distinctVars] at hK hS ⊢
-        have := Nat.mul_le_mul_left (2 ^ φ.numVars + 1)
-          (Nat.add_le_add_left hK ((B φ + 1) ^ d + B φ))
-        simp only [size] at this hS ⊢
-        nlinarith)
-    refine ⟨e, (h.mono c (fun φ => ?_) fun φ => ?_).of_enc_eq fun φ => rfl⟩
-    all_goals
-      have h₁ := hT φ
-      simp only [size] at h₁
-      generalize 2 ^ φ.distinctVars.length = N at h₁ ⊢
-      generalize (encNat N).length = K at h₁ ⊢
-      obtain ⟨X, hX⟩ : ∃ X, (B φ + 1) ^ d + B φ = X := ⟨_, rfl⟩
-      rw [hX] at h₁
-      have h₂ : K ≤ (K + 1) ^ 2 := by nlinarith
-      have h₃ : X + (K + 1) ^ 2 ≤ (N + 1) * (X + (K + 1) ^ 2) := Nat.le_mul_of_pos_left _ (by omega)
-      nlinarith
-  simpa only [computableInO_iff_computableTidilyInO] using this
-
 end BruteForce
 
+open ComputableTidilyInPolyTime in
 /-- **`SAT` by exhaustive search**: `SAT` is decidable within time `2 ^ n` times a polynomial in the
 length of the encoded formula, on formulas with `n` variables. -/
 theorem SAT_decidableInExpTime_one : DecidableInExpTime SAT encCNF CNF.numVars 1 := by
-  obtain ⟨e, h⟩ := BruteForce.exists_computableInO_search
-  refine DecidableInExpTime.of_computableInO h (fun φ => (BruteForce.search_eq_true_iff φ).symm) 1 e
-    fun φ => ?_
-  rw [one_mul, Real.rpow_natCast]
-  push_cast
-  rw [one_mul]
+  have hB : DecidableInExpTime
+      {p : (CNF ℕ × List ℕ) × ℕ | p.1.1.eval (bitsAssignment p.1.2 p.2) = true}
+      (encPair (encPair encCNF (encList encNat)) encNat) (fun _ => 0) 0 :=
+    .of_computableInPolyTime computableInPolyTime_eval_bitsAssignment (fun _ => Iff.rfl)
+  have hf : ComputableInPolyTime
+      (fun q : CNF ℕ × ℕ => ((q.1, q.1.distinctVars), q.2))
+      (encPair encCNF encNat) (encPair (encPair encCNF (encList encNat)) encNat) := by
+    have := SAT.computableInPolyTime_distinctVars.tidy
+    exact .of_tidy (by fun_prop)
+  have hν : ComputableInPolyTime CNF.numVars encCNF encUnary := by
+    have := SAT.computableInPolyTime_distinctVars.tidy
+    refine .of_tidy ?_
+    have heq : (CNF.numVars : CNF ℕ → ℕ) = fun φ => φ.distinctVars.length := by
+      funext φ; exact φ.length_distinctVars.symm
+    rw [heq]
+    fun_prop
+  have hfA (φ : CNF ℕ) : φ ∈ SAT ↔ ∃ r < 2 ^ φ.numVars,
+      ((φ, φ.distinctVars), r) ∈
+        {p : (CNF ℕ × List ℕ) × ℕ | p.1.1.eval (bitsAssignment p.1.2 p.2) = true} := by
+    rw [mem_SAT, ← φ.length_distinctVars,
+      CNF.satisfiable_iff_exists_bitsAssignment fun v hv => CNF.mem_distinctVars.mpr hv]
+    rfl
+  simpa using hB.of_exhaustiveSearch hf hν hfA (c := 0) (fun _ _ => Nat.zero_le _)
+    (M := 1) (K := 0) (fun φ => by simp) le_rfl
 
 open ComputableTidilyInPolyTime in
 /-- Checking that every clause has at most `k` literals is polynomial-time. -/