From b803c16a45e7f60ef74628df4ed83bc3f5f3f2a2 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sat, 24 Oct 2026 23:27:50 +0000 Subject: [PATCH 1/2] =?UTF-8?q?feat(FineGrained):=20Sch=C3=B6ning's=20rand?= =?UTF-8?q?om=20walk=20for=203-SAT=20succeeds=20with=20probability=20(3/4)?= =?UTF-8?q?^n/(3n+1)=20(#894)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Define Schöning's local search and one trial, compare the walk with a biased random walk on Hamming distances by induction on the step budget, count paths, bound the middle binomial weight, and average over the uniform start. AI-assisted: Jetski (worker-jetski-17d3679e). --- Complexity.lean | 1 + .../Complexity/FineGrained/Schoening.lean | 503 ++++++++++++++++++ ComplexityTests/Schoening.lean | 54 ++ ROADMAP.md | 2 +- references.bib | 9 + 5 files changed, 568 insertions(+), 1 deletion(-) create mode 100644 Complexity/Computability/Complexity/FineGrained/Schoening.lean create mode 100644 ComplexityTests/Schoening.lean diff --git a/Complexity.lean b/Complexity.lean index c1564dfb09..8f40eb968e 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -742,6 +742,7 @@ public import Complexity.Computability.Complexity.FineGrained.GraphProblems public import Complexity.Computability.Complexity.FineGrained.OrthogonalVectors public import Complexity.Computability.Complexity.FineGrained.PermutationIndependentSet public import Complexity.Computability.Complexity.FineGrained.Reduction +public import Complexity.Computability.Complexity.FineGrained.Schoening public import Complexity.Computability.Complexity.FineGrained.Sparsification public import Complexity.Computability.Complexity.HardnessEncoding.PolyTime public import Complexity.Computability.Complexity.HardnessEncoding.Program diff --git a/Complexity/Computability/Complexity/FineGrained/Schoening.lean b/Complexity/Computability/Complexity/FineGrained/Schoening.lean new file mode 100644 index 0000000000..dbe71a1eb5 --- /dev/null +++ b/Complexity/Computability/Complexity/FineGrained/Schoening.lean @@ -0,0 +1,503 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Logics.Propositional.CNF +public import Mathlib.InformationTheory.Hamming +public import Complexity.Probability.PMF +import Complexity.Probability.PMF.Event +import Mathlib.Algebra.BigOperators.Fin +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# Schöning's random walk for 3-SAT + +Schöning's algorithm searches for a satisfying assignment of a CNF formula by local search with +restarts. One *trial* draws a uniformly random assignment and then performs `3 n` steps, where `n` +is the number of variables. Each step stops if the formula is satisfied. Otherwise it takes the +first unsatisfied clause, chooses one of its literal occurrences uniformly, and flips that +variable (`Cslib.Complexity.Schoening.walk`, `Cslib.Complexity.Schoening.trial`) +[Schöning][Schoening1999]. + +For a satisfiable formula whose clauses have at most three literals, a trial succeeds with +probability at least `(3 / 4) ^ n / (3 n + 1)` (`Cslib.Complexity.Schoening.trial_success`). So +about `(4 / 3) ^ n` independent trials find a satisfying assignment with high probability, +exponentially faster than the `2 ^ n` assignments of brute force. Schöning states the bound up to a +polynomial factor; the factor `1 / (3 n + 1)` here is this file's explicit constant. + +The proof compares the walk with a biased random walk on distances. Fix a satisfying assignment +`σ⋆`. A step changes the Hamming distance to `σ⋆` by one. Since `σ⋆` satisfies the chosen clause +and the current assignment does not, at least one of its at most three literals moves toward `σ⋆`. +Let `hit t d` be the probability that a walk on `ℕ`, stepping down with probability `1 / 3` and up +with probability `2 / 3`, reaches `0` from `d` within `t` steps (`Cslib.Complexity.Schoening.hit`). +It is antitone in `d` (`hit_succ_le`), so by induction on `t` the trial walk succeeds with +probability at least `hit t (dist σ σ⋆)` (`hit_le_succeedProb`). No coupling is needed. + +A path of `2 j` down-steps and `j` up-steps reaches `0` from `j`, so +`hit (3 j) j ≥ C(3j, j) (1/3)^{2j} (2/3)^j` (`choose_mul_le_hit`). The middle binomial weight is the +largest of the `3 j + 1` terms of `(1 + 2) ^ {3j}`, so `C(3j, j) 4^j (3j + 1) ≥ 27^j` +(`pow_le_choose_mul`), and `hit (3 j) j ≥ 2^{-j} / (3 j + 1)`. Averaging `2^{-dist}` over a +uniform start gives `(3/4)^n`, a product over the coordinates. + +## Main definitions + +* `Cslib.Complexity.Schoening.walk`: `t` steps of the local search from an assignment. +* `Cslib.Complexity.Schoening.trial`: a uniform start followed by `3 n` steps. +* `Cslib.Complexity.Schoening.hit`: hitting probabilities of the biased walk. + +## Main results + +* `Cslib.Complexity.Schoening.hit_le_succeedProb`: the local search dominates the biased walk. +* `Cslib.Complexity.Schoening.choose_mul_le_hit`: path counting for the biased walk. +* `Cslib.Complexity.Schoening.pow_le_choose_mul`: `27^j ≤ C(3j, j) 4^j (3j + 1)`. +* `Cslib.Complexity.Schoening.trial_success`: a trial succeeds with probability at least + `(3 / 4) ^ n / (3 n + 1)`. + +## References + +* [U. Schöning, *A probabilistic algorithm for k-SAT and constraint satisfaction + problems*][Schoening1999] +-/ + +@[expose] public section + +namespace Cslib.Complexity.Schoening + +open Cslib.Logic.PL Finset + +variable {V : Type*} [Fintype V] [DecidableEq V] + +/-! ### The algorithm -/ + +/-- Flip the value of the variable `v`. -/ +def flip (σ : V → Bool) (v : V) : V → Bool := Function.update σ v (!σ v) + +/-- The first clause of `φ` that `σ` falsifies, if any. -/ +def firstUnsat (φ : CNF V) (σ : V → Bool) : Option (Clause V) := + φ.find? fun c => !c.eval σ + +/-- Flip the variable of a uniformly chosen literal occurrence of `c`. The empty clause, which no +assignment satisfies, leaves the assignment unchanged. -/ +noncomputable def flipStep (c : Clause V) (σ : V → Bool) : PMF (V → Bool) := + if h : c.length = 0 then PMF.pure σ else + haveI : NeZero c.length := ⟨h⟩ + (Probability.PMF.uniformOfFintype (Fin c.length)).map fun i => flip σ (c.get i).1 + +/-- **Schöning's local search**: `t` steps from `σ`. Each step stops if `φ` is satisfied, and +otherwise flips a uniformly chosen variable of the first unsatisfied clause. -/ +noncomputable def walk (φ : CNF V) : ℕ → (V → Bool) → PMF (V → Bool) + | 0, σ => PMF.pure σ + | t + 1, σ => + match firstUnsat φ σ with + | none => PMF.pure σ + | some c => (flipStep c σ).bind (walk φ t) + +/-- **One trial of Schöning's algorithm**: a uniformly random assignment followed by `3 n` steps of +local search, where `n` is the number of variables. -/ +noncomputable def trial (φ : CNF V) : PMF (V → Bool) := + (Probability.PMF.uniformOfFintype (V → Bool)).bind (walk φ (3 * Fintype.card V)) + +/-- The probability that `μ` produces an assignment satisfying `φ`. -/ +noncomputable def succeedProb (φ : CNF V) (μ : PMF (V → Bool)) : ℝ := + (μ.toOuterMeasure {σ | φ.eval σ = true}).toReal + +/-! ### The biased walk -/ + +/-- The probability that a walk on `ℕ` that steps down with probability `1 / 3` and up with +probability `2 / 3` reaches `0` from `d` within `t` steps. -/ +noncomputable def hit : ℕ → ℕ → ℝ + | _, 0 => 1 + | 0, _ + 1 => 0 + | t + 1, d + 1 => hit t d / 3 + 2 * hit t (d + 2) / 3 + +@[simp] theorem hit_zero_right (t : ℕ) : hit t 0 = 1 := by cases t <;> rfl + +@[simp] theorem hit_zero_succ (d : ℕ) : hit 0 (d + 1) = 0 := rfl + +theorem hit_succ_succ (t d : ℕ) : hit (t + 1) (d + 1) = hit t d / 3 + 2 * hit t (d + 2) / 3 := + rfl + +theorem hit_nonneg (t d : ℕ) : 0 ≤ hit t d := by + induction t generalizing d with + | zero => cases d <;> simp + | succ t ih => + cases d with + | zero => simp + | succ d => + rw [hit_succ_succ] + have := ih d + have := ih (d + 2) + positivity + +theorem hit_le_one (t d : ℕ) : hit t d ≤ 1 := by + induction t generalizing d with + | zero => cases d <;> simp + | succ t ih => + cases d with + | zero => simp + | succ d => + rw [hit_succ_succ] + linarith [ih d, ih (d + 2)] + +/-- Hitting `0` is less likely from farther away. -/ +theorem hit_succ_le (t d : ℕ) : hit t (d + 1) ≤ hit t d := by + induction t generalizing d with + | zero => simpa using hit_nonneg 0 d + | succ t ih => + cases d with + | zero => simpa using hit_le_one (t + 1) 1 + | succ d => + rw [hit_succ_succ, hit_succ_succ] + linarith [ih d, ih (d + 2)] + +theorem hit_antitone (t : ℕ) : Antitone (hit t) := + antitone_nat_of_succ_le (hit_succ_le t) + +/-- Hitting `0` is more likely with more time. -/ +theorem hit_le_hit_succ (t d : ℕ) : hit t d ≤ hit (t + 1) d := by + induction t generalizing d with + | zero => cases d <;> simp [hit_nonneg] + | succ t ih => + cases d with + | zero => simp + | succ d => + rw [hit_succ_succ, hit_succ_succ (t + 1)] + linarith [ih d, ih (d + 2)] + +theorem hit_monotone (d : ℕ) : Monotone fun t => hit t d := + monotone_nat_of_le_succ fun t => hit_le_hit_succ t d + +/-- A single binomial weight is at most one. -/ +private theorem choose_mul_pow_le_one (m a b : ℕ) (h : a + b = m) : + (m.choose a : ℝ) * (1 / 3) ^ b * (2 / 3) ^ a ≤ 1 := by + have hsum := add_pow (2 / 3 : ℝ) (1 / 3) m + rw [show (2 / 3 : ℝ) + 1 / 3 = 1 by norm_num, one_pow] at hsum + have ha : a ∈ range (m + 1) := mem_range.mpr (by omega) + have hle := single_le_sum (f := fun i => (2 / 3 : ℝ) ^ i * (1 / 3) ^ (m - i) * (m.choose i)) + (fun i _ => by positivity) ha + rw [← hsum, show m - a = b by omega] at hle + linarith + +/-- **Path counting.** Any sequence of `b` down-steps and `a` up-steps with `d + a ≤ b` reaches `0` +from `d`, so the biased walk reaches `0` from `d` within `a + b` steps with probability at least +`C(a + b, a) (1/3)^b (2/3)^a`. -/ +theorem choose_mul_le_hit (a b d : ℕ) (h : d + a ≤ b) : + ((a + b).choose a : ℝ) * (1 / 3) ^ b * (2 / 3) ^ a ≤ hit (a + b) d := by + induction hm : a + b generalizing a b d with + | zero => + obtain ⟨rfl, rfl⟩ : a = 0 ∧ b = 0 := by omega + obtain rfl : d = 0 := by omega + simp + | succ m ih => + cases d with + | zero => simpa using choose_mul_pow_le_one (m + 1) a b hm + | succ d => + obtain ⟨b, rfl⟩ : ∃ b', b = b' + 1 := ⟨b - 1, by omega⟩ + rw [hit_succ_succ] + have h₁ := ih a b d (by omega) (by omega) + cases a with + | zero => + have := hit_nonneg m (d + 2) + simp only [Nat.choose_zero_right, Nat.cast_one, one_mul, pow_zero, mul_one] at h₁ ⊢ + rw [pow_succ] + linarith + | succ a => + have h₂ := ih a (b + 1) (d + 2) (by omega) (by omega) + rw [Nat.choose_succ_succ, Nat.cast_add] + calc + ((m.choose a : ℝ) + m.choose (a + 1)) * (1 / 3) ^ (b + 1) * (2 / 3) ^ (a + 1) = + (m.choose (a + 1) : ℝ) * (1 / 3) ^ b * (2 / 3) ^ (a + 1) / 3 + + 2 * ((m.choose a : ℝ) * (1 / 3) ^ (b + 1) * (2 / 3) ^ a) / 3 := by ring + _ ≤ hit m d / 3 + 2 * hit m (d + 2) / 3 := by gcongr + +/-! ### The middle binomial weight -/ + +/-- The weights `C(3j, i) 2^{3j - i}` of `(1 + 2) ^ {3j}` increase up to `i = j`. -/ +private theorem weight_le_succ {j i : ℕ} (hi : i < j) : + (3 * j).choose i * 2 ^ (3 * j - i) ≤ (3 * j).choose (i + 1) * 2 ^ (3 * j - (i + 1)) := by + have hrec := Nat.choose_succ_right_eq (3 * j) i + have hpow : 2 ^ (3 * j - i) = 2 * 2 ^ (3 * j - (i + 1)) := by + rw [← pow_succ'] + congr 1 + omega + rw [hpow] + have key : (3 * j).choose i * (2 * 2 ^ (3 * j - (i + 1))) * (i + 1) ≤ + (3 * j).choose (i + 1) * 2 ^ (3 * j - (i + 1)) * (i + 1) := by + calc + (3 * j).choose i * (2 * 2 ^ (3 * j - (i + 1))) * (i + 1) = + (3 * j).choose i * (2 * (i + 1)) * 2 ^ (3 * j - (i + 1)) := by ring + _ ≤ (3 * j).choose i * (3 * j - i) * 2 ^ (3 * j - (i + 1)) := by + gcongr + omega + _ = (3 * j).choose (i + 1) * 2 ^ (3 * j - (i + 1)) * (i + 1) := by + rw [← hrec] + ring + exact Nat.le_of_mul_le_mul_right key (Nat.succ_pos i) + +/-- The weights `C(3j, i) 2^{3j - i}` of `(1 + 2) ^ {3j}` decrease from `i = j`. -/ +private theorem weight_succ_le {j i : ℕ} (hi : j ≤ i) : + (3 * j).choose (i + 1) * 2 ^ (3 * j - (i + 1)) ≤ (3 * j).choose i * 2 ^ (3 * j - i) := by + rcases lt_or_ge i (3 * j) with hlt | hge + · have hrec := Nat.choose_succ_right_eq (3 * j) i + have hpow : 2 ^ (3 * j - i) = 2 * 2 ^ (3 * j - (i + 1)) := by + rw [← pow_succ'] + congr 1 + omega + rw [hpow] + have key : (3 * j).choose (i + 1) * 2 ^ (3 * j - (i + 1)) * (i + 1) ≤ + (3 * j).choose i * (2 * 2 ^ (3 * j - (i + 1))) * (i + 1) := by + calc + (3 * j).choose (i + 1) * 2 ^ (3 * j - (i + 1)) * (i + 1) = + (3 * j).choose i * (3 * j - i) * 2 ^ (3 * j - (i + 1)) := by + rw [← hrec] + ring + _ ≤ (3 * j).choose i * (2 * (i + 1)) * 2 ^ (3 * j - (i + 1)) := by + gcongr + omega + _ = (3 * j).choose i * (2 * 2 ^ (3 * j - (i + 1))) * (i + 1) := by ring + exact Nat.le_of_mul_le_mul_right key (Nat.succ_pos i) + · rw [Nat.choose_eq_zero_of_lt (by omega), zero_mul] + exact Nat.zero_le _ + +/-- The middle weight `C(3j, j) 2^{2j}` is the largest weight of `(1 + 2) ^ {3j}`. -/ +private theorem weight_le_middle (j i : ℕ) : + (3 * j).choose i * 2 ^ (3 * j - i) ≤ (3 * j).choose j * 2 ^ (3 * j - j) := by + rcases le_total i j with hij | hij + · have key : ∀ k i, i + k = j → + (3 * j).choose i * 2 ^ (3 * j - i) ≤ (3 * j).choose j * 2 ^ (3 * j - j) := by + intro k + induction k with + | zero => intro i hi; subst hi; rfl + | succ k ih => + intro i hi + exact (weight_le_succ (by omega)).trans (ih (i + 1) (by omega)) + exact key (j - i) i (by omega) + · have key : ∀ k, (3 * j).choose (j + k) * 2 ^ (3 * j - (j + k)) ≤ + (3 * j).choose j * 2 ^ (3 * j - j) := by + intro k + induction k with + | zero => rfl + | succ k ih => exact (weight_succ_le (i := j + k) (by omega)).trans ih + obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hij + exact key k + +/-- **The middle binomial coefficient of `(1 + 2) ^ {3j}`**: `27^j ≤ C(3j, j) 4^j (3j + 1)`, since +the middle weight is the largest of the `3 j + 1` weights summing to `27^j`. -/ +theorem pow_le_choose_mul (j : ℕ) : 27 ^ j ≤ (3 * j).choose j * 4 ^ j * (3 * j + 1) := by + have hsum : 27 ^ j = ∑ i ∈ range (3 * j + 1), (3 * j).choose i * 2 ^ (3 * j - i) := by + have h := add_pow (1 : ℕ) 2 (3 * j) + rw [show (1 : ℕ) + 2 = 3 by rfl, show (3 : ℕ) ^ (3 * j) = 27 ^ j by + rw [pow_mul]; norm_num] at h + rw [h] + exact sum_congr rfl fun i _ => by rw [one_pow, one_mul, mul_comm, Nat.cast_id] + rw [hsum] + calc + ∑ i ∈ range (3 * j + 1), (3 * j).choose i * 2 ^ (3 * j - i) ≤ + ∑ _i ∈ range (3 * j + 1), (3 * j).choose j * 2 ^ (3 * j - j) := + sum_le_sum fun i _ => weight_le_middle j i + _ = (3 * j).choose j * 4 ^ j * (3 * j + 1) := by + rw [sum_const, card_range, smul_eq_mul, show 3 * j - j = 2 * j by omega, pow_mul] + norm_num + ring + +/-- From distance `j`, the biased walk reaches `0` within `3 j` steps with probability at least +`2^{-j} / (3 j + 1)`. -/ +theorem inv_le_hit (j : ℕ) : (1 / 2 : ℝ) ^ j / (3 * j + 1) ≤ hit (3 * j) j := by + have hpath := choose_mul_le_hit j (2 * j) j (by omega) + rw [show j + 2 * j = 3 * j by omega] at hpath + refine le_trans ?_ hpath + have hbin : (27 : ℝ) ^ j ≤ (3 * j).choose j * 4 ^ j * (3 * j + 1) := by + exact_mod_cast pow_le_choose_mul j + have hpos : (0 : ℝ) < 3 * j + 1 := by positivity + have hx : (0 : ℝ) < 2 ^ j := by positivity + have hy : (0 : ℝ) < 27 ^ j := by positivity + rw [show (4 : ℝ) ^ j = 2 ^ j * 2 ^ j by rw [← mul_pow]; norm_num] at hbin + have hweight : ((3 * j).choose j : ℝ) * (1 / 3) ^ (2 * j) * (2 / 3) ^ j = + (3 * j).choose j * (2 ^ j / 27 ^ j) := by + rw [mul_assoc, pow_mul, ← mul_pow] + norm_num [div_pow] + rw [hweight, div_le_iff₀ hpos, one_div_pow, div_le_iff₀ hx] + have hrhs : ((3 * j).choose j : ℝ) * (2 ^ j / 27 ^ j) * (3 * j + 1) * 2 ^ j = + ((3 * j).choose j * (2 ^ j * 2 ^ j) * (3 * j + 1)) / 27 ^ j := by + field_simp + rw [hrhs, le_div_iff₀ hy, one_mul] + exact hbin + +/-! ### The local search dominates the biased walk -/ + +/-- Flipping one variable changes the Hamming distance to `τ` by one: it grows if the variable +agreed with `τ` and shrinks otherwise. -/ +theorem hammingDist_flip (σ τ : V → Bool) (v : V) : + hammingDist (flip σ v) τ = + if σ v = τ v then hammingDist σ τ + 1 else hammingDist σ τ - 1 := by + unfold hammingDist + split_ifs with h + · have hset : (univ.filter fun i => flip σ v i ≠ τ i) = + insert v (univ.filter fun i => σ i ≠ τ i) := by + ext i + by_cases hi : i = v + · subst hi + cases hσ : σ i <;> cases hτ : τ i <;> simp_all [flip] + · simp [flip, Function.update_apply, hi] + rw [hset, card_insert_of_notMem (by simp [h])] + · have hset : (univ.filter fun i => flip σ v i ≠ τ i) = + (univ.filter fun i => σ i ≠ τ i).erase v := by + ext i + by_cases hi : i = v + · subst hi + cases hσ : σ i <;> cases hτ : τ i <;> simp_all [flip] + · simp [flip, Function.update_apply, hi] + rw [hset, card_erase_of_mem (by simp [h])] + +omit [Fintype V] [DecidableEq V] in +theorem succeedProb_pure (φ : CNF V) (σ : V → Bool) : + succeedProb φ (PMF.pure σ) = if φ.eval σ = true then 1 else 0 := by + rw [succeedProb, PMF.toOuterMeasure_pure_apply] + split_ifs <;> simp_all + +omit [Fintype V] [DecidableEq V] in +theorem succeedProb_nonneg (φ : CNF V) (μ : PMF (V → Bool)) : 0 ≤ succeedProb φ μ := + ENNReal.toReal_nonneg + +omit [Fintype V] in +/-- The success probability of one step followed by `t` more is the average over the literal +occurrences of the chosen clause. -/ +private theorem succeedProb_flipStep_bind (φ : CNF V) {c : Clause V} (hc : c.length ≠ 0) + (σ : V → Bool) (μ : (V → Bool) → PMF (V → Bool)) : + haveI : NeZero c.length := ⟨hc⟩ + succeedProb φ ((flipStep c σ).bind μ) = + ∑ i : Fin c.length, (c.length : ℝ)⁻¹ * succeedProb φ (μ (flip σ (c.get i).1)) := by + have : NeZero c.length := ⟨hc⟩ + simp only [flipStep, hc, ↓reduceDIte] + rw [PMF.bind_map, succeedProb, Cslib.Probability.PMF.toOuterMeasure_bind_toReal] + simp only [Cslib.Probability.PMF.uniformOfFintype_apply, Fintype.card_fin, ENNReal.toReal_inv, + ENNReal.toReal_natCast, Function.comp_apply, succeedProb] + +/-- **The local search dominates the biased walk.** If `σ⋆` satisfies `φ` and every clause of `φ` +has at most three literals, then `t` steps from `σ` reach a satisfying assignment with probability +at least `hit t (dist σ σ⋆)`. -/ +theorem hit_le_succeedProb {φ : CNF V} {σs : V → Bool} (hs : φ.eval σs = true) + (h3 : ∀ c ∈ φ, c.length ≤ 3) (t : ℕ) (σ : V → Bool) : + hit t (hammingDist σ σs) ≤ succeedProb φ (walk φ t σ) := by + induction t generalizing σ with + | zero => + rw [walk, succeedProb_pure] + rcases Nat.eq_zero_or_pos (hammingDist σ σs) with h0 | hpos + · rw [hammingDist_eq_zero.mp h0] + simp [hs] + · obtain ⟨d, hd⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne' + rw [hd, hit_zero_succ] + split_ifs <;> norm_num + | succ t ih => + rw [walk] + cases hfu : firstUnsat φ σ with + | none => + have hsat : φ.eval σ = true := by + rw [CNF.eval_eq_true_iff] + intro c hc + have := List.find?_eq_none.mp hfu c hc + simpa using this + simp only [succeedProb_pure, hsat, ite_true] + exact hit_le_one _ _ + | some c => + have hc : c ∈ φ := List.mem_of_find?_eq_some hfu + have hcσ : ∀ l ∈ c, σ l.1 ≠ l.2 := by + have := List.find?_some hfu + simp only [Bool.not_eq_eq_eq_not, Bool.not_true] at this + intro l hl hl' + have hsat : c.eval σ = true := (Clause.eval_eq_true_iff σ c).mpr ⟨l, hl, hl'⟩ + rw [hsat] at this + exact absurd this (by decide) + obtain ⟨l, hl, hls⟩ := + (Clause.eval_eq_true_iff σs c).mp ((CNF.eval_eq_true_iff σs φ).mp hs c hc) + have hne : σ l.1 ≠ σs l.1 := by rw [hls]; exact hcσ l hl + have hdpos : hammingDist σ σs ≠ 0 := fun h => hne (congrFun (hammingDist_eq_zero.mp h) _) + obtain ⟨d, hd⟩ := Nat.exists_eq_succ_of_ne_zero hdpos + have hlen : c.length ≠ 0 := (List.length_pos_of_mem hl).ne' + have : NeZero c.length := ⟨hlen⟩ + rw [hd, hit_succ_succ, succeedProb_flipStep_bind φ hlen] + set f : Fin c.length → ℝ := fun i => succeedProb φ (walk φ t (flip σ (c.get i).1)) + obtain ⟨i₀, hi₀⟩ := List.get_of_mem hl + have hterm : ∀ i, hit t (d + 2) ≤ f i := by + intro i + refine le_trans (hit_antitone t ?_) (ih _) + rw [hammingDist_flip, hd] + split_ifs <;> omega + have hterm₀ : hit t d ≤ f i₀ := by + refine le_trans (le_of_eq ?_) (ih _) + rw [hi₀, hammingDist_flip, hd] + simp [hne] + have hsum : hit t d + ((c.length : ℝ) - 1) * hit t (d + 2) ≤ ∑ i, f i := by + rw [← add_sum_erase _ _ (mem_univ i₀)] + have hcard : ((c.length : ℝ) - 1) * hit t (d + 2) = + ∑ _i ∈ univ.erase i₀, hit t (d + 2) := by + rw [sum_const, card_erase_of_mem (mem_univ _), card_univ, Fintype.card_fin, + nsmul_eq_mul, Nat.cast_sub (Nat.one_le_iff_ne_zero.mpr hlen), Nat.cast_one] + rw [hcard] + exact add_le_add hterm₀ (sum_le_sum fun i _ => hterm i) + rw [← mul_sum] + have hm3 : (c.length : ℝ) ≤ 3 := by exact_mod_cast h3 c hc + have hm1 : (1 : ℝ) ≤ c.length := by exact_mod_cast Nat.one_le_iff_ne_zero.mpr hlen + have hAB : hit t (d + 2) ≤ hit t d := hit_antitone t (by omega) + have hB := hit_nonneg t (d + 2) + calc + hit t d / 3 + 2 * hit t (d + 2) / 3 ≤ + (c.length : ℝ)⁻¹ * (hit t d + ((c.length : ℝ) - 1) * hit t (d + 2)) := by + rw [inv_mul_eq_div, le_div_iff₀ (by linarith)] + nlinarith [mul_nonneg (sub_nonneg.mpr hAB) (sub_nonneg.mpr hm3)] + _ ≤ (c.length : ℝ)⁻¹ * ∑ i, f i := by gcongr + +/-! ### Schöning's bound -/ + +omit [DecidableEq V] in +/-- Averaging `2^{-dist(σ, τ)}` over all assignments `σ` gives `(3/2)^n`, a product over the +coordinates. -/ +theorem sum_half_pow_hammingDist [DecidableEq V] (τ : V → Bool) : + ∑ σ : V → Bool, (1 / 2 : ℝ) ^ hammingDist σ τ = (3 / 2) ^ Fintype.card V := by + have hprod (σ : V → Bool) : + (1 / 2 : ℝ) ^ hammingDist σ τ = ∏ i, if σ i = τ i then 1 else 1 / 2 := by + rw [prod_ite, prod_const_one, one_mul, prod_const] + rfl + simp only [hprod] + rw [← Fintype.prod_sum (fun i b => if b = τ i then (1 : ℝ) else 1 / 2)] + have hb (i : V) : ∑ b : Bool, (if b = τ i then (1 : ℝ) else 1 / 2) = 3 / 2 := by + rw [Fintype.sum_bool] + cases τ i <;> norm_num + simp only [hb, prod_const, card_univ] + +/-- **Schöning's theorem for 3-SAT, one trial.** For a satisfiable CNF formula on `n` variables +whose clauses have at most three literals, one trial of Schöning's algorithm finds a satisfying +assignment with probability at least `(3 / 4) ^ n / (3 n + 1)`. -/ +theorem trial_success {φ : CNF V} (hφ : φ.Satisfiable) (h3 : ∀ c ∈ φ, c.length ≤ 3) : + (3 / 4 : ℝ) ^ Fintype.card V / (3 * Fintype.card V + 1) ≤ succeedProb φ (trial φ) := by + obtain ⟨σs, hs⟩ := hφ + set n := Fintype.card V + have hlow (σ : V → Bool) : + (1 / 2 : ℝ) ^ hammingDist σ σs / (3 * n + 1) ≤ succeedProb φ (walk φ (3 * n) σ) := by + have hd : hammingDist σ σs ≤ n := hammingDist_le_card_fintype + calc + (1 / 2 : ℝ) ^ hammingDist σ σs / (3 * n + 1) ≤ + (1 / 2 : ℝ) ^ hammingDist σ σs / (3 * hammingDist σ σs + 1) := by + gcongr + _ ≤ hit (3 * hammingDist σ σs) (hammingDist σ σs) := inv_le_hit _ + _ ≤ hit (3 * n) (hammingDist σ σs) := hit_monotone _ (by omega) + _ ≤ _ := hit_le_succeedProb hs h3 _ σ + rw [trial, succeedProb, Cslib.Probability.PMF.toOuterMeasure_bind_toReal] + simp only [Cslib.Probability.PMF.uniformOfFintype_apply, ENNReal.toReal_inv, Fintype.card_fun, + Fintype.card_bool, Nat.cast_pow, Nat.cast_ofNat] + calc + (3 / 4 : ℝ) ^ n / (3 * n + 1) = + ∑ σ : V → Bool, ((2 : ℝ) ^ n)⁻¹ * ((1 / 2 : ℝ) ^ hammingDist σ σs / (3 * n + 1)) := by + rw [← mul_sum, ← sum_div, sum_half_pow_hammingDist, ← mul_div_assoc, ← inv_pow, ← mul_pow] + norm_num + _ ≤ ∑ σ : V → Bool, ((2 : ℝ) ^ n)⁻¹ * succeedProb φ (walk φ (3 * n) σ) := by + gcongr with σ + exact hlow σ + +end Cslib.Complexity.Schoening diff --git a/ComplexityTests/Schoening.lean b/ComplexityTests/Schoening.lean new file mode 100644 index 0000000000..ed7c33b711 --- /dev/null +++ b/ComplexityTests/Schoening.lean @@ -0,0 +1,54 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Complexity.FineGrained.Schoening + +/-! Schöning's random walk: a concrete satisfiable instance, the biased walk and the binomial bound, +and axiom guards. -/ + +namespace ComplexityTests.Schoening + +open Cslib.Logic.PL Cslib.Complexity.Schoening + +/-- `(x₀ ∨ x₁) ∧ (¬x₀ ∨ x₁ ∨ x₂)`: satisfiable, with clauses of at most three literals. -/ +def φ : CNF (Fin 3) := [[(0, true), (1, true)], [(0, false), (1, true), (2, true)]] + +theorem φ_satisfiable : φ.Satisfiable := ⟨fun _ => true, by decide⟩ + +theorem φ_three : ∀ c ∈ φ, c.length ≤ 3 := by decide + +-- The hypotheses of `trial_success` are satisfiable: one trial succeeds with probability at least +-- `(3 / 4) ^ 3 / 10`. +example : (3 / 4 : ℝ) ^ 3 / (3 * 3 + 1) ≤ succeedProb φ (trial φ) := by + simpa using trial_success φ_satisfiable φ_three + +-- A satisfying start succeeds without any step. +example : succeedProb φ (walk φ 0 fun _ => true) = 1 := by + rw [walk, succeedProb_pure, ite_eq_left (by decide)] + +-- The biased walk: from distance one, three steps reach `0` with probability `1/3 + 2/9 * 1/3`. +example : hit 3 1 = 1 / 3 + 2 / 3 * (1 / 3 * (1 / 3)) := by + simp only [hit_succ_succ, hit_zero_right, hit_zero_succ] + norm_num + +-- The middle binomial bound at `j = 2`: `27² ≤ C(6, 2) · 4² · 7`. +example : 27 ^ 2 ≤ (3 * 2).choose 2 * 4 ^ 2 * (3 * 2 + 1) := pow_le_choose_mul 2 + +/-- +info: 'Cslib.Complexity.Schoening.hit_le_succeedProb' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms hit_le_succeedProb + +/-- +info: 'Cslib.Complexity.Schoening.trial_success' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms trial_success + +end ComplexityTests.Schoening diff --git a/ROADMAP.md b/ROADMAP.md index d7856f02ab..cd95540be5 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -584,7 +584,7 @@ developments, not assertions that every prerequisite is missing or assignments t | Proof complexity | Build on [Cook–Reckhow systems and simulations](Complexity/Computability/Complexity/ProofSystem.lean), including the polynomially bounded-system characterization of NP = coNP, the [resolution size–width tradeoff](Complexity/Logics/Propositional/Resolution/SizeWidth.lean), [tree-like resolution/DPLL search-tree certificates](Complexity/Logics/Propositional/Resolution/TreeLike.lean), [Tseitin formulas on expanders](Complexity/Logics/Propositional/Resolution/TseitinExpander.lean) and [Haken's pigeonhole lower bound](Complexity/Logics/Propositional/Resolution/Pigeonhole.lean). Extend proof-space lower bounds, Frege, cutting planes, polynomial calculus and sum-of-squares. The certificate correspondence does not certify a DPLL solver's runtime. | | Average-case complexity and learning | Uniform-distribution learning on CSLib's PAC API, the LMN low-degree algorithm and Kushilevitz–Mansour with membership queries are [proved](Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean); running times are not machine-certified. Distributional problems and reductions, samplability, average-to-worst-case connections, PAC/agnostic/SQ learning, learning lower bounds, compression and refutation. Existing cryptographic learners are starting points, not coverage of learning theory. | | Property and distribution testing | Distance and access models, one/two-sided and tolerant testing, query/sample bounds, canonical graph/algebraic/distribution testers and lower bounds. | -| Fine-grained and parameterized complexity | Under ETH, 3-coloring, independent set, vertex cover and Hamiltonian cycle and path have no 2^{o(\|V\|+\|E\|)} algorithms and clique none in 2^{o(\|V\|)} ([GraphProblems](Complexity/Computability/Complexity/FineGrained/GraphProblems.lean)); the Hamiltonian bounds (directed and undirected) use linear-size diamond reductions. [FPT and XP](Complexity/Computability/Complexity/Parameterized.lean) are defined with arbitrary (not necessarily computable) `f`; `P ⊆ FPT ⊆ XP`, Boolean closure of FPT (complement for XP), closure under fpt-reductions and `FPT = XP = P` for bounded parameters are proved, and SAT is in FPT for the number of variables. [Kernelization](Complexity/Computability/Complexity/Parameterized/Kernelization.lean) (`IsKernelization`, `HasKernel`, `HasPolyKernel`) and the Cai–Chen–Downey–Fellows equivalence (`A ∈ FPT enc κ ↔ HasKernel enc κ A` for `A ∈ DTIME enc t` over a nonempty instance type) are proved, and [VertexCover](Complexity/Computability/Complexity/Parameterized/VertexCover.lean) is in FPT parameterized by target size `k` in time `O(2^k (|x|+1)^e)` by a bounded search tree and has [Buss's polynomial kernel](Complexity/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean) with at most `k(k+2)` vertices and encoded length at most `40(k+1)^6` (`VertexCover_hasPolyKernel`). Further fine-grained reductions and consequences conditional on ETH/SETH and other named hypotheses; strongly uniform (computable `f`) variants, further explicit polynomial kernels, W/A hierarchies and parameterized lower bounds. | +| Fine-grained and parameterized complexity | Under ETH, 3-coloring, independent set, vertex cover and Hamiltonian cycle and path have no 2^{o(\|V\|+\|E\|)} algorithms and clique none in 2^{o(\|V\|)} ([GraphProblems](Complexity/Computability/Complexity/FineGrained/GraphProblems.lean)); the Hamiltonian bounds (directed and undirected) use linear-size diamond reductions. [FPT and XP](Complexity/Computability/Complexity/Parameterized.lean) are defined with arbitrary (not necessarily computable) `f`; `P ⊆ FPT ⊆ XP`, Boolean closure of FPT (complement for XP), closure under fpt-reductions and `FPT = XP = P` for bounded parameters are proved, and SAT is in FPT for the number of variables. [Kernelization](Complexity/Computability/Complexity/Parameterized/Kernelization.lean) (`IsKernelization`, `HasKernel`, `HasPolyKernel`) and the Cai–Chen–Downey–Fellows equivalence (`A ∈ FPT enc κ ↔ HasKernel enc κ A` for `A ∈ DTIME enc t` over a nonempty instance type) are proved, and [VertexCover](Complexity/Computability/Complexity/Parameterized/VertexCover.lean) is in FPT parameterized by target size `k` in time `O(2^k (|x|+1)^e)` by a bounded search tree and has [Buss's polynomial kernel](Complexity/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean) with at most `k(k+2)` vertices and encoded length at most `40(k+1)^6` (`VertexCover_hasPolyKernel`). On the algorithmic side, one trial of [Schöning's random walk](Complexity/Computability/Complexity/FineGrained/Schoening.lean) finds a satisfying assignment of a satisfiable 3-CNF with probability at least `(3/4)^n / (3n + 1)`; general `k`, amplification, a time bound and PPSZ remain (#894). Further fine-grained reductions and consequences conditional on ETH/SETH and other named hypotheses; strongly uniform (computable `f`) variants, further explicit polynomial kernels, W/A hierarchies and parameterized lower bounds. | | Total search and computational games | Build on [FNP, FP and TFNP with search reductions](Complexity/Computability/Complexity/Classes/TFNP.lean), including `FP = FNP` exactly when `P = NP` ([search to decision](Complexity/Computability/Complexity/Classes/TFNP/SearchToDecision.lean)), `TFNP ⊆ FP → NP ∩ coNP ⊆ P`, and the canonical subclasses [PLS, PPP, PPAD and PPA](Complexity/Computability/Complexity/Classes/TFNP/Subclasses.lean) with their combinatorial totality principles ([Principles](Complexity/Computability/Complexity/Classes/TFNP/Subclasses/Principles.lean)), inclusions `PLS, PPP, PPAD, PPA ⊆ TFNP`, `PPAD ⊆ PPP`, and `PPAD ⊆ PPA`, and De Morgan circuit problems (`LocalOpt ∈ PLS`, `Pigeon ∈ PPP`, `EndOfLine ∈ PPAD`, `Leaf ∈ PPA`). Their [completeness](Complexity/Computability/Complexity/Classes/TFNP/Subclasses/Completeness.lean) now follows from polynomial-time construction of function-family circuit codes, preserving binary local-search costs. Develop CLS, further local search, fixed-point and equilibrium problems. | | Logic and descriptive complexity | Building on [Fagin's theorem](Complexity/Computability/Complexity/Fagin/Converse.lean): logical characterizations of additional resource classes, fixed-point and order-invariant queries, and uniform translations between syntax, structures and algorithms. | | Kolmogorov complexity and metacomplexity | Build on [plain Kolmogorov uncomputability](Complexity/Computability/Kolmogorov/Uncomputability.lean), [single-tape and Post–Turing (`TM0`/`TM1`) description methods and simulations](Complexity/Computability/Kolmogorov/SingleTape.lean), and [multi-tape description methods and `Partrec` optimality](Complexity/Computability/Kolmogorov/MultiTape.lean) (#318): `ofTM0` and `ofTM1` are defined through the `SingleTapeTM` embeddings of Mathlib's `TM0`/`TM1`; `ofSingleTapeTM` (and `ofTM0`) are simulated by `ofMultiTapeTM` with zero program overhead and linear time overhead (single-tape → multi-tape only; the reverse simulation is not formalized); and each of `ofSingleTapeTM`, `ofTM0`, `ofTM1` and `ofMultiTapeTM`, pushed forward along a computable decoder, is simulated by the universal partial-recursive description method `universal` with additive overhead. Extend prefix-free complexity, resource-bounded MCSP variants and connections to learning, cryptography and lower bounds. | diff --git a/references.bib b/references.bib index bb3ab7ca28..048e35dfba 100644 --- a/references.bib +++ b/references.bib @@ -4089,3 +4089,12 @@ @article{AKS2004 year = {2004}, doi = {10.4007/annals.2004.160.781} } + +@inproceedings{Schoening1999, + author = {Sch{\"o}ning, Uwe}, + title = {A Probabilistic Algorithm for k-{SAT} and Constraint Satisfaction Problems}, + booktitle = {40th Annual Symposium on Foundations of Computer Science (FOCS)}, + pages = {410--414}, + year = {1999}, + doi = {10.1109/SFFCS.1999.814612} +} From 495d1d77b4a99adde008ccbdca0a803122dc5e35 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 25 Oct 2026 00:10:10 +0000 Subject: [PATCH 2/2] =?UTF-8?q?feat(FineGrained):=20Sch=C3=B6ning's=20boun?= =?UTF-8?q?d=20for=20k-SAT=20(#894)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Generalize the biased walk to down-probability 1/k, the middle-weight bound to ((k-1)+1)^{ki}, and the hitting bound to any distance d via d = (k-2) i + e, giving one-trial success probability at least ((k-1)/k)^(k-3) (k/(2(k-1)))^n / (3n+1) for k-CNF; the 3-SAT bound is the case k = 3. AI-assisted: Jetski (worker-jetski-17d3679e). --- .../Complexity/FineGrained/Schoening.lean | 500 +++++++++++------- ComplexityTests/Schoening.lean | 27 +- ROADMAP.md | 2 +- 3 files changed, 333 insertions(+), 196 deletions(-) diff --git a/Complexity/Computability/Complexity/FineGrained/Schoening.lean b/Complexity/Computability/Complexity/FineGrained/Schoening.lean index dbe71a1eb5..ee1dabc597 100644 --- a/Complexity/Computability/Complexity/FineGrained/Schoening.lean +++ b/Complexity/Computability/Complexity/FineGrained/Schoening.lean @@ -16,7 +16,7 @@ import Mathlib.Tactic.Linarith import Mathlib.Tactic.Positivity /-! -# Schöning's random walk for 3-SAT +# Schöning's random walk for k-SAT Schöning's algorithm searches for a satisfying assignment of a CNF formula by local search with restarts. One *trial* draws a uniformly random assignment and then performs `3 n` steps, where `n` @@ -25,25 +25,29 @@ first unsatisfied clause, chooses one of its literal occurrences uniformly, and variable (`Cslib.Complexity.Schoening.walk`, `Cslib.Complexity.Schoening.trial`) [Schöning][Schoening1999]. -For a satisfiable formula whose clauses have at most three literals, a trial succeeds with -probability at least `(3 / 4) ^ n / (3 n + 1)` (`Cslib.Complexity.Schoening.trial_success`). So -about `(4 / 3) ^ n` independent trials find a satisfying assignment with high probability, -exponentially faster than the `2 ^ n` assignments of brute force. Schöning states the bound up to a -polynomial factor; the factor `1 / (3 n + 1)` here is this file's explicit constant. +For `k ≥ 3` and a satisfiable formula whose clauses have at most `k` literals, a trial succeeds +with probability at least `((k - 1)/k)^{k - 3} (k / (2(k - 1)))^n / (3 n + 1)` +(`Cslib.Complexity.Schoening.trial_success_of_length_le`); for `k = 3` this is +`(3 / 4) ^ n / (3 n + 1)` (`Cslib.Complexity.Schoening.trial_success`). So about +`(2 - 2/k)^n` independent trials find a satisfying assignment with high probability, exponentially +faster than the `2 ^ n` assignments of brute force. Schöning states the bound up to a polynomial +factor; the factors `((k - 1)/k)^{k - 3}` and `1 / (3 n + 1)` are this file's explicit constants. The proof compares the walk with a biased random walk on distances. Fix a satisfying assignment `σ⋆`. A step changes the Hamming distance to `σ⋆` by one. Since `σ⋆` satisfies the chosen clause -and the current assignment does not, at least one of its at most three literals moves toward `σ⋆`. -Let `hit t d` be the probability that a walk on `ℕ`, stepping down with probability `1 / 3` and up -with probability `2 / 3`, reaches `0` from `d` within `t` steps (`Cslib.Complexity.Schoening.hit`). -It is antitone in `d` (`hit_succ_le`), so by induction on `t` the trial walk succeeds with -probability at least `hit t (dist σ σ⋆)` (`hit_le_succeedProb`). No coupling is needed. - -A path of `2 j` down-steps and `j` up-steps reaches `0` from `j`, so -`hit (3 j) j ≥ C(3j, j) (1/3)^{2j} (2/3)^j` (`choose_mul_le_hit`). The middle binomial weight is the -largest of the `3 j + 1` terms of `(1 + 2) ^ {3j}`, so `C(3j, j) 4^j (3j + 1) ≥ 27^j` -(`pow_le_choose_mul`), and `hit (3 j) j ≥ 2^{-j} / (3 j + 1)`. Averaging `2^{-dist}` over a -uniform start gives `(3/4)^n`, a product over the coordinates. +and the current assignment does not, at least one of its at most `k` literals moves toward `σ⋆`. +Let `hit k t d` be the probability that a walk on `ℕ`, stepping down with probability `1 / k` and +up with probability `(k - 1) / k`, reaches `0` from `d` within `t` steps +(`Cslib.Complexity.Schoening.hit`). It is antitone in `d` (`hit_succ_le`), so by induction on `t` +the trial walk succeeds with probability at least `hit k t (dist σ σ⋆)` (`hit_le_succeedProb`). +No coupling is needed. + +Write `d = (k - 2) i + e` with `e < k - 2`. A path of `i + d` down-steps and `i` up-steps reaches +`0` from `d` within `ki + e ≤ 3d` steps (`choose_mul_le_hit`). The middle weight +`C(ki, i) (k - 1)^{ki - i}` is the largest of the `ki + 1` terms of `((k - 1) + 1)^{ki}` +(`pow_le_choose_mul`), which gives `hit k (3 d) d ≥ ((k - 1)/k)^{k - 3} (k - 1)^{-d} / (3 d + 1)` +(`inv_le_hit`). Averaging `(k - 1)^{-dist}` over a uniform start gives `(k / (2(k - 1)))^n`, a +product over the coordinates (`sum_pow_hammingDist`). ## Main definitions @@ -55,9 +59,11 @@ uniform start gives `(3/4)^n`, a product over the coordinates. * `Cslib.Complexity.Schoening.hit_le_succeedProb`: the local search dominates the biased walk. * `Cslib.Complexity.Schoening.choose_mul_le_hit`: path counting for the biased walk. -* `Cslib.Complexity.Schoening.pow_le_choose_mul`: `27^j ≤ C(3j, j) 4^j (3j + 1)`. -* `Cslib.Complexity.Schoening.trial_success`: a trial succeeds with probability at least - `(3 / 4) ^ n / (3 n + 1)`. +* `Cslib.Complexity.Schoening.pow_le_choose_mul`: `k^{ki} ≤ C(ki, i) (k - 1)^{ki - i} (ki + 1)`. +* `Cslib.Complexity.Schoening.inv_le_hit`: the hitting bound from distance `d` within `3 d` steps. +* `Cslib.Complexity.Schoening.trial_success_of_length_le`: Schöning's bound for k-SAT. +* `Cslib.Complexity.Schoening.trial_success`: a trial for 3-SAT succeeds with probability at + least `(3 / 4) ^ n / (3 n + 1)`. ## References @@ -109,21 +115,27 @@ noncomputable def succeedProb (φ : CNF V) (μ : PMF (V → Bool)) : ℝ := /-! ### The biased walk -/ -/-- The probability that a walk on `ℕ` that steps down with probability `1 / 3` and up with -probability `2 / 3` reaches `0` from `d` within `t` steps. -/ -noncomputable def hit : ℕ → ℕ → ℝ +/-- The probability that a walk on `ℕ` that steps down with probability `1 / k` and up with +probability `(k - 1) / k` reaches `0` from `d` within `t` steps. -/ +noncomputable def hit (k : ℕ) : ℕ → ℕ → ℝ | _, 0 => 1 | 0, _ + 1 => 0 - | t + 1, d + 1 => hit t d / 3 + 2 * hit t (d + 2) / 3 + | t + 1, d + 1 => (hit k t d + ((k : ℝ) - 1) * hit k t (d + 2)) / k -@[simp] theorem hit_zero_right (t : ℕ) : hit t 0 = 1 := by cases t <;> rfl +variable {k : ℕ} -@[simp] theorem hit_zero_succ (d : ℕ) : hit 0 (d + 1) = 0 := rfl +@[simp] theorem hit_zero_right (k t : ℕ) : hit k t 0 = 1 := by cases t <;> rfl -theorem hit_succ_succ (t d : ℕ) : hit (t + 1) (d + 1) = hit t d / 3 + 2 * hit t (d + 2) / 3 := +@[simp] theorem hit_zero_succ (k d : ℕ) : hit k 0 (d + 1) = 0 := rfl + +theorem hit_succ_succ (k t d : ℕ) : + hit k (t + 1) (d + 1) = (hit k t d + ((k : ℝ) - 1) * hit k t (d + 2)) / k := rfl -theorem hit_nonneg (t d : ℕ) : 0 ≤ hit t d := by +theorem hit_nonneg (hk : 1 ≤ k) (t d : ℕ) : 0 ≤ hit k t d := by + have hk1 : (0 : ℝ) ≤ (k : ℝ) - 1 := by + have : (1 : ℝ) ≤ k := by exact_mod_cast hk + linarith induction t generalizing d with | zero => cases d <;> simp | succ t ih => @@ -135,60 +147,72 @@ theorem hit_nonneg (t d : ℕ) : 0 ≤ hit t d := by have := ih (d + 2) positivity -theorem hit_le_one (t d : ℕ) : hit t d ≤ 1 := by +theorem hit_le_one (hk : 1 ≤ k) (t d : ℕ) : hit k t d ≤ 1 := by + have hk1 : (1 : ℝ) ≤ k := by exact_mod_cast hk induction t generalizing d with | zero => cases d <;> simp | succ t ih => cases d with | zero => simp | succ d => - rw [hit_succ_succ] - linarith [ih d, ih (d + 2)] + rw [hit_succ_succ, div_le_one (by linarith)] + nlinarith [ih d, ih (d + 2), hit_nonneg hk t (d + 2)] /-- Hitting `0` is less likely from farther away. -/ -theorem hit_succ_le (t d : ℕ) : hit t (d + 1) ≤ hit t d := by +theorem hit_succ_le (hk : 1 ≤ k) (t d : ℕ) : hit k t (d + 1) ≤ hit k t d := by + have hk1 : (1 : ℝ) ≤ k := by exact_mod_cast hk induction t generalizing d with - | zero => simpa using hit_nonneg 0 d + | zero => simpa using hit_nonneg hk 0 d | succ t ih => cases d with - | zero => simpa using hit_le_one (t + 1) 1 + | zero => simpa using hit_le_one hk (t + 1) 1 | succ d => rw [hit_succ_succ, hit_succ_succ] - linarith [ih d, ih (d + 2)] + gcongr ?_ / _ + nlinarith [ih d, ih (d + 2)] -theorem hit_antitone (t : ℕ) : Antitone (hit t) := - antitone_nat_of_succ_le (hit_succ_le t) +theorem hit_antitone (hk : 1 ≤ k) (t : ℕ) : Antitone (hit k t) := + antitone_nat_of_succ_le (hit_succ_le hk t) /-- Hitting `0` is more likely with more time. -/ -theorem hit_le_hit_succ (t d : ℕ) : hit t d ≤ hit (t + 1) d := by +theorem hit_le_hit_succ (hk : 1 ≤ k) (t d : ℕ) : hit k t d ≤ hit k (t + 1) d := by + have hk1 : (1 : ℝ) ≤ k := by exact_mod_cast hk induction t generalizing d with - | zero => cases d <;> simp [hit_nonneg] + | zero => cases d <;> simp [hit_nonneg hk] | succ t ih => cases d with | zero => simp | succ d => - rw [hit_succ_succ, hit_succ_succ (t + 1)] - linarith [ih d, ih (d + 2)] + rw [hit_succ_succ, hit_succ_succ (t := t + 1)] + gcongr ?_ / _ + nlinarith [ih d, ih (d + 2)] -theorem hit_monotone (d : ℕ) : Monotone fun t => hit t d := - monotone_nat_of_le_succ fun t => hit_le_hit_succ t d +theorem hit_monotone (hk : 1 ≤ k) (d : ℕ) : Monotone fun t => hit k t d := + monotone_nat_of_le_succ fun t => hit_le_hit_succ hk t d /-- A single binomial weight is at most one. -/ -private theorem choose_mul_pow_le_one (m a b : ℕ) (h : a + b = m) : - (m.choose a : ℝ) * (1 / 3) ^ b * (2 / 3) ^ a ≤ 1 := by - have hsum := add_pow (2 / 3 : ℝ) (1 / 3) m - rw [show (2 / 3 : ℝ) + 1 / 3 = 1 by norm_num, one_pow] at hsum +private theorem choose_mul_pow_le_one (hk : 1 ≤ k) (m a b : ℕ) (h : a + b = m) : + (m.choose a : ℝ) * (1 / k) ^ b * (((k : ℝ) - 1) / k) ^ a ≤ 1 := by + have hk1 : (1 : ℝ) ≤ k := by exact_mod_cast hk + have hsum := add_pow (((k : ℝ) - 1) / k) (1 / k) m + rw [show ((k : ℝ) - 1) / k + 1 / k = 1 by field_simp; ring, one_pow] at hsum have ha : a ∈ range (m + 1) := mem_range.mpr (by omega) - have hle := single_le_sum (f := fun i => (2 / 3 : ℝ) ^ i * (1 / 3) ^ (m - i) * (m.choose i)) - (fun i _ => by positivity) ha + have hle := single_le_sum + (f := fun i => (((k : ℝ) - 1) / k) ^ i * (1 / k) ^ (m - i) * (m.choose i)) + (fun i _ => by have : (0 : ℝ) ≤ (k : ℝ) - 1 := by linarith + positivity) ha rw [← hsum, show m - a = b by omega] at hle linarith /-- **Path counting.** Any sequence of `b` down-steps and `a` up-steps with `d + a ≤ b` reaches `0` from `d`, so the biased walk reaches `0` from `d` within `a + b` steps with probability at least -`C(a + b, a) (1/3)^b (2/3)^a`. -/ -theorem choose_mul_le_hit (a b d : ℕ) (h : d + a ≤ b) : - ((a + b).choose a : ℝ) * (1 / 3) ^ b * (2 / 3) ^ a ≤ hit (a + b) d := by +`C(a + b, a) (1/k)^b ((k - 1)/k)^a`. -/ +theorem choose_mul_le_hit (hk : 1 ≤ k) (a b d : ℕ) (h : d + a ≤ b) : + ((a + b).choose a : ℝ) * (1 / k) ^ b * (((k : ℝ) - 1) / k) ^ a ≤ hit k (a + b) d := by + have hk1 : (1 : ℝ) ≤ k := by exact_mod_cast hk + have hk0 : (0 : ℝ) < k := by linarith + have hkm : (0 : ℝ) ≤ (k : ℝ) - 1 := by linarith + have hkne : (k : ℝ) ≠ 0 := hk0.ne' induction hm : a + b generalizing a b d with | zero => obtain ⟨rfl, rfl⟩ : a = 0 ∧ b = 0 := by omega @@ -196,138 +220,211 @@ theorem choose_mul_le_hit (a b d : ℕ) (h : d + a ≤ b) : simp | succ m ih => cases d with - | zero => simpa using choose_mul_pow_le_one (m + 1) a b hm + | zero => simpa using choose_mul_pow_le_one hk (m + 1) a b hm | succ d => obtain ⟨b, rfl⟩ : ∃ b', b = b' + 1 := ⟨b - 1, by omega⟩ rw [hit_succ_succ] have h₁ := ih a b d (by omega) (by omega) + have hB := hit_nonneg hk m (d + 2) cases a with | zero => - have := hit_nonneg m (d + 2) simp only [Nat.choose_zero_right, Nat.cast_one, one_mul, pow_zero, mul_one] at h₁ ⊢ - rw [pow_succ] - linarith + rw [pow_succ, le_div_iff₀ hk0] + have : (1 / (k : ℝ)) ^ b * (1 / k) * k = (1 / k) ^ b := by field_simp + nlinarith [mul_nonneg hkm hB] | succ a => have h₂ := ih a (b + 1) (d + 2) (by omega) (by omega) rw [Nat.choose_succ_succ, Nat.cast_add] calc - ((m.choose a : ℝ) + m.choose (a + 1)) * (1 / 3) ^ (b + 1) * (2 / 3) ^ (a + 1) = - (m.choose (a + 1) : ℝ) * (1 / 3) ^ b * (2 / 3) ^ (a + 1) / 3 + - 2 * ((m.choose a : ℝ) * (1 / 3) ^ (b + 1) * (2 / 3) ^ a) / 3 := by ring - _ ≤ hit m d / 3 + 2 * hit m (d + 2) / 3 := by gcongr + ((m.choose a : ℝ) + m.choose (a + 1)) * (1 / k) ^ (b + 1) * + (((k : ℝ) - 1) / k) ^ (a + 1) = + ((m.choose (a + 1) : ℝ) * (1 / k) ^ b * (((k : ℝ) - 1) / k) ^ (a + 1) + + ((k : ℝ) - 1) * ((m.choose a : ℝ) * (1 / k) ^ (b + 1) * + (((k : ℝ) - 1) / k) ^ a)) / k := by + rw [eq_div_iff hkne] + have hkk : (k : ℝ) * (k : ℝ)⁻¹ = 1 := mul_inv_cancel₀ hkne + linear_combination ((m.choose a : ℝ) + m.choose (a + 1)) * ((k : ℝ)⁻¹) ^ b * + (((k : ℝ) - 1) * (k : ℝ)⁻¹) ^ (a + 1) * hkk + _ ≤ (hit k m d + ((k : ℝ) - 1) * hit k m (d + 2)) / k := by gcongr /-! ### The middle binomial weight -/ -/-- The weights `C(3j, i) 2^{3j - i}` of `(1 + 2) ^ {3j}` increase up to `i = j`. -/ -private theorem weight_le_succ {j i : ℕ} (hi : i < j) : - (3 * j).choose i * 2 ^ (3 * j - i) ≤ (3 * j).choose (i + 1) * 2 ^ (3 * j - (i + 1)) := by - have hrec := Nat.choose_succ_right_eq (3 * j) i - have hpow : 2 ^ (3 * j - i) = 2 * 2 ^ (3 * j - (i + 1)) := by +/-- The weights `C(ki, a) (k - 1)^{ki - a}` of `((k - 1) + 1)^{ki}` increase up to `a = i`. -/ +private theorem weight_le_succ {k i a : ℕ} (hk : 1 ≤ k) (ha : a < i) : + (k * i).choose a * (k - 1) ^ (k * i - a) ≤ + (k * i).choose (a + 1) * (k - 1) ^ (k * i - (a + 1)) := by + have hrec := Nat.choose_succ_right_eq (k * i) a + have hai : a + 1 ≤ k * i := le_trans ha (Nat.le_mul_of_pos_left i hk) + have hpow : (k - 1) ^ (k * i - a) = (k - 1) * (k - 1) ^ (k * i - (a + 1)) := by rw [← pow_succ'] congr 1 omega + have hcoef : (k - 1) * (a + 1) ≤ k * i - a := by + obtain ⟨k', rfl⟩ : ∃ k', k = k' + 1 := ⟨k - 1, by omega⟩ + simp only [Nat.add_sub_cancel] + have : (k' + 1) * (a + 1) ≤ (k' + 1) * i := Nat.mul_le_mul_left _ ha + have : k' * (a + 1) + (a + 1) = (k' + 1) * (a + 1) := by ring + omega rw [hpow] - have key : (3 * j).choose i * (2 * 2 ^ (3 * j - (i + 1))) * (i + 1) ≤ - (3 * j).choose (i + 1) * 2 ^ (3 * j - (i + 1)) * (i + 1) := by + have key : (k * i).choose a * ((k - 1) * (k - 1) ^ (k * i - (a + 1))) * (a + 1) ≤ + (k * i).choose (a + 1) * (k - 1) ^ (k * i - (a + 1)) * (a + 1) := by calc - (3 * j).choose i * (2 * 2 ^ (3 * j - (i + 1))) * (i + 1) = - (3 * j).choose i * (2 * (i + 1)) * 2 ^ (3 * j - (i + 1)) := by ring - _ ≤ (3 * j).choose i * (3 * j - i) * 2 ^ (3 * j - (i + 1)) := by - gcongr - omega - _ = (3 * j).choose (i + 1) * 2 ^ (3 * j - (i + 1)) * (i + 1) := by + (k * i).choose a * ((k - 1) * (k - 1) ^ (k * i - (a + 1))) * (a + 1) = + (k * i).choose a * ((k - 1) * (a + 1)) * (k - 1) ^ (k * i - (a + 1)) := by ring + _ ≤ (k * i).choose a * (k * i - a) * (k - 1) ^ (k * i - (a + 1)) := by gcongr + _ = (k * i).choose (a + 1) * (k - 1) ^ (k * i - (a + 1)) * (a + 1) := by rw [← hrec] ring - exact Nat.le_of_mul_le_mul_right key (Nat.succ_pos i) - -/-- The weights `C(3j, i) 2^{3j - i}` of `(1 + 2) ^ {3j}` decrease from `i = j`. -/ -private theorem weight_succ_le {j i : ℕ} (hi : j ≤ i) : - (3 * j).choose (i + 1) * 2 ^ (3 * j - (i + 1)) ≤ (3 * j).choose i * 2 ^ (3 * j - i) := by - rcases lt_or_ge i (3 * j) with hlt | hge - · have hrec := Nat.choose_succ_right_eq (3 * j) i - have hpow : 2 ^ (3 * j - i) = 2 * 2 ^ (3 * j - (i + 1)) := by + exact Nat.le_of_mul_le_mul_right key (Nat.succ_pos a) + +/-- The weights `C(ki, a) (k - 1)^{ki - a}` of `((k - 1) + 1)^{ki}` decrease from `a = i`. -/ +private theorem weight_succ_le {k i a : ℕ} (hk : 1 ≤ k) (ha : i ≤ a) : + (k * i).choose (a + 1) * (k - 1) ^ (k * i - (a + 1)) ≤ + (k * i).choose a * (k - 1) ^ (k * i - a) := by + rcases lt_or_ge a (k * i) with hlt | hge + · have hrec := Nat.choose_succ_right_eq (k * i) a + have hpow : (k - 1) ^ (k * i - a) = (k - 1) * (k - 1) ^ (k * i - (a + 1)) := by rw [← pow_succ'] congr 1 omega + have hcoef : k * i - a ≤ (k - 1) * (a + 1) := by + obtain ⟨k', rfl⟩ : ∃ k', k = k' + 1 := ⟨k - 1, by omega⟩ + simp only [Nat.add_sub_cancel] + have : (k' + 1) * i ≤ (k' + 1) * a := Nat.mul_le_mul_left _ ha + have : k' * (a + 1) + (a + 1) = (k' + 1) * a + (k' + 1) := by ring + omega rw [hpow] - have key : (3 * j).choose (i + 1) * 2 ^ (3 * j - (i + 1)) * (i + 1) ≤ - (3 * j).choose i * (2 * 2 ^ (3 * j - (i + 1))) * (i + 1) := by + have key : (k * i).choose (a + 1) * (k - 1) ^ (k * i - (a + 1)) * (a + 1) ≤ + (k * i).choose a * ((k - 1) * (k - 1) ^ (k * i - (a + 1))) * (a + 1) := by calc - (3 * j).choose (i + 1) * 2 ^ (3 * j - (i + 1)) * (i + 1) = - (3 * j).choose i * (3 * j - i) * 2 ^ (3 * j - (i + 1)) := by + (k * i).choose (a + 1) * (k - 1) ^ (k * i - (a + 1)) * (a + 1) = + (k * i).choose a * (k * i - a) * (k - 1) ^ (k * i - (a + 1)) := by rw [← hrec] ring - _ ≤ (3 * j).choose i * (2 * (i + 1)) * 2 ^ (3 * j - (i + 1)) := by - gcongr - omega - _ = (3 * j).choose i * (2 * 2 ^ (3 * j - (i + 1))) * (i + 1) := by ring - exact Nat.le_of_mul_le_mul_right key (Nat.succ_pos i) + _ ≤ (k * i).choose a * ((k - 1) * (a + 1)) * (k - 1) ^ (k * i - (a + 1)) := by gcongr + _ = (k * i).choose a * ((k - 1) * (k - 1) ^ (k * i - (a + 1))) * (a + 1) := by ring + exact Nat.le_of_mul_le_mul_right key (Nat.succ_pos a) · rw [Nat.choose_eq_zero_of_lt (by omega), zero_mul] exact Nat.zero_le _ -/-- The middle weight `C(3j, j) 2^{2j}` is the largest weight of `(1 + 2) ^ {3j}`. -/ -private theorem weight_le_middle (j i : ℕ) : - (3 * j).choose i * 2 ^ (3 * j - i) ≤ (3 * j).choose j * 2 ^ (3 * j - j) := by - rcases le_total i j with hij | hij - · have key : ∀ k i, i + k = j → - (3 * j).choose i * 2 ^ (3 * j - i) ≤ (3 * j).choose j * 2 ^ (3 * j - j) := by - intro k - induction k with - | zero => intro i hi; subst hi; rfl - | succ k ih => - intro i hi - exact (weight_le_succ (by omega)).trans (ih (i + 1) (by omega)) - exact key (j - i) i (by omega) - · have key : ∀ k, (3 * j).choose (j + k) * 2 ^ (3 * j - (j + k)) ≤ - (3 * j).choose j * 2 ^ (3 * j - j) := by - intro k - induction k with +/-- The middle weight `C(ki, i) (k - 1)^{ki - i}` is the largest weight of `((k - 1) + 1)^{ki}`. -/ +private theorem weight_le_middle {k : ℕ} (hk : 1 ≤ k) (i a : ℕ) : + (k * i).choose a * (k - 1) ^ (k * i - a) ≤ (k * i).choose i * (k - 1) ^ (k * i - i) := by + rcases le_total a i with hai | hai + · have key : ∀ m a, a + m = i → + (k * i).choose a * (k - 1) ^ (k * i - a) ≤ (k * i).choose i * (k - 1) ^ (k * i - i) := by + intro m + induction m with + | zero => intro a ha; subst ha; rfl + | succ m ih => + intro a ha + exact (weight_le_succ hk (by omega)).trans (ih (a + 1) (by omega)) + exact key (i - a) a (by omega) + · have key : ∀ m, (k * i).choose (i + m) * (k - 1) ^ (k * i - (i + m)) ≤ + (k * i).choose i * (k - 1) ^ (k * i - i) := by + intro m + induction m with | zero => rfl - | succ k ih => exact (weight_succ_le (i := j + k) (by omega)).trans ih - obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hij - exact key k - -/-- **The middle binomial coefficient of `(1 + 2) ^ {3j}`**: `27^j ≤ C(3j, j) 4^j (3j + 1)`, since -the middle weight is the largest of the `3 j + 1` weights summing to `27^j`. -/ -theorem pow_le_choose_mul (j : ℕ) : 27 ^ j ≤ (3 * j).choose j * 4 ^ j * (3 * j + 1) := by - have hsum : 27 ^ j = ∑ i ∈ range (3 * j + 1), (3 * j).choose i * 2 ^ (3 * j - i) := by - have h := add_pow (1 : ℕ) 2 (3 * j) - rw [show (1 : ℕ) + 2 = 3 by rfl, show (3 : ℕ) ^ (3 * j) = 27 ^ j by - rw [pow_mul]; norm_num] at h + | succ m ih => exact (weight_succ_le (a := i + m) hk (by omega)).trans ih + obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le hai + exact key m + +/-- **The middle binomial weight**: `k^{ki} ≤ C(ki, i) (k - 1)^{ki - i} (ki + 1)`, since the middle +weight is the largest of the `ki + 1` weights of `((k - 1) + 1)^{ki}`. -/ +theorem pow_le_choose_mul (hk : 1 ≤ k) (i : ℕ) : + k ^ (k * i) ≤ (k * i).choose i * (k - 1) ^ (k * i - i) * (k * i + 1) := by + have hsum : k ^ (k * i) = ∑ a ∈ range (k * i + 1), (k * i).choose a * (k - 1) ^ (k * i - a) := by + have h := add_pow (1 : ℕ) (k - 1) (k * i) + rw [show 1 + (k - 1) = k by omega] at h rw [h] - exact sum_congr rfl fun i _ => by rw [one_pow, one_mul, mul_comm, Nat.cast_id] + exact sum_congr rfl fun a _ => by rw [one_pow, one_mul, mul_comm, Nat.cast_id] rw [hsum] calc - ∑ i ∈ range (3 * j + 1), (3 * j).choose i * 2 ^ (3 * j - i) ≤ - ∑ _i ∈ range (3 * j + 1), (3 * j).choose j * 2 ^ (3 * j - j) := - sum_le_sum fun i _ => weight_le_middle j i - _ = (3 * j).choose j * 4 ^ j * (3 * j + 1) := by - rw [sum_const, card_range, smul_eq_mul, show 3 * j - j = 2 * j by omega, pow_mul] - norm_num - ring - -/-- From distance `j`, the biased walk reaches `0` within `3 j` steps with probability at least -`2^{-j} / (3 j + 1)`. -/ -theorem inv_le_hit (j : ℕ) : (1 / 2 : ℝ) ^ j / (3 * j + 1) ≤ hit (3 * j) j := by - have hpath := choose_mul_le_hit j (2 * j) j (by omega) - rw [show j + 2 * j = 3 * j by omega] at hpath - refine le_trans ?_ hpath - have hbin : (27 : ℝ) ^ j ≤ (3 * j).choose j * 4 ^ j * (3 * j + 1) := by - exact_mod_cast pow_le_choose_mul j - have hpos : (0 : ℝ) < 3 * j + 1 := by positivity - have hx : (0 : ℝ) < 2 ^ j := by positivity - have hy : (0 : ℝ) < 27 ^ j := by positivity - rw [show (4 : ℝ) ^ j = 2 ^ j * 2 ^ j by rw [← mul_pow]; norm_num] at hbin - have hweight : ((3 * j).choose j : ℝ) * (1 / 3) ^ (2 * j) * (2 / 3) ^ j = - (3 * j).choose j * (2 ^ j / 27 ^ j) := by - rw [mul_assoc, pow_mul, ← mul_pow] - norm_num [div_pow] - rw [hweight, div_le_iff₀ hpos, one_div_pow, div_le_iff₀ hx] - have hrhs : ((3 * j).choose j : ℝ) * (2 ^ j / 27 ^ j) * (3 * j + 1) * 2 ^ j = - ((3 * j).choose j * (2 ^ j * 2 ^ j) * (3 * j + 1)) / 27 ^ j := by - field_simp - rw [hrhs, le_div_iff₀ hy, one_mul] - exact hbin + ∑ a ∈ range (k * i + 1), (k * i).choose a * (k - 1) ^ (k * i - a) ≤ + ∑ _a ∈ range (k * i + 1), (k * i).choose i * (k - 1) ^ (k * i - i) := + sum_le_sum fun a _ => weight_le_middle hk i a + _ = (k * i).choose i * (k - 1) ^ (k * i - i) * (k * i + 1) := by + rw [sum_const, card_range, smul_eq_mul, mul_comm] + +/-- From distance `d`, the biased walk reaches `0` within `3 d` steps with probability at least +`((k - 1)/k)^{k - 3} (k - 1)^{-d} / (3 d + 1)`, for `k ≥ 3`. Write `d = (k - 2) i + e` with +`e < k - 2`; the paths with `i` up-steps and `i + d` down-steps have length `ki + e ≤ 3d`. -/ +theorem inv_le_hit (hk : 3 ≤ k) (d : ℕ) : + (((k : ℝ) - 1) / k) ^ (k - 3) * (1 / ((k : ℝ) - 1)) ^ d / (3 * d + 1) ≤ hit k (3 * d) d := by + set i := d / (k - 2) + set e := d % (k - 2) + have hdie : (k - 2) * i + e = d := Nat.div_add_mod d (k - 2) + have he : e ≤ k - 3 := by + have := Nat.mod_lt d (show 0 < k - 2 by omega) + omega + have hlen : i + (i + d) = k * i + e := by + rw [← hdie] + obtain ⟨k', rfl⟩ : ∃ k', k = k' + 2 := ⟨k - 2, by omega⟩ + simp only [Nat.add_sub_cancel] + ring + have hid : i ≤ d := Nat.div_le_self d (k - 2) + have hki : k * i ≤ 3 * d := by omega + have hpath := choose_mul_le_hit (by omega : 1 ≤ k) i (i + d) d (by omega) + have hmono : hit k (i + (i + d)) d ≤ hit k (3 * d) d := + hit_monotone (by omega) d (by omega) + refine le_trans ?_ (hpath.trans hmono) + -- The natural-number inequality behind the bound. + have hmode := pow_le_choose_mul (by omega : 1 ≤ k) i + have hnat : (k - 1) ^ (k - 3) * k ^ (i + (i + d)) ≤ + (i + (i + d)).choose i * (k - 1) ^ (i + d) * k ^ (k - 3) * (3 * d + 1) := by + obtain ⟨f, hf⟩ : ∃ f, k - 3 = e + f := ⟨k - 3 - e, by omega⟩ + have hid' : i + d = (k * i - i) + e := by omega + rw [hlen, hf, hid', pow_add, pow_add, pow_add, pow_add] + calc + (k - 1) ^ e * (k - 1) ^ f * (k ^ (k * i) * k ^ e) ≤ + (k - 1) ^ e * (k - 1) ^ f * + ((k * i).choose i * (k - 1) ^ (k * i - i) * (k * i + 1) * k ^ e) := by gcongr + _ ≤ (k - 1) ^ e * k ^ f * + ((k * i).choose i * (k - 1) ^ (k * i - i) * (k * i + 1) * k ^ e) := by + gcongr + omega + _ = (k * i).choose i * ((k - 1) ^ (k * i - i) * (k - 1) ^ e) * (k ^ e * k ^ f) * + (k * i + 1) := by ring + _ ≤ (k * i + e).choose i * ((k - 1) ^ (k * i - i) * (k - 1) ^ e) * (k ^ e * k ^ f) * + (3 * d + 1) := by + gcongr + omega + -- Transfer to the reals. + have hk1 : (1 : ℝ) ≤ (k : ℝ) - 1 := by + have : (3 : ℝ) ≤ k := by exact_mod_cast hk + linarith + have hk0 : (0 : ℝ) < k := by linarith + have hcast : ((k - 1 : ℕ) : ℝ) = (k : ℝ) - 1 := by + rw [Nat.cast_sub (by omega), Nat.cast_one] + have hreal : ((k : ℝ) - 1) ^ (k - 3) * (k : ℝ) ^ (i + (i + d)) ≤ + ((i + (i + d)).choose i : ℝ) * ((k : ℝ) - 1) ^ (i + d) * (k : ℝ) ^ (k - 3) * + (3 * d + 1) := by + rw [← hcast] + exact_mod_cast hnat + have hpos1 : (0 : ℝ) < ((k : ℝ) - 1) := by linarith + rw [div_le_iff₀ (by positivity)] + rw [div_pow, div_pow, div_pow, one_pow, one_pow] + rw [show ((k : ℝ) - 1) ^ (k - 3) / (k : ℝ) ^ (k - 3) * (1 / ((k : ℝ) - 1) ^ d) = + ((k : ℝ) - 1) ^ (k - 3) / ((k : ℝ) ^ (k - 3) * ((k : ℝ) - 1) ^ d) by + field_simp] + rw [div_le_iff₀ (by positivity)] + have hsplit : (k : ℝ) ^ (i + (i + d)) = (k : ℝ) ^ (i + d) * (k : ℝ) ^ i := by + rw [← pow_add] + congr 1 + ring + calc + ((k : ℝ) - 1) ^ (k - 3) = + ((k : ℝ) - 1) ^ (k - 3) * (k : ℝ) ^ (i + (i + d)) / (k : ℝ) ^ (i + (i + d)) := by + field_simp + _ ≤ ((i + (i + d)).choose i : ℝ) * ((k : ℝ) - 1) ^ (i + d) * (k : ℝ) ^ (k - 3) * + (3 * d + 1) / (k : ℝ) ^ (i + (i + d)) := by gcongr + _ = ((i + (i + d)).choose i : ℝ) * (1 / (k : ℝ) ^ (i + d)) * + (((k : ℝ) - 1) / (k : ℝ)) ^ i * (3 * d + 1) * + ((k : ℝ) ^ (k - 3) * ((k : ℝ) - 1) ^ d) := by + rw [hsplit, div_pow] + have hdd : ((k : ℝ) - 1) ^ (i + d) = ((k : ℝ) - 1) ^ i * ((k : ℝ) - 1) ^ d := pow_add _ _ _ + rw [hdd] + field_simp /-! ### The local search dominates the biased walk -/ @@ -380,11 +477,11 @@ private theorem succeedProb_flipStep_bind (φ : CNF V) {c : Clause V} (hc : c.le ENNReal.toReal_natCast, Function.comp_apply, succeedProb] /-- **The local search dominates the biased walk.** If `σ⋆` satisfies `φ` and every clause of `φ` -has at most three literals, then `t` steps from `σ` reach a satisfying assignment with probability -at least `hit t (dist σ σ⋆)`. -/ -theorem hit_le_succeedProb {φ : CNF V} {σs : V → Bool} (hs : φ.eval σs = true) - (h3 : ∀ c ∈ φ, c.length ≤ 3) (t : ℕ) (σ : V → Bool) : - hit t (hammingDist σ σs) ≤ succeedProb φ (walk φ t σ) := by +has at most `k ≥ 1` literals, then `t` steps from `σ` reach a satisfying assignment with probability +at least `hit k t (dist σ σ⋆)`. -/ +theorem hit_le_succeedProb (hk : 1 ≤ k) {φ : CNF V} {σs : V → Bool} (hs : φ.eval σs = true) + (h3 : ∀ c ∈ φ, c.length ≤ k) (t : ℕ) (σ : V → Bool) : + hit k t (hammingDist σ σs) ≤ succeedProb φ (walk φ t σ) := by induction t generalizing σ with | zero => rw [walk, succeedProb_pure] @@ -404,7 +501,7 @@ theorem hit_le_succeedProb {φ : CNF V} {σs : V → Bool} (hs : φ.eval σs = t have := List.find?_eq_none.mp hfu c hc simpa using this simp only [succeedProb_pure, hsat, ite_true] - exact hit_le_one _ _ + exact hit_le_one hk _ _ | some c => have hc : c ∈ φ := List.mem_of_find?_eq_some hfu have hcσ : ∀ l ∈ c, σ l.1 ≠ l.2 := by @@ -424,80 +521,101 @@ theorem hit_le_succeedProb {φ : CNF V} {σs : V → Bool} (hs : φ.eval σs = t rw [hd, hit_succ_succ, succeedProb_flipStep_bind φ hlen] set f : Fin c.length → ℝ := fun i => succeedProb φ (walk φ t (flip σ (c.get i).1)) obtain ⟨i₀, hi₀⟩ := List.get_of_mem hl - have hterm : ∀ i, hit t (d + 2) ≤ f i := by + have hterm : ∀ i, hit k t (d + 2) ≤ f i := by intro i - refine le_trans (hit_antitone t ?_) (ih _) + refine le_trans (hit_antitone hk t ?_) (ih _) rw [hammingDist_flip, hd] split_ifs <;> omega - have hterm₀ : hit t d ≤ f i₀ := by + have hterm₀ : hit k t d ≤ f i₀ := by refine le_trans (le_of_eq ?_) (ih _) rw [hi₀, hammingDist_flip, hd] simp [hne] - have hsum : hit t d + ((c.length : ℝ) - 1) * hit t (d + 2) ≤ ∑ i, f i := by + have hsum : hit k t d + ((c.length : ℝ) - 1) * hit k t (d + 2) ≤ ∑ i, f i := by rw [← add_sum_erase _ _ (mem_univ i₀)] - have hcard : ((c.length : ℝ) - 1) * hit t (d + 2) = - ∑ _i ∈ univ.erase i₀, hit t (d + 2) := by + have hcard : ((c.length : ℝ) - 1) * hit k t (d + 2) = + ∑ _i ∈ univ.erase i₀, hit k t (d + 2) := by rw [sum_const, card_erase_of_mem (mem_univ _), card_univ, Fintype.card_fin, nsmul_eq_mul, Nat.cast_sub (Nat.one_le_iff_ne_zero.mpr hlen), Nat.cast_one] rw [hcard] exact add_le_add hterm₀ (sum_le_sum fun i _ => hterm i) rw [← mul_sum] - have hm3 : (c.length : ℝ) ≤ 3 := by exact_mod_cast h3 c hc + have hm3 : (c.length : ℝ) ≤ k := by exact_mod_cast h3 c hc have hm1 : (1 : ℝ) ≤ c.length := by exact_mod_cast Nat.one_le_iff_ne_zero.mpr hlen - have hAB : hit t (d + 2) ≤ hit t d := hit_antitone t (by omega) - have hB := hit_nonneg t (d + 2) + have hAB : hit k t (d + 2) ≤ hit k t d := hit_antitone hk t (by omega) + have hB := hit_nonneg hk t (d + 2) calc - hit t d / 3 + 2 * hit t (d + 2) / 3 ≤ - (c.length : ℝ)⁻¹ * (hit t d + ((c.length : ℝ) - 1) * hit t (d + 2)) := by - rw [inv_mul_eq_div, le_div_iff₀ (by linarith)] + (hit k t d + ((k : ℝ) - 1) * hit k t (d + 2)) / k ≤ + (c.length : ℝ)⁻¹ * (hit k t d + ((c.length : ℝ) - 1) * hit k t (d + 2)) := by + rw [inv_mul_eq_div, div_le_div_iff₀ (by linarith) (by linarith)] nlinarith [mul_nonneg (sub_nonneg.mpr hAB) (sub_nonneg.mpr hm3)] _ ≤ (c.length : ℝ)⁻¹ * ∑ i, f i := by gcongr /-! ### Schöning's bound -/ omit [DecidableEq V] in -/-- Averaging `2^{-dist(σ, τ)}` over all assignments `σ` gives `(3/2)^n`, a product over the +/-- Averaging `q^{dist(σ, τ)}` over all assignments `σ` gives `(1 + q)^n`, a product over the coordinates. -/ -theorem sum_half_pow_hammingDist [DecidableEq V] (τ : V → Bool) : - ∑ σ : V → Bool, (1 / 2 : ℝ) ^ hammingDist σ τ = (3 / 2) ^ Fintype.card V := by - have hprod (σ : V → Bool) : - (1 / 2 : ℝ) ^ hammingDist σ τ = ∏ i, if σ i = τ i then 1 else 1 / 2 := by +theorem sum_pow_hammingDist [DecidableEq V] (q : ℝ) (τ : V → Bool) : + ∑ σ : V → Bool, q ^ hammingDist σ τ = (1 + q) ^ Fintype.card V := by + have hprod (σ : V → Bool) : q ^ hammingDist σ τ = ∏ i, if σ i = τ i then 1 else q := by rw [prod_ite, prod_const_one, one_mul, prod_const] rfl simp only [hprod] - rw [← Fintype.prod_sum (fun i b => if b = τ i then (1 : ℝ) else 1 / 2)] - have hb (i : V) : ∑ b : Bool, (if b = τ i then (1 : ℝ) else 1 / 2) = 3 / 2 := by + rw [← Fintype.prod_sum (fun i b => if b = τ i then (1 : ℝ) else q)] + have hb (i : V) : ∑ b : Bool, (if b = τ i then (1 : ℝ) else q) = 1 + q := by rw [Fintype.sum_bool] - cases τ i <;> norm_num + cases τ i <;> simp [add_comm] simp only [hb, prod_const, card_univ] -/-- **Schöning's theorem for 3-SAT, one trial.** For a satisfiable CNF formula on `n` variables -whose clauses have at most three literals, one trial of Schöning's algorithm finds a satisfying -assignment with probability at least `(3 / 4) ^ n / (3 n + 1)`. -/ -theorem trial_success {φ : CNF V} (hφ : φ.Satisfiable) (h3 : ∀ c ∈ φ, c.length ≤ 3) : - (3 / 4 : ℝ) ^ Fintype.card V / (3 * Fintype.card V + 1) ≤ succeedProb φ (trial φ) := by +/-- **Schöning's theorem for k-SAT, one trial.** For `k ≥ 3` and a satisfiable CNF formula on `n` +variables whose clauses have at most `k` literals, one trial of Schöning's algorithm finds a +satisfying assignment with probability at least +`((k - 1)/k)^{k - 3} (k / (2 (k - 1)))^n / (3 n + 1)`. -/ +theorem trial_success_of_length_le (hk : 3 ≤ k) {φ : CNF V} (hφ : φ.Satisfiable) + (hlen : ∀ c ∈ φ, c.length ≤ k) : + (((k : ℝ) - 1) / k) ^ (k - 3) * ((k : ℝ) / (2 * ((k : ℝ) - 1))) ^ Fintype.card V / + (3 * Fintype.card V + 1) ≤ succeedProb φ (trial φ) := by obtain ⟨σs, hs⟩ := hφ set n := Fintype.card V - have hlow (σ : V → Bool) : - (1 / 2 : ℝ) ^ hammingDist σ σs / (3 * n + 1) ≤ succeedProb φ (walk φ (3 * n) σ) := by + have hk1 : (1 : ℝ) < (k : ℝ) - 1 := by + have : (3 : ℝ) ≤ k := by exact_mod_cast hk + linarith + set c := (((k : ℝ) - 1) / k) ^ (k - 3) + have hc : 0 ≤ c := by positivity + have hlow (σ : V → Bool) : c * (1 / ((k : ℝ) - 1)) ^ hammingDist σ σs / (3 * n + 1) ≤ + succeedProb φ (walk φ (3 * n) σ) := by have hd : hammingDist σ σs ≤ n := hammingDist_le_card_fintype calc - (1 / 2 : ℝ) ^ hammingDist σ σs / (3 * n + 1) ≤ - (1 / 2 : ℝ) ^ hammingDist σ σs / (3 * hammingDist σ σs + 1) := by + c * (1 / ((k : ℝ) - 1)) ^ hammingDist σ σs / (3 * n + 1) ≤ + c * (1 / ((k : ℝ) - 1)) ^ hammingDist σ σs / (3 * hammingDist σ σs + 1) := by gcongr - _ ≤ hit (3 * hammingDist σ σs) (hammingDist σ σs) := inv_le_hit _ - _ ≤ hit (3 * n) (hammingDist σ σs) := hit_monotone _ (by omega) - _ ≤ _ := hit_le_succeedProb hs h3 _ σ + _ ≤ hit k (3 * hammingDist σ σs) (hammingDist σ σs) := inv_le_hit hk _ + _ ≤ hit k (3 * n) (hammingDist σ σs) := hit_monotone (by omega) _ (by omega) + _ ≤ _ := hit_le_succeedProb (by omega) hs hlen _ σ rw [trial, succeedProb, Cslib.Probability.PMF.toOuterMeasure_bind_toReal] simp only [Cslib.Probability.PMF.uniformOfFintype_apply, ENNReal.toReal_inv, Fintype.card_fun, Fintype.card_bool, Nat.cast_pow, Nat.cast_ofNat] calc - (3 / 4 : ℝ) ^ n / (3 * n + 1) = - ∑ σ : V → Bool, ((2 : ℝ) ^ n)⁻¹ * ((1 / 2 : ℝ) ^ hammingDist σ σs / (3 * n + 1)) := by - rw [← mul_sum, ← sum_div, sum_half_pow_hammingDist, ← mul_div_assoc, ← inv_pow, ← mul_pow] - norm_num + c * ((k : ℝ) / (2 * ((k : ℝ) - 1))) ^ n / (3 * n + 1) = + ∑ σ : V → Bool, ((2 : ℝ) ^ n)⁻¹ * + (c * (1 / ((k : ℝ) - 1)) ^ hammingDist σ σs / (3 * n + 1)) := by + rw [← mul_sum, ← sum_div, ← mul_sum, sum_pow_hammingDist] + have : (1 + 1 / ((k : ℝ) - 1)) = (k : ℝ) / ((k : ℝ) - 1) := by + field_simp + ring + rw [this, div_pow, div_pow, mul_pow, show Fintype.card V = n from rfl] + field_simp _ ≤ ∑ σ : V → Bool, ((2 : ℝ) ^ n)⁻¹ * succeedProb φ (walk φ (3 * n) σ) := by gcongr with σ exact hlow σ +/-- **Schöning's theorem for 3-SAT, one trial.** For a satisfiable CNF formula on `n` variables +whose clauses have at most three literals, one trial of Schöning's algorithm finds a satisfying +assignment with probability at least `(3 / 4) ^ n / (3 n + 1)`. -/ +theorem trial_success {φ : CNF V} (hφ : φ.Satisfiable) (h3 : ∀ c ∈ φ, c.length ≤ 3) : + (3 / 4 : ℝ) ^ Fintype.card V / (3 * Fintype.card V + 1) ≤ succeedProb φ (trial φ) := by + have h := trial_success_of_length_le (le_refl 3) hφ h3 + norm_num at h ⊢ + exact h + end Cslib.Complexity.Schoening diff --git a/ComplexityTests/Schoening.lean b/ComplexityTests/Schoening.lean index ed7c33b711..b4a177c468 100644 --- a/ComplexityTests/Schoening.lean +++ b/ComplexityTests/Schoening.lean @@ -29,13 +29,25 @@ example : (3 / 4 : ℝ) ^ 3 / (3 * 3 + 1) ≤ succeedProb φ (trial φ) := by example : succeedProb φ (walk φ 0 fun _ => true) = 1 := by rw [walk, succeedProb_pure, ite_eq_left (by decide)] --- The biased walk: from distance one, three steps reach `0` with probability `1/3 + 2/9 * 1/3`. -example : hit 3 1 = 1 / 3 + 2 / 3 * (1 / 3 * (1 / 3)) := by +-- The biased walk for `k = 3`: from distance one, three steps reach `0` with probability +-- `1/3 + 2/3 · 1/3 · 1/3`. +example : hit 3 3 1 = 1 / 3 + 2 / 3 * (1 / 3 * (1 / 3)) := by simp only [hit_succ_succ, hit_zero_right, hit_zero_succ] norm_num --- The middle binomial bound at `j = 2`: `27² ≤ C(6, 2) · 4² · 7`. -example : 27 ^ 2 ≤ (3 * 2).choose 2 * 4 ^ 2 * (3 * 2 + 1) := pow_le_choose_mul 2 +-- The middle binomial bound for `k = 3`, `i = 2`: `3⁶ ≤ C(6, 2) · 2⁴ · 7`. +example : 3 ^ (3 * 2) ≤ (3 * 2).choose 2 * (3 - 1) ^ (3 * 2 - 2) * (3 * 2 + 1) := + pow_le_choose_mul (by norm_num) 2 + +/-- `(x₀ ∨ x₁ ∨ x₂ ∨ x₃)`: a satisfiable 4-CNF on four variables. -/ +def ψ : CNF (Fin 4) := [[(0, true), (1, true), (2, true), (3, true)]] + +-- The general bound applies with `k = 4`: `(3/4) · (2/3)⁴ / 13`. +example : (3 / 4 : ℝ) * (2 / 3) ^ 4 / 13 ≤ succeedProb ψ (trial ψ) := by + have h := trial_success_of_length_le (k := 4) (by norm_num) (φ := ψ) + ⟨fun _ => true, by decide⟩ (by decide) + norm_num at h ⊢ + linarith /-- info: 'Cslib.Complexity.Schoening.hit_le_succeedProb' depends on axioms: @@ -44,6 +56,13 @@ info: 'Cslib.Complexity.Schoening.hit_le_succeedProb' depends on axioms: #guard_msgs (whitespace := lax) in #print axioms hit_le_succeedProb +/-- +info: 'Cslib.Complexity.Schoening.trial_success_of_length_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms trial_success_of_length_le + /-- info: 'Cslib.Complexity.Schoening.trial_success' depends on axioms: [propext, Classical.choice, Quot.sound] diff --git a/ROADMAP.md b/ROADMAP.md index cd95540be5..af6ceb5809 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -584,7 +584,7 @@ developments, not assertions that every prerequisite is missing or assignments t | Proof complexity | Build on [Cook–Reckhow systems and simulations](Complexity/Computability/Complexity/ProofSystem.lean), including the polynomially bounded-system characterization of NP = coNP, the [resolution size–width tradeoff](Complexity/Logics/Propositional/Resolution/SizeWidth.lean), [tree-like resolution/DPLL search-tree certificates](Complexity/Logics/Propositional/Resolution/TreeLike.lean), [Tseitin formulas on expanders](Complexity/Logics/Propositional/Resolution/TseitinExpander.lean) and [Haken's pigeonhole lower bound](Complexity/Logics/Propositional/Resolution/Pigeonhole.lean). Extend proof-space lower bounds, Frege, cutting planes, polynomial calculus and sum-of-squares. The certificate correspondence does not certify a DPLL solver's runtime. | | Average-case complexity and learning | Uniform-distribution learning on CSLib's PAC API, the LMN low-degree algorithm and Kushilevitz–Mansour with membership queries are [proved](Complexity/MachineLearning/UniformLearning/KushilevitzMansour.lean); running times are not machine-certified. Distributional problems and reductions, samplability, average-to-worst-case connections, PAC/agnostic/SQ learning, learning lower bounds, compression and refutation. Existing cryptographic learners are starting points, not coverage of learning theory. | | Property and distribution testing | Distance and access models, one/two-sided and tolerant testing, query/sample bounds, canonical graph/algebraic/distribution testers and lower bounds. | -| Fine-grained and parameterized complexity | Under ETH, 3-coloring, independent set, vertex cover and Hamiltonian cycle and path have no 2^{o(\|V\|+\|E\|)} algorithms and clique none in 2^{o(\|V\|)} ([GraphProblems](Complexity/Computability/Complexity/FineGrained/GraphProblems.lean)); the Hamiltonian bounds (directed and undirected) use linear-size diamond reductions. [FPT and XP](Complexity/Computability/Complexity/Parameterized.lean) are defined with arbitrary (not necessarily computable) `f`; `P ⊆ FPT ⊆ XP`, Boolean closure of FPT (complement for XP), closure under fpt-reductions and `FPT = XP = P` for bounded parameters are proved, and SAT is in FPT for the number of variables. [Kernelization](Complexity/Computability/Complexity/Parameterized/Kernelization.lean) (`IsKernelization`, `HasKernel`, `HasPolyKernel`) and the Cai–Chen–Downey–Fellows equivalence (`A ∈ FPT enc κ ↔ HasKernel enc κ A` for `A ∈ DTIME enc t` over a nonempty instance type) are proved, and [VertexCover](Complexity/Computability/Complexity/Parameterized/VertexCover.lean) is in FPT parameterized by target size `k` in time `O(2^k (|x|+1)^e)` by a bounded search tree and has [Buss's polynomial kernel](Complexity/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean) with at most `k(k+2)` vertices and encoded length at most `40(k+1)^6` (`VertexCover_hasPolyKernel`). On the algorithmic side, one trial of [Schöning's random walk](Complexity/Computability/Complexity/FineGrained/Schoening.lean) finds a satisfying assignment of a satisfiable 3-CNF with probability at least `(3/4)^n / (3n + 1)`; general `k`, amplification, a time bound and PPSZ remain (#894). Further fine-grained reductions and consequences conditional on ETH/SETH and other named hypotheses; strongly uniform (computable `f`) variants, further explicit polynomial kernels, W/A hierarchies and parameterized lower bounds. | +| Fine-grained and parameterized complexity | Under ETH, 3-coloring, independent set, vertex cover and Hamiltonian cycle and path have no 2^{o(\|V\|+\|E\|)} algorithms and clique none in 2^{o(\|V\|)} ([GraphProblems](Complexity/Computability/Complexity/FineGrained/GraphProblems.lean)); the Hamiltonian bounds (directed and undirected) use linear-size diamond reductions. [FPT and XP](Complexity/Computability/Complexity/Parameterized.lean) are defined with arbitrary (not necessarily computable) `f`; `P ⊆ FPT ⊆ XP`, Boolean closure of FPT (complement for XP), closure under fpt-reductions and `FPT = XP = P` for bounded parameters are proved, and SAT is in FPT for the number of variables. [Kernelization](Complexity/Computability/Complexity/Parameterized/Kernelization.lean) (`IsKernelization`, `HasKernel`, `HasPolyKernel`) and the Cai–Chen–Downey–Fellows equivalence (`A ∈ FPT enc κ ↔ HasKernel enc κ A` for `A ∈ DTIME enc t` over a nonempty instance type) are proved, and [VertexCover](Complexity/Computability/Complexity/Parameterized/VertexCover.lean) is in FPT parameterized by target size `k` in time `O(2^k (|x|+1)^e)` by a bounded search tree and has [Buss's polynomial kernel](Complexity/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean) with at most `k(k+2)` vertices and encoded length at most `40(k+1)^6` (`VertexCover_hasPolyKernel`). On the algorithmic side, one trial of [Schöning's random walk](Complexity/Computability/Complexity/FineGrained/Schoening.lean) finds a satisfying assignment of a satisfiable k-CNF with probability at least `((k-1)/k)^(k-3) (k/(2(k-1)))^n / (3n + 1)`, which is `(3/4)^n / (3n + 1)` for 3-SAT; amplification, a time bound and PPSZ remain (#894). Further fine-grained reductions and consequences conditional on ETH/SETH and other named hypotheses; strongly uniform (computable `f`) variants, further explicit polynomial kernels, W/A hierarchies and parameterized lower bounds. | | Total search and computational games | Build on [FNP, FP and TFNP with search reductions](Complexity/Computability/Complexity/Classes/TFNP.lean), including `FP = FNP` exactly when `P = NP` ([search to decision](Complexity/Computability/Complexity/Classes/TFNP/SearchToDecision.lean)), `TFNP ⊆ FP → NP ∩ coNP ⊆ P`, and the canonical subclasses [PLS, PPP, PPAD and PPA](Complexity/Computability/Complexity/Classes/TFNP/Subclasses.lean) with their combinatorial totality principles ([Principles](Complexity/Computability/Complexity/Classes/TFNP/Subclasses/Principles.lean)), inclusions `PLS, PPP, PPAD, PPA ⊆ TFNP`, `PPAD ⊆ PPP`, and `PPAD ⊆ PPA`, and De Morgan circuit problems (`LocalOpt ∈ PLS`, `Pigeon ∈ PPP`, `EndOfLine ∈ PPAD`, `Leaf ∈ PPA`). Their [completeness](Complexity/Computability/Complexity/Classes/TFNP/Subclasses/Completeness.lean) now follows from polynomial-time construction of function-family circuit codes, preserving binary local-search costs. Develop CLS, further local search, fixed-point and equilibrium problems. | | Logic and descriptive complexity | Building on [Fagin's theorem](Complexity/Computability/Complexity/Fagin/Converse.lean): logical characterizations of additional resource classes, fixed-point and order-invariant queries, and uniform translations between syntax, structures and algorithms. | | Kolmogorov complexity and metacomplexity | Build on [plain Kolmogorov uncomputability](Complexity/Computability/Kolmogorov/Uncomputability.lean), [single-tape and Post–Turing (`TM0`/`TM1`) description methods and simulations](Complexity/Computability/Kolmogorov/SingleTape.lean), and [multi-tape description methods and `Partrec` optimality](Complexity/Computability/Kolmogorov/MultiTape.lean) (#318): `ofTM0` and `ofTM1` are defined through the `SingleTapeTM` embeddings of Mathlib's `TM0`/`TM1`; `ofSingleTapeTM` (and `ofTM0`) are simulated by `ofMultiTapeTM` with zero program overhead and linear time overhead (single-tape → multi-tape only; the reverse simulation is not formalized); and each of `ofSingleTapeTM`, `ofTM0`, `ofTM1` and `ofMultiTapeTM`, pushed forward along a computable decoder, is simulated by the universal partial-recursive description method `universal` with additive overhead. Extend prefix-free complexity, resource-bounded MCSP variants and connections to learning, cryptography and lower bounds. |