Parity tests for CNF formulas

The violation vector of an assignment σ to a formula φ with m clauses is the bit string of length m whose bit e records whether σ falsifies clause e (Cslib.Logic.PL.CNF.violations). It is zero exactly when σ satisfies φ (Cslib.Logic.PL.CNF.violations_eq_zero_iff).

The rows of a matrix over 𝔽₂ with m columns each test the parity of the violations of a set of clauses; every satisfying assignment passes every row. The greedy selection of parity tests (Cslib.BitString.numPassing_greedy) therefore yields [OpenAI2026ETH, Lemma 6.2]: if after the initial rows every passing nonsatisfying assignment violates at least m / P clauses, then 3 n greedily chosen rows, n the number of variables, are passed exactly by the satisfying assignments (Cslib.Logic.PL.CNF.numPassing_greedy). The initial rows are the subject of [OpenAI2026ETH, Lemma 6.1], not proved here.

Main definitions

• Cslib.Logic.PL.CNF.violations: the violation vector of an assignment.

Main results

• Cslib.Logic.PL.CNF.violations_eq_zero_iff: the violation vector is zero exactly on satisfying assignments.
• Cslib.Logic.PL.CNF.numPassing_greedy: after 3 n greedy rounds the rows accept exactly the satisfying assignments.

References

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

def Cslib.Logic.PL.CNF.violations {V : Type u_1} (φ : CNF V) (σ : V → Bool) : Fin (List.length φ) → Bool

The violation vector of the assignment σ: bit e is true when σ falsifies clause e of φ.

theorem Cslib.Logic.PL.CNF.violations_eq_zero_iff {V : Type u_1} (φ : CNF V) (σ : V → Bool) : φ.violations σ = 0 ↔ eval σ φ = true

The violation vector is zero exactly when the assignment satisfies the formula.

theorem Cslib.Logic.PL.CNF.numPassing_greedy {V : Type u_1} [Fintype V] [DecidableEq V] (φ : CNF V) {P : ℕ} (hn : 1 ≤ Fintype.card V) (hP : 1 ≤ P) (A : ℕ → List (Fin (List.length φ) → Bool)) (hinit : ∀ (σ : V → Bool), BitString.PassesTests φ.violations (A 0) σ → eval σ φ = false → List.length φ ≤ P * BitString.weight (φ.violations σ)) (γ : ℕ → Fin P → Fin (List.length φ) × Bool) (hA : ∀ (i : ℕ), A (i + 1) = A i ++ [BitString.testRow (γ i)]) (hγ : ∀ (i : ℕ) (γ' : Fin P → 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

Greedy parity tests for a CNF formula [OpenAI2026ETH, Lemma 6.2]. Suppose that after the initial rows A 0 every passing nonsatisfying assignment violates at least m / P of the m clauses of φ, and that φ has n ≥ 1 variables. Append rows A (i + 1) = A i ++ [testRow (γ i)], where each list γ i minimizes the number of passing assignments among all lists of length P. After 3 n rounds, the passing assignments are exactly the satisfying ones.