Frontier track: exponential-time SAT algorithms (Schöning, PPSZ)

Status: available. M0 can be claimed now.

Targets

Schöning (FOCS 1999): k-SAT in randomized time O*((2 − 2/k)ⁿ), so (4/3)ⁿ for 3-SAT.
PPSZ: R. Paturi, P. Pudlák, M. Saks and F. Zane (FOCS 1998; JACM 2005), with Hertli's
analysis for general formulas (FOCS 2011). Verify exact constants.

These complement the ETH and SETH lower bounds in FineGrained/.

What's already here

Fine-grained material: FineGrained/ (BruteForce, Exponents, GraphProblems,
OrthogonalVectors, PermutationIndependentSet).
CNF types: Logics/Propositional/CNF.
Probabilistic programs (OracleComp, ProbComp).

Milestones

M0, design. The randomized-algorithm model and time convention: word-RAM or native machines,
and how the exponential bound is stated.
M1, the random-walk analysis. Schöning's success-probability bound.
M2, the algorithm. Schöning's algorithm with its time bound in the chosen model, plus an
abstract.
M3, the PPSZ encoding/critical-clause lemma and its unique-SAT bound.
M4, PPSZ for general formulas (optional, following Hertli).

Rules for every track

These follow the frontier program umbrella issue and AGENTS.md.

M0 is a short design milestone, posted as a comment here before any Lean. It pins the exact
theorem statements, with exact citations (paper, theorem or lemma number), the models and
encodings, and the open decisions for Samuel. Later milestones follow the design.
Faithfulness. Everything is faithful to the literature, or equivalent in a clear or proven
way. Label original lemmas. Never state more than is proved.
Plain-first (refactor(api): use plain computability in definitions and public statements; keep tidy for proofs #456, S4 (#456): delete the tidy computability calculus; keep only a machine-level kernel #862). No tidy computability in statements or proofs outside the Machines
kernel. Lower the tidy baseline if counts move.
PRs. One reviewable PR (≤ about 40 files) per milestone, with nonvacuous tests and #print axioms guards. Headline results get a curated abstract under the AGENTS.md rules.
Claims. Claim a milestone with an active status comment before starting. Nothing is locked;
rebase onto whatever lands first.

🤖 Generated with Claude Code

Status: active. worker-jetski-17d3679e claims M0 (scoped to M1) and M1 (the random-walk analysis for 3-SAT). Branch: feat/schoening-walk-894. M2–M4 stay available; M2's model decisions are listed below for Samuel.

M0 design (M1)

Sources. U. Schöning, A probabilistic algorithm for k-SAT and constraint satisfaction problems, FOCS 1999; journal version A Probabilistic Algorithm for k-SAT Based on Limited Local Search and Restart, Algorithmica 32 (2002). The target is the k = 3 case: each trial succeeds with probability at least about (3/4)ⁿ, giving (4/3)ⁿ·poly(n) expected trials.

Model for M1. M1 is pure probability over the existing Logics/Propositional/CNF types (CNF V = List (Clause V)), with V = Fin n. It lives in Complexity/Computability/Complexity/FineGrained/Schoening.lean, beside the ETH/SETH material, in namespace Cslib.Complexity.Schoening.

walk φ : ℕ → (Fin n → Bool) → PMF (Fin n → Bool): if σ satisfies φ (or no steps remain), stop. Otherwise take the first unsatisfied clause, pick one of its literal occurrences uniformly (PMF.ofMultiset), and flip that variable. The analysis does not use which unsatisfied clause is chosen.
trial φ: a uniform initial assignment, then walk φ (3 * n).

M1 headline (k = 3): for every satisfiable CNF on Fin n whose clauses have at most 3 literals,
Pr[trial φ ends in a satisfying assignment] ≥ (3/4)ⁿ / (3n + 1).

Proof outline:

Comparison with a biased walk, by induction on the step budget. Let hit t d be the probability that a walk going down with probability 1/3 and up with probability 2/3 reaches 0 from d within t steps. Then Pr[walk t σ succeeds] ≥ hit t (dist(σ, σ*)) for a fixed satisfying σ*. This uses only that some literal of the chosen clause moves toward σ*, and that hit t is antitone in d and monotone in t. No coupling is needed.
Path counting: hit (3j) j ≥ C(3j, j)·(1/3)^{2j}·(2/3)^j.
The binomial mode bound C(3j, j) ≥ (27/4)^j / (3j + 1).
Averaging 2^{-dist} over a uniform start gives exactly (3/4)ⁿ (a product over coordinates).

The explicit polynomial factor 1/(3n + 1) is our own constant, labelled as such; Schöning states the bound up to polynomial factors.

Not in M1 (open decisions for Samuel, M2):

General k, with bound (k / (2(k−1)))ⁿ. Its path count differs (j/(k−2) up-steps).
Amplification by ⌈(3n+1)(4/3)ⁿ⌉·c independent trials.
The time model for the "O*((4/3)ⁿ) time" claim: native machines, word-RAM, or a step count of the algorithm (default proposal: a step count first, machine certificates later).

— worker-jetski-17d3679e

worker-jetski-17d3679e: M1 for k = 3 is awaiting review in #908 (all six gates pass). Still open on this track: general k, amplification and the time model (M2, which needs Samuel's decision), and PPSZ (M3–M4).

worker-jetski-17d3679e: active on extending #908's analysis to general k (bound (k/(2(k−1)))ⁿ up to polynomial factors), on a branch stacked on #908.

feat(FineGrained): Schöning's bound for k-SAT (#894)

worker-jetski-17d3679e: I generalized #908 in place to k-SAT: trial_success_of_length_le gives ((k−1)/k)^{k−3}·(k/(2(k−1)))ⁿ/(3n+1) for every k ≥ 3, with 3-SAT as a corollary. It's awaiting review at e55fab79, and all six gates pass. M1 is now complete for all k. Amplification and the time model (M2) and PPSZ remain open.

worker-jetski-17d3679e: active on a bounded part of M3: PPZ for unique k-SAT (Paturi–Pudlák–Zane, Satisfiability Coding Lemma, FOCS 1997). The deliverable is:

Critical clauses. In a uniquely satisfiable formula, every variable x has a clause in which x's literal is the only true literal under the solution.
Forcing. Under a uniformly random variable order, x comes last among its critical clause's variables with probability at least 1/k. In that case x is forced by unit propagation.
The unique-SAT bound. One PPZ round outputs the solution with probability at least 2^{−(1−1/k)n}, by Jensen (AM–GM) on E[2^{−#unforced}].

This is the PPZ encoding lemma, not PPSZ: PPSZ's s-implication bound remains open in M3. Branch feat/ppz-894, independent of #908.

worker-jetski-17d3679e: PPZ for unique k-SAT is awaiting review in #928, with all six gates passing. Next, still active, I'm extending it to general satisfiable k-CNF through isolated solutions. The isolation lemma ∑_{σ∈S} 2^{I(σ)−n} ≥ 1 combined with x^{1/k} ≥ x gives the same 2^{−(1−1/k)n} bound. That work is stacked on #928.

worker-jetski-17d3679e: awaiting review: #930 (stacked on #928) handles general satisfiable formulas. One PPZ round finds a satisfying assignment with probability ≥ 2^{-(1-1/k)n}, using the isolation inequality. All six gates pass. M2 (time model and amplification) and PPSZ remain open.

feat(FineGrained): Schöning's random walk for 3-SAT succeeds with pro…

feat(FineGrained): Schöning's bound for k-SAT (#894)

feat(FineGrained): the satisfiability coding lemma and PPZ for unique…

feat(FineGrained): PPZ for satisfiable k-SAT via the isolation inequa…

feat(FineGrained): the satisfiability coding lemma and PPZ for unique…

awaiting review (worker-claude-e6cf7b0d-ppz-round, Claude Code, Opus). Handoff for M2.

feat(WordRAM/PPZ): one PPZ round on the randomized word RAM with its exact law #1954, PPZ round, stacked on feat(PPZ): lazy-order rounds and the forced-value scan on the word RAM #1949. roundProgram_spec: one round on the input encode φ halts within n(28L + 40) + 12L + 19 instructions with at most 2n rand calls, outputs whether the assignment it leaves satisfies φ, and leaves a partial assignment whose law is exactly PPZ.round φ. The lazy Fisher–Yates loop matches roundOn_succ step by step. The satisfaction check is Schöning's scan, renamed into the 32-register file.
feat(WordRAM/PPZ): the PPZ algorithm on the randomized word RAM #1960, PPZ amplification, stacked on feat(WordRAM/PPZ): one PPZ round on the randomized word RAM with its exact law #1954. ampProgram_spec on k :: c :: encode φ runs up to R = 2^⌈(k−1)n/k⌉ · c rounds, with the counter computed on the machine by Schöning's mulAdd and decCounter (renamed). It has no false positives and the exact law repeatRound φ R. ampProgram_failure_le_exp gives failure ≤ e^{−c} on satisfiable k-CNFs (k ≥ 1), and ampTime_le gives time ≤ 200 (n+L+1)^2 · 2^{(1−1/k)n} · (c+1).

Not done:

PPSZ on the RAM. PPSZ.implied (w-implication) needs a search over clause subsets of size at most w. The round loop of feat(WordRAM/PPZ): one PPZ round on the randomized word RAM with its exact law #1954 takes any oracle code with a forcedCode_spec-style contract: replace forcedCode and the roundOn (forced φ) law with an impliedCode and roundOn (implied φ w).
Abstract candidate for PPZ next to feat(abstracts): Schöning's 3-SAT algorithm on the randomized word RAM (candidate) #1945, pinning ampProgram_spec, ampProgram_failure_le_exp and ampTime_le, if Samuel selects it.

I'm stopping here; PPSZ on the RAM is available.

feat(WordRAM/Schoening): Schöning's algorithm on the randomized word …

feat(WordRAM/Schoening): multiword trial counter, no word-size assump…

Status: active. worker-claude-e6cf7b0d-ppsz-ram (Claude Code, Opus; subagent of coordinator-claude-e6cf7b0d) claims PPSZ on the randomized word RAM from the handoff, stacked on #1960 (claude/ppz-amplify-894), branch claude/ppsz-wordram-894.

The mathematical layer on main is PPSZ.round φ w = PPZ.roundWith (implied φ w) (#1453), with success bounds from #1466/#1500/#1605. Plan:

impliedCode: decide w-implication on the RAM by a nested odometer search (a choice of w clauses, then a compatible choice of one literal per clause), with an exact contract and an instruction bound in n, L and w.
The PPSZ round with exact law PPSZ.round φ w, by making feat(WordRAM/PPZ): one PPZ round on the randomized word RAM with its exact law #1954's round loop generic in the oracle code.
Amplification if time permits.

awaiting review (worker-claude-e6cf7b0d-ppsz-ram, Claude Code, Opus). Handoff for M2.

#1980, stacked on #1960: PPSZ's oracle on the RAM.

PPSZ.wImplied_iff_test reduces w-implication to a finite search over List.sections: either τ x = some b, or some choice of w clauses (with repetitions) has no compatible choice of one literal per clause under τ[x ↦ !b].
impliedCode_spec runs that search with two nested odometers.
- It needs the clauses in [cBeg, cEnd) below τ at tBase = Tb, s stored at Tb + 2n, and 2s zero words after it.
- It stores optCode (implied φ s τ x) in res and leaves memory unchanged (its scratch is cleared).
- Time: impliedTime s E ≤ 140 (s+1)² (E+1)^(2s), where E is the length of the clause encoding.
Its registers avoid feat(WordRAM/PPZ): one PPZ round on the randomized word RAM with its exact law #1954's RoundFrame, xReg, iReg and jReg, and feat(WordRAM/PPZ): the PPZ algorithm on the randomized word RAM #1960's counter registers 29–31.

Not done: the PPSZ round and its amplification. Plan for the next worker:

Generic round. In PPZ/Round.lean, make roundBody, roundLoop and roundCore take the oracle code oc as a parameter, with this contract: from RoundFrame φ C Tb M y, xReg = v and PartialAt y.mem Tb τ, the run of oc reaches z within T instructions with z.mem = y.mem and z.regs res = optCode (O τ v), and oc preserves the frame registers, xReg, iReg and jReg.
- The proofs carry over with T + 16 (body), d (T + 18) + 2 (loop) and n (T + 25) + 6 (core) in place of 28 E + 15.
- Keep roundBody := roundBodyWith forcedCode and the PPZ theorem statements, so PPZ/Amplify.lean is unaffected.
PPSZ round. Use the input s :: encode φ.
- The setup is feat(WordRAM/PPZ): one PPZ round on the randomized word RAM with its exact law #1954's plus three things: cBeg = 3, n read from mem 2, and s copied to Tb + 2n. The words after it are zero in Data.init.
- Discharge impliedCode_spec's hypotheses from RoundFrame.rest with M the setup memory.
- The law is roundWith (implied φ s) = PPSZ.round φ s by definition.
Amplification. Put the counter after the scratch words (bBase = Tb + 2n + 1 + 2s) and reuse feat(WordRAM/PPZ): the PPZ algorithm on the randomized word RAM #1960's loop.
- The merged success bound is 2^{-(1 - qbar k h) n} (feat(fine-grained): PPSZ critical clause trees and the unique k-SAT bound #1466/feat(fine-grained): PPSZ for every satisfiable k-CNF, k >= 3 #1605).
- The exponent is rational for fixed k, h, so a round count like 2^⌈(1 - qbar k h) n⌉ c needs qbar k h as an input or a fixed constant.

I'm stopping here; the PPSZ round on the RAM is available.

Status: active. worker-claude-e6cf7b0d-ppsz-round (Claude Code, Opus; subagent of coordinator-claude-e6cf7b0d) claims the PPSZ round on the randomized word RAM and its amplification, from the handoff. Branch claude/ppsz-round-894, stacked on #1980 (claude/ppsz-wordram-894).

Make feat(WordRAM/PPZ): one PPZ round on the randomized word RAM with its exact law #1954's round loop generic in the oracle code, keeping the PPZ names and statements.
The PPSZ round on s :: encode φ, whose output law is exactly PPSZ.round φ s.
Amplification.

Round count (the choice I'm making for step 3). The input supplies a rational upper bound a / b on the exponent 1 − qbar k h. On s :: a :: b :: c :: encode φ the program runs R = 2^⌈a n / b⌉ · c rounds. It computes R on the machine as PPZ does; PPZ is the case (a, b) = (k − 1, k). The failure theorem assumes 1 − qbar k h ≤ a / b, ∑_{i<h} (k−1)^i ≤ s and clauses of at most k ≥ 3 literals, and bounds the failure probability by e^{−c}. The time is 2^{(a/b) n} (c + 1) times a polynomial in which the oracle contributes (L + 1)^{2s}. For 3-SAT, (s, a, b) = (3, 39, 70) gives about 1.471^n rounds, via round_success_of_satisfiable_three.

I prefer this to two alternatives:

Reading a precomputed ceiling ⌈(1 − qbar k h) n⌉ from the input would make the input depend on n and leave the algorithm's arithmetic to the caller.
Computing qbar k h on the machine would need the exact rational value of the integral.

feat(PPZ): lazy-order rounds and the forced-value scan on the word RAM (

feat(WordRAM/PPSZ): ε-form of PPSZ's failure bound on the word RAM (#894

awaiting review (worker-claude-e6cf7b0d-ppsz-round, Claude Code, Opus). Handoff for M2: PPSZ now runs on the randomized word RAM with amplification.

#1986, the PPSZ round, stacked on #1980.

The round loop of feat(WordRAM/PPZ): one PPZ round on the randomized word RAM with its exact law #1954 is generic in its oracle code (IsOracleCode, roundCoreWith). PPZ's names and statements are unchanged.
PPSZ.roundProgram_spec covers the input s :: encode φ. One round halts within n (impliedTime s L + 25) + 12 L + 23 instructions, makes at most 2n rand calls, and leaves an assignment whose law is exactly PPSZ.round φ s.

#1990, PPSZ amplified, stacked on #1986.

feat(WordRAM/PPZ): the PPZ algorithm on the randomized word RAM #1960's loop is generalized in place (IsRoundCore, ampLoopWith, repeatRoundWith, countSetup_spec). PPZ's statements are unchanged.
PPSZ.ampProgram_spec covers the input s :: a :: b :: c :: encode φ. The program runs R = 2^⌈an/b⌉ c rounds. It has no false positives, and its output has exactly the law of R independent rounds.
The failure probability is at most e^{−c} when 1 − qbar k h ≤ a/b, k ≥ 3 and s ≥ ∑_{i<h} (k−1)^i (ampProgram_failure_le_exp).
For 3-SAT, (s, a, b) = (3, 39, 70) gives about 1.471^n c rounds (ampProgram_failure_le_exp_three). There is also an ε-form for a/b ≥ 1 − μ_k/(k−1) + ε (ampProgram_failure_le_exp_limit).
ampTime_le: the time is at most 600 (s+1)² (n+L+1)^(2s+1) 2^((a/b) n) (c+1).
The round count is the input bound a/b from my comment above.

Still open on M2:

Integration order. The stack is feat(WordRAM/PPZ): one PPZ round on the randomized word RAM with its exact law #1954 → feat(WordRAM/PPZ): the PPZ algorithm on the randomized word RAM #1960 → feat(WordRAM/PPSZ): w-implication on the randomized word RAM #1980 → feat(WordRAM/PPSZ): one PPSZ round on the randomized word RAM with its exact law #1986 → feat(WordRAM/PPSZ): the PPSZ algorithm on the randomized word RAM #1990. feat(WordRAM/PPSZ): one PPSZ round on the randomized word RAM with its exact law #1986 edits feat(WordRAM/PPZ): one PPZ round on the randomized word RAM with its exact law #1954's PPZ/Round.lean, and feat(WordRAM/PPSZ): the PPSZ algorithm on the randomized word RAM #1990 edits feat(WordRAM/PPZ): the PPZ algorithm on the randomized word RAM #1960's PPZ/Amplify.lean. Queue each one only after its parent has landed and it has merged main.
Abstract candidates for PPZ and PPSZ, if Samuel selects them. They would pin ampProgram_spec, the failure bounds and ampTime_le.
Not formalized: the uniform o(n) form with s growing in n, and computing qbar k h on the machine.

I'm stopping here; these items are available.

feat(WordRAM/PPZ): one PPZ round on the randomized word RAM with its …

feat(WordRAM/PPZ): the PPZ algorithm on the randomized word RAM (csli…

feat(WordRAM/PPSZ): w-implication on the randomized word RAM (cslib-c…

feat(WordRAM/PPSZ): one PPSZ round on the randomized word RAM with it…

feat(WordRAM/PPSZ): the PPSZ algorithm on the randomized word RAM (cs…

triage-claude-e6cf7b0d-6: M2's word-RAM stack has fully landed. #1986 (PPSZ round) and #1990 (PPSZ amplified) merged at 09:08 and 09:26 UTC, after #1954, #1960 and #1980. main now has PPSZ.roundProgram_spec, PPSZ.ampProgram_spec, ampProgram_failure_le_exp (with the _three and _limit forms) and ampTime_le in Algorithms/WordRAM/PPSZ/, beside the PPZ and Schöning counterparts. None of these modules contains a sorry.

So every milestone's Lean is on main. The issue stays open for M2's abstract:

the Schöning candidate feat(abstracts): Schöning's 3-SAT algorithm on the randomized word RAM (candidate) #1945 awaits Samuel's selection;
no PPZ or PPSZ abstract candidate has been opened.

Not formalized, as recorded above: the uniform o(n) form with s growing in n, and computing qbar k h on the machine.

Navigation Menu

Repository navigation

Frontier track: exponential-time SAT algorithms (Schöning, PPSZ) #894

Targets

What's already here

Milestones

Rules for every track

M0 design (M1)

50 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Frontier track: exponential-time SAT algorithms (Schöning, PPSZ) #894

Description

Targets

What's already here

Milestones

Rules for every track

Activity

SamuelSchlesinger commented on Oct 24, 2026

M0 design (M1)

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 25, 2026

SamuelSchlesinger commented on Oct 25, 2026

SamuelSchlesinger commented on Oct 25, 2026

SamuelSchlesinger commented on Oct 25, 2026

SamuelSchlesinger commented on Oct 25, 2026

50 remaining items

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions