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 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.

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 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

• 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: 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

• U. Schöning, A probabilistic algorithm for k-SAT and constraint satisfaction problems

The algorithm

def Cslib.Complexity.Schoening.firstUnsat {V : Type u_1} (φ : Logic.PL.CNF V) (σ : V → Bool) : Option (Logic.PL.Clause V)

The first clause of φ that σ falsifies, if any.

noncomputable def Cslib.Complexity.Schoening.flipStep {V : Type u_1} [DecidableEq V] (c : Logic.PL.Clause V) (σ : V → Bool) : PMF (V → Bool)

Flip the variable of a uniformly chosen literal occurrence of c. The empty clause, which no assignment satisfies, leaves the assignment unchanged.

noncomputable def Cslib.Complexity.Schoening.walk {V : Type u_1} [DecidableEq V] (φ : Logic.PL.CNF V) : ℕ → (V → Bool) → PMF (V → Bool)

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 Cslib.Complexity.Schoening.trial {V : Type u_1} [Fintype V] [DecidableEq V] (φ : Logic.PL.CNF V) : PMF (V → Bool)

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 Cslib.Complexity.Schoening.succeedProb {V : Type u_1} (φ : Logic.PL.CNF V) (μ : PMF (V → Bool)) : ℝ

The probability that μ produces an assignment satisfying φ.

The biased walk

noncomputable def Cslib.Complexity.Schoening.hit (k : ℕ) : ℕ → ℕ → ℝ

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.

@[simp]

theorem Cslib.Complexity.Schoening.hit_zero_right (k t : ℕ) : hit k t 0 = 1

@[simp]

theorem Cslib.Complexity.Schoening.hit_zero_succ (k d : ℕ) : hit k 0 (d + 1) = 0

theorem Cslib.Complexity.Schoening.hit_succ_succ (k t d : ℕ) : hit k (t + 1) (d + 1) = (hit k t d + (↑k - 1) * hit k t (d + 2)) / ↑k

theorem Cslib.Complexity.Schoening.hit_nonneg {k : ℕ} (hk : 1 ≤ k) (t d : ℕ) : 0 ≤ hit k t d

theorem Cslib.Complexity.Schoening.hit_le_one {k : ℕ} (hk : 1 ≤ k) (t d : ℕ) : hit k t d ≤ 1

theorem Cslib.Complexity.Schoening.hit_succ_le {k : ℕ} (hk : 1 ≤ k) (t d : ℕ) : hit k t (d + 1) ≤ hit k t d

Hitting 0 is less likely from farther away.

theorem Cslib.Complexity.Schoening.hit_antitone {k : ℕ} (hk : 1 ≤ k) (t : ℕ) : Antitone (hit k t)

theorem Cslib.Complexity.Schoening.hit_le_hit_succ {k : ℕ} (hk : 1 ≤ k) (t d : ℕ) : hit k t d ≤ hit k (t + 1) d

Hitting 0 is more likely with more time.

theorem Cslib.Complexity.Schoening.hit_monotone {k : ℕ} (hk : 1 ≤ k) (d : ℕ) : Monotone fun (t : ℕ) => hit k t d

theorem Cslib.Complexity.Schoening.choose_mul_le_hit {k : ℕ} (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

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/k)^b ((k - 1)/k)^a.

The middle binomial weight

theorem Cslib.Complexity.Schoening.pow_le_choose_mul {k : ℕ} (hk : 1 ≤ k) (i : ℕ) : k ^ (k * i) ≤ (k * i).choose i * (k - 1) ^ (k * i - i) * (k * i + 1)

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 Cslib.Complexity.Schoening.inv_le_hit {k : ℕ} (hk : 3 ≤ k) (d : ℕ) : ((↑k - 1) / ↑k) ^ (k - 3) * (1 / (↑k - 1)) ^ d / (3 * ↑d + 1) ≤ hit k (3 * d) d

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.

The local search dominates the biased walk

theorem Cslib.Complexity.Schoening.succeedProb_pure {V : Type u_1} (φ : Logic.PL.CNF V) (σ : V → Bool) : succeedProb φ (PMF.pure σ) = if Logic.PL.CNF.eval σ φ = true then 1 else 0

theorem Cslib.Complexity.Schoening.succeedProb_nonneg {V : Type u_1} (φ : Logic.PL.CNF V) (μ : PMF (V → Bool)) : 0 ≤ succeedProb φ μ

theorem Cslib.Complexity.Schoening.hit_le_succeedProb {V : Type u_1} [Fintype V] [DecidableEq V] {k : ℕ} (hk : 1 ≤ k) {φ : Logic.PL.CNF V} {σs : V → Bool} (hs : Logic.PL.CNF.eval σs φ = true) (h3 : ∀ c ∈ φ, List.length c ≤ k) (t : ℕ) (σ : V → Bool) : hit k t (hammingDist σ σs) ≤ succeedProb φ (walk φ t σ)

The local search dominates the biased walk. If σ⋆ satisfies φ and every clause of φ has at most k ≥ 1 literals, then t steps from σ reach a satisfying assignment with probability at least hit k t (dist σ σ⋆).

Schöning's bound

theorem Cslib.Complexity.Schoening.sum_pow_hammingDist {V : Type u_1} [Fintype V] [DecidableEq V] (q : ℝ) (τ : V → Bool) : ∑ σ : V → Bool, q ^ hammingDist σ τ = (1 + q) ^ Fintype.card V

Averaging q^{dist(σ, τ)} over all assignments σ gives (1 + q)^n, a product over the coordinates.

theorem Cslib.Complexity.Schoening.trial_success_of_length_le {V : Type u_1} [Fintype V] [DecidableEq V] {k : ℕ} (hk : 3 ≤ k) {φ : Logic.PL.CNF V} (hφ : φ.Satisfiable) (hlen : ∀ c ∈ φ, List.length c ≤ k) : ((↑k - 1) / ↑k) ^ (k - 3) * (↑k / (2 * (↑k - 1))) ^ Fintype.card V / (3 * ↑(Fintype.card V) + 1) ≤ succeedProb φ (trial φ)

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 Cslib.Complexity.Schoening.trial_success {V : Type u_1} [Fintype V] [DecidableEq V] {φ : Logic.PL.CNF V} (hφ : φ.Satisfiable) (h3 : ∀ c ∈ φ, List.length c ≤ 3) : (3 / 4) ^ Fintype.card V / (3 * ↑(Fintype.card V) + 1) ≤ succeedProb φ (trial φ)

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).