Exact parity tests for sparse CNF formulas

Combining the initial parity tests of [OpenAI2026ETH, Lemma 6.1] (Cslib.BitString.exists_initialTests) with the greedy selection of [OpenAI2026ETH, Lemma 6.2] (Cslib.Logic.PL.CNF.numPassing_greedy): for a formula on n ≥ 1 variables with m ≤ B n clauses, there are at most 3 n initial parity tests on the clause-violation bits, each reading at most D₀ = 320000 B² μ³ of them, such that every passing nonsatisfying assignment violates at least m / P clauses, P = 20000 B² μ², μ = ⌊log₂ m⌋ + 1 (Cslib.Logic.PL.CNF.exists_initialTests). After them, 3 n greedily chosen tests of list length P are passed exactly by the satisfying assignments (Cslib.Logic.PL.CNF.numPassing_greedy_initial). Both statements are about existence and counts; computing the tests is not treated here.

Main results

• Cslib.Logic.PL.CNF.exists_initialTests: initial tests for a formula.
• Cslib.Logic.PL.CNF.numPassing_greedy_initial: the greedy tests after them are exact.

References

• OpenAI, The Exponential Time Hypothesis is False, §§6.1–6.2

theorem Cslib.Logic.PL.CNF.exists_initialTests {V : Type u_1} [Fintype V] (φ : CNF V) {B : ℕ} (hn : 1 ≤ Fintype.card V) (hB : 1 ≤ B) (hm : List.length φ ≤ B * Fintype.card V) : ∃ (A₀ : List (Fin (List.length φ) → Bool)), A₀.length ≤ 3 * Fintype.card V ∧ (∀ r ∈ A₀, BitString.weight r ≤ 320000 * B ^ 2 * (Nat.log 2 (List.length φ) + 1) ^ 3) ∧ ∀ (σ : V → Bool), BitString.PassesTests φ.violations A₀ σ → eval σ φ = false → List.length φ ≤ 20000 * B ^ 2 * (Nat.log 2 (List.length φ) + 1) ^ 2 * BitString.weight (φ.violations σ)

Initial parity tests for a formula [OpenAI2026ETH, Lemma 6.1]: for a formula on n ≥ 1 variables with m ≤ B n clauses, B ≥ 1, there are at most 3 n rows on the m violation bits, each with at most 320000 B² μ³ ones, such that every passing nonsatisfying assignment violates at least m / (20000 B² μ²) clauses, where μ = ⌊log₂ m⌋ + 1.

theorem Cslib.Logic.PL.CNF.numPassing_greedy_initial {V : Type u_1} [Fintype V] [DecidableEq V] (φ : CNF V) {B : ℕ} (hn : 1 ≤ Fintype.card V) (hB : 1 ≤ B) (hm : List.length φ ≤ B * Fintype.card V) : ∃ (A₀ : List (Fin (List.length φ) → Bool)), A₀.length ≤ 3 * Fintype.card V ∧ (∀ r ∈ A₀, BitString.weight r ≤ 320000 * B ^ 2 * (Nat.log 2 (List.length φ) + 1) ^ 3) ∧ ∀ (A : ℕ → List (Fin (List.length φ) → Bool)) (γ : ℕ → Fin (20000 * B ^ 2 * (Nat.log 2 (List.length φ) + 1) ^ 2) → Fin (List.length φ) × Bool), A 0 = A₀ → (∀ (i : ℕ), A (i + 1) = A i ++ [BitString.testRow (γ i)]) → (∀ (i : ℕ) (γ' : Fin (20000 * B ^ 2 * (Nat.log 2 (List.length φ) + 1) ^ 2) → Fin (List.length φ) × Bool), BitString.numPassing φ.violations (A i ++ [BitString.testRow (γ i)]) ≤ BitString.numPassing φ.violations (A i ++ [BitString.testRow γ'])) → BitString.numPassing φ.violations (A (3 * Fintype.card V)) = {σ : V → Bool | eval σ φ = true}.card

Exact parity tests for a formula [OpenAI2026ETH, Lemmas 6.1–6.2]: for a formula on n ≥ 1 variables with m ≤ B n clauses, B ≥ 1, there are initial rows as in CNF.exists_initialTests such that, after appending 3 n rows testRow (γ i) of list length P = 20000 B² μ², each minimizing the number of passing assignments, the passing assignments are exactly the satisfying ones.