A better algorithm for random k-SAT

1.1 Solving random k-SAT

• Random k-SAT heuristics target efficiently solving most random instances even though k-SAT is NP-hard.Source: §1.1 · p. 1
• Pure literal rules repeatedly assign variables appearing with only one polarity and simplify the formula.Source: §1.1 · p. 1
• Unit clause propagation satisfies a clause containing only one literal, then simplifies the formula and repeats.Source: §1.1 · p. 1
• Walksat repeatedly selects an unsatisfied clause and randomly flips a variable occurring in it.Source: §1.1 · p. 1
• Backtracking recursively assigns variables and reverses an assignment when the chosen branch fails.Source: §1.1 · p. 1

1 INTRODUCTION 2

• Before this work, no algorithm was known to find satisfying assignments with probability Ω(1) beyond O(2^k/k), despite their existence over a larger density regime.Source: §1 · p. 2
• Fix is a polynomial-time algorithm that finds satisfying assignments w.h.p. for m/n ≤ (1−ε_k)2^k ln(k)/k, with ε_k → 0.Source: §1 · p. 2
• Fix is a combinatorial local-search algorithm with implementation time O((n + m)^(3/2)).Source: §1 · p. 2

1.2 A digression: replica symmetry breaking

• The dRSB hypothesis places a transition near 2^k ln(k)/k, where solution correlations change from local to long-range.Source: §1.2 · p. 2
• For densities above (1+ε_k)2^k ln(k)/k, most solutions have most variables frozen, suggesting local search is unlikely to succeed.Source: §1.2 · p. 2
• The discussion and theorem focus on large k, with no explicit ε_k bounds attempted for small k such as 3, 4, and 5.Source: §1.2 · p. 2

1.3 Related work

• Before Fix, SCB was the best rigorous result, succeeding at densities η_k2^k/k with η_k increasing to 1.817, while DPLL-type methods require exponential time beyond O(2^k/k).Source: §1.3 · p. 3
• Belief Propagation decimation has evidence for success up to e·2^k/k, but proving its performance remains open.Source: §1.3 · p. 3
• Survey Propagation has no evidence of finding satisfying assignments beyond O(2^k/k) for general k.Source: §1.3 · p. 3

1.4 Techniques and outline

• Earlier algorithms assign variables sequentially, simplify after each assignment, and usually do not revise previous decisions.Source: §1.4 · pp. 3–4
• Fix instead starts from a complete all-true assignment and greedily flips variables without generating new unsatisfied clauses.Source: §1.4 · p. 4
• Fix combines deferred decisions, martingale methods, and direct combinatorial analysis because its tracked random variables are more complex than in Unit Clause.Source: §1.4 · p. 4

2.1 Balls and bins

• A balls-and-bins lemma bounds the probability that fewer than half the expected empty bins remain, using Poissonization and Chernoff concentration.Source: §2.1 · pp. 4–5

2.2 Random k-SAT formulas

• The random formula is an ordered m-tuple of ordered k-tuples of literals, sampled uniformly with replacement from 2n literals.Source: §2.2 · p. 5
• For m = O(n), w.h.p. at most ln n clauses contain repeated variables, and no variable occurs in more than ln^2 n clauses.Source: §2.2 · pp. 5–6
• The proof bounds repeated-variable events by union and Markov inequalities, while variable occurrence counts use a binomial model and Chernoff bounds.Source: §2.2 · p. 6
• The section introduces filtrations, conditional expectations, a product-expectation lemma, and the Azuma-Hoeffding martingale tail bound.Source: §2.2 · p. 6
• A first-moment lemma controls clauses with few positive literals that intersect a small variable set at densities m/n ≤ 2^k k^−1 ln k.Source: §2.2 · p. 6

• The final probability expression is o(1).Source: §3 · p. 7

• For k ≥ k0 and sufficiently large n, Fix outputs a satisfying assignment w.h.p. at m = ⌊(1 −ε)2^k k^-1 ln k⌋.Here k0 depends on ε, and ε satisfies 0 < ε < 0.1.Source: §3 · p. 7
• Fix starts from the all-true assignment and selects variables Z to set false, prioritizing variables whose flipping does not create new unsatisfied clauses.A variable is Z-safe when it does not occur positively in a Z-unique clause.Source: §3 · p. 7
• Phase 1 processes all-negative clauses, choosing the least safe variable among the first k1 positions and otherwise selecting the variable in position k1.Source: §3 · p. 7

• The all-true assignment leaves (1 + o(1))2^-k m clauses unsatisfied w.h.p., while Phase 1 yields an assignment that is already substantially better.Source: §3 · p. 8

Phase 2

• Phase 2 defines endangered clauses as those relying on Z′ for satisfaction and constructs Z′ so every clause is secure or contains at least three variables from Z′.Source: §3 · p. 8
• Phase 2 greedily adds safe variables to Z′ while attempting to avoid variables whose positive occurrences could endanger other clauses.Source: §3 · p. 8
• The process executes at most n/3 iterations and produces |Z′| ≤ n k^-12 w.h.p.Source: §3 · p. 8

Phase 3

• The endangered clauses form a 3-SAT-like instance on Z′, and Fix uses a bipartite matching covering those clauses to assign its variables.The matching connects each endangered clause to the variables from Z′ that occur in it.Source: §3 · pp. 8–9
• The matching can be computed in O((n + m)3/2) time using Hopcroft–Karp.Source: §3 · p. 9

• Phase 3 produces a satisfying assignment w.h.p. because a matching covering all endangered clauses lets Fix satisfy both secure and endangered clauses.Source: §3 · p. 9

4 Proof of Proposition 3.2

• The argument assumes fixed 0 < ε < 0.1, sufficiently large k and n, and density m = floor((1−ε)2^k ln k/k).It sets ω = (1−ε) ln k and k_1 = ceil(k/2).Source: §4 · p. 9

4.1 Outline

• Phase 1 is represented by evolving sets Z_t, maps π_t, and a filtration F_t that records the process history.At each iteration one variable is added to Z_t, while π_t only reveals previously hidden literal identities; Fact 4.1 establishes measurability of the process variables.Source: §4.1 · pp. 9–10
• Conditioned on F_t, the unrevealed underlying variables are jointly uniform over V \ Z_t, enabling independent conditional estimates throughout the analysis.This is Proposition 4.2, proved by a bijection between assignments to unrevealed variables and formulas in the corresponding equivalence class.Source: §4.1 · p. 11
• With high probability, at most 2nω exp(−kt/n)/k clauses remain all-negative through time t, the process stops before 4nk^−1 ln ω iterations, and at least nk^(ε/2)−1 variables remain empty bins.These bounds come from Lemma 4.3, Corollary 4.4, and Corollary 4.6, and supply the structural controls used to prove Proposition 3.2.Source: §4.1 · pp. 11–12

4.2 Proof of Lemma 4.5

• With probability 1−o(1/n), at most (1+ε/9)Λ_l(t)n clauses in U_t have precisely l positive literals for every 1 ≤ l < k.Lemma 4.8 bounds the conditional probability of the relevant exposure events, yielding Lemma 4.9’s uniform count estimate.Source: §4.2 · pp. 14–15
• With high probability, at most n exp(−l) clauses have l ≥ ln k positive literals with at least l −1 literals in Zθ.The proof also bounds the corresponding cases with exactly l positive literals and l −1 in Zθ by 2λm clauses.Source: §4.2 · p. 16
• With high probability, at most (1 + ε/3)ωn clauses remain in Ut simultaneously for every t ≤ min{T, θ}.The proof combines Lemmas 4.10 and 4.9 after establishing bounds for each positive-literal count.Source: §4.2 · p. 16

4.3 Proof of Corollary 4.6

• The map ψt is shown to have conditional probabilities bounded by (n −s)^−|τ^−1(s)|, establishing its near-uniform behavior.This follows from conditional independence of the relevant literals and a three-case calculation for ψs(i).Source: §4.3 · pp. 17–18
• With high probability, for every t ≤ T, fewer than ν = nk−ε/2 variables outside Zt satisfy Ut(x) = 0.The argument compares ψt with uniform balls thrown into bins and applies Corollary 4.4 and Lemma 4.5.Source: §4.3 · p. 19

5.1 Outline

• At every t ≤ θ′, at least n k^(ε/3)−1 variables outside Z′_t have U′_t(x)=0 with high probability.The bound follows from the corresponding Phase 1 supply of variables and the estimate |U′_t \ U_T| ≤ n/k.Source: §5.1 · p. 20
• Phase 2 stops by time θ′ with high probability, implying |Z′_{T′}| = 3T′ and establishing Proposition 3.3.Each process step removes at least one endangered clause, so the stopping time is bounded by the initial number of such clauses, controlled by Corollary 5.6.Source: §5.1 · p. 20

5.3 Proof of Corollary 5.5

• With probability at least 1−o(1/n), no more than n exp(−k) clauses contain at least k/4 literals from Z_t in positions k_1<j≤k for any t≤θ.This estimate prepares the proof of Corollary 5.5 by ruling out clauses containing an exceptionally large number of exposed literals.Source: §5.3 · p. 24
• The proof of Corollary 5.5 combines independence, union bounds, moment estimates, Markov’s inequality, and Corollary 4.4 with Lemma 5.10 to derive its claimed high-probability bounds.In particular, the argument bounds Y′ via (47) and Y′′ by θδ with high probability, yielding the assertion.Source: §5.3 · p. 26

5.4 Proof of Corollary 5.6

• With high probability, the five classes of endangered clauses satisfy Xa + ··· + Xe ≤ θ′.The proof bounds Xa + Xb by O(ln n), Xc by exp(−kε/8)n, Xd by 2 exp(−κ/2)n, and uses Y ≤ 3θ′ exp(−kε/4) to control Xe.Source: §5.4 · p. 27

Setup

• With m = floor((1 − ε)2^k k^−1 ln k n), the proof establishes the parameter regime in which Proposition 3.4 is analyzed.It assumes sufficiently large k and n, with ω = (1 − ε) ln k and θ = floor(4n k^−1 ln ω).Source: §6 · p. 27

Probabilistic bound

• A first-moment argument bounds the probability that small sets Y and M satisfy the structural conditions required for a matching obstruction.The proof introduces events E(Y, t, M, L, Λ), bounds their probabilities using independence and union bounds, and extends the estimate to all relevant small sets.Source: §6 · pp. 27–28
• For every t ≤ θ, the obstruction event involving sets of size 3 ≤ |Y| = |M| ≤ n k^−1/2 has probability o(1/n).This is obtained from Corollary 6.4 and a union bound over the possible sets and parameters.Source: §6 · p. 29

Matching reduction

• The marriage-theorem argument reduces failure of the desired matching to sets Y and M of equal size whose endangered clauses have all neighbors inside Y.Each such clause must contain at least three variables from Z′, yielding |Y| = |M| ≥ 3 and the structural conditions used in the probabilistic bound.Source: §6 · pp. 27, 29

Conclusion

• The matching fails with probability o(1), because the remaining alternatives—an earlier exceptional event, |Z′| > n k^−1/2, or the bounded obstruction event—each occur with probability o(1).The final step combines Proposition 3.2, Proposition 3.3, and Corollary 6.5 over at most θ time steps.Source: §6 · p. 29