Counting sparsification on CNF formulas

List-level operations for the counting sparsification refinement of Appendix A.1 [OAI26c]: tautology removal (removeTautologies), nontautological normalization (countingNormalize), singleton negated-heart unit clauses (negatedHeartUnits), the disjoint counting children (countingChild), and one deterministic counting-sparsification step (countingNext).

Initial preprocessing (countingNormalize φ = normalize (removeTautologies φ)) removes tautologies, deduplicates literals and clauses, and reduces to a subset-minimal antichain. At each branching step on a heavy heart H satisfying deg_c(H) ≥ θ_{c - |H|} (equation (A.1), p. 44, with the unnumbered threshold schedule θ j = M ^ j), the false (A) branch adds H while the true (B) branch adds both the petals petals ψ c H and the singleton negated-heart units negatedHeartUnits H [OpenAI2026ETH, Appendix A.1, equation (A.2), pp. 44–45]. Applying dedupClauses before reduce restores the duplicate-free antichain (CountingNormalized) across steps without re-running tautology removal, while computing the exact clause-set operation ClauseSet.Sparsification.countingChild (toClauseSet_countingChild) and conserving the declared-variable model count (modelCountOn_countingChild).

Main definitions

• Cslib.Logic.PL.CNF.Sparsification.Clause.isTautology, Cslib.Logic.PL.CNF.Sparsification.removeTautologies, Cslib.Logic.PL.CNF.Sparsification.countingNormalize: tautology removal and normalization.
• Cslib.Logic.PL.CNF.Sparsification.negatedHeartUnits, Cslib.Logic.PL.CNF.Sparsification.countingIntro, Cslib.Logic.PL.CNF.Sparsification.countingChild, Cslib.Logic.PL.CNF.Sparsification.countingNext: the list-level counting step.
• Cslib.Logic.PL.CNF.Sparsification.countingThreshold: the counting thresholds θ j = M ^ j.
• Cslib.Logic.PL.CNF.Sparsification.Nontautological, Cslib.Logic.PL.CNF.Sparsification.CountingNormalized: the nontautological normal form.

Main results

• Cslib.Logic.PL.CNF.Sparsification.eval_countingNormalize, Cslib.Logic.PL.CNF.Sparsification.modelCountOn_countingNormalize, Cslib.Logic.PL.CNF.Sparsification.countingNormalized_countingNormalize: nontautological normalization preserves evaluation and declared-variable model counts.
• Cslib.Logic.PL.CNF.Sparsification.toClauseSet_countingChild, Cslib.Logic.PL.CNF.Sparsification.toClauseSet_countingNext: the list-level counting children compute the clause-set counting children.
• Cslib.Logic.PL.CNF.Sparsification.modelCountOn_countingChild, Cslib.Logic.PL.CNF.Sparsification.modelCountOn_countingNext: additive conservation of CNF.modelCountOn across both branches.
• Cslib.Logic.PL.CNF.Sparsification.countingNormalized_countingChild, Cslib.Logic.PL.CNF.Sparsification.countingNormalized_countingNext: the counting step preserves the nontautological normal form.

References

• OpenAI, The Exponential Time Hypothesis is False, Appendix A.1

Tautology removal and counting normalization

def Cslib.Logic.PL.CNF.Sparsification.Clause.isTautology {V : Type u_1} [DecidableEq V] (C : Clause V) : Bool

Whether a clause contains both a literal and its negation.

def Cslib.Logic.PL.CNF.Sparsification.removeTautologies {V : Type u_1} [DecidableEq V] (φ : CNF V) : CNF V

Remove tautological clauses from a CNF formula.

def Cslib.Logic.PL.CNF.Sparsification.countingNormalize {V : Type u_1} [DecidableEq V] (φ : CNF V) : CNF V

Bring a formula into nontautological normal form: remove tautological clauses, deduplicate literals and clauses, and reduce by strict subset containment.

def Cslib.Logic.PL.CNF.Sparsification.negatedHeartUnits {V : Type u_1} (H : Clause V) : CNF V

Singleton clauses [-l] for each literal l of a heart H.

def Cslib.Logic.PL.CNF.Sparsification.countingIntro {V : Type u_1} [DecidableEq V] (ψ : CNF V) (c : ℕ) (H : Clause V) (b : Bool) : CNF V

The clauses introduced by a counting-sparsification branch: the heart (false) or the petals together with the singleton negated-heart units (true).

def Cslib.Logic.PL.CNF.Sparsification.countingChild {V : Type u_1} [DecidableEq V] (ψ : CNF V) (c : ℕ) (H : Clause V) (b : Bool) : CNF V

A counting child of a branching node: append the introduced clauses, deduplicate clauses with identical literal sets, and reduce by strict subset containment.

def Cslib.Logic.PL.CNF.Sparsification.countingNext {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (k : ℕ) (ψ : CNF V) (b : Bool) : CNF V

One deterministic counting-sparsification step using the computed choice choice θ k ψ.

def Cslib.Logic.PL.CNF.Sparsification.countingThreshold (M j : ℕ) : ℕ

The counting-sparsification threshold schedule θ j = M ^ j (defined on p. 44 of [OpenAI2026ETH, Appendix A.1] for 0 ≤ j < k, extended here to a total function on ℕ, and used in the heavy-heart branching inequality deg_c(H) ≥ θ_{c - |H|} of equation (A.1)).

theorem Cslib.Logic.PL.CNF.Sparsification.one_le_countingThreshold {M : ℕ} (hM : 1 ≤ M) (j : ℕ) : 1 ≤ countingThreshold M j

For 1 ≤ M, every counting threshold is positive.

Nontautological normal form

def Cslib.Logic.PL.CNF.Sparsification.Nontautological {V : Type u_1} (ψ : CNF V) : Prop

A CNF formula is nontautological if no clause contains both a literal and its negation.

structure Cslib.Logic.PL.CNF.Sparsification.CountingNormalized {V : Type u_1} [DecidableEq V] (k : ℕ) (ψ : CNF V) extends Cslib.Logic.PL.CNF.Sparsification.Normalized k ψ : Prop

The normal form for list-level counting sparsification at width k: Normalized k ψ together with Nontautological ψ.

• nodup (C : Clause V) : C ∈ ψ → List.Nodup C
• length_le (C : Clause V) : C ∈ ψ → List.length C ≤ k
• nodup_toFinset : (List.map List.toFinset ψ).Nodup
• reduced : ClauseSet.Sparsification.Reduced ψ.toClauseSet
• nontautological : Nontautological ψ

theorem Cslib.Logic.PL.CNF.Sparsification.Clause.isTautology_eq_true_iff {V : Type u_1} [DecidableEq V] {C : Clause V} : isTautology C = true ↔ ∃ l ∈ C, Std.Sat.Literal.negate l ∈ C

theorem Cslib.Logic.PL.CNF.Sparsification.Clause.isTautology_eq_false_iff {V : Type u_1} [DecidableEq V] {C : Clause V} : isTautology C = false ↔ ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C

theorem Cslib.Logic.PL.CNF.Sparsification.eval_eq_true_of_isTautology {V : Type u_1} [DecidableEq V] {C : Clause V} (h : Clause.isTautology C = true) (σ : V → Bool) : Clause.eval σ C = true

Any tautological clause evaluates to true under every assignment.

theorem Cslib.Logic.PL.CNF.Sparsification.removeTautologies_sublist {V : Type u_1} [DecidableEq V] (φ : CNF V) : List.Sublist (removeTautologies φ) φ

removeTautologies φ is a sublist of φ.

@[simp]

theorem Cslib.Logic.PL.CNF.Sparsification.eval_removeTautologies {V : Type u_1} [DecidableEq V] (φ : CNF V) (σ : V → Bool) : eval σ (removeTautologies φ) = eval σ φ

Removing tautological clauses preserves evaluation under every assignment.

@[simp]

theorem Cslib.Logic.PL.CNF.Sparsification.modelCountOn_removeTautologies {V : Type u_1} [DecidableEq V] (φ : CNF V) (declared : Finset V) : (removeTautologies φ).modelCountOn declared = φ.modelCountOn declared

Removing tautological clauses preserves the declared-variable model count.

theorem Cslib.Logic.PL.CNF.Sparsification.nontautological_removeTautologies {V : Type u_1} [DecidableEq V] (φ : CNF V) : Nontautological (removeTautologies φ)

removeTautologies φ is nontautological.

theorem Cslib.Logic.PL.CNF.Sparsification.sat_toClauseSet_countingNormalize_iff {V : Type u_1} [DecidableEq V] (φ : CNF V) (σ : V → Bool) : (countingNormalize φ).toClauseSet.Sat σ ↔ eval σ φ = true

The clause set of countingNormalize φ has the same satisfying assignments as φ.

@[simp]

theorem Cslib.Logic.PL.CNF.Sparsification.eval_countingNormalize {V : Type u_1} [DecidableEq V] (φ : CNF V) (σ : V → Bool) : eval σ (countingNormalize φ) = eval σ φ

countingNormalize φ evaluates identically to φ under every assignment.

@[simp]

theorem Cslib.Logic.PL.CNF.Sparsification.modelCountOn_countingNormalize {V : Type u_1} [DecidableEq V] (φ : CNF V) (declared : Finset V) : (countingNormalize φ).modelCountOn declared = φ.modelCountOn declared

countingNormalize φ preserves the declared-variable model count.

theorem Cslib.Logic.PL.CNF.Sparsification.exists_of_mem_countingNormalize {V : Type u_1} [DecidableEq V] {φ : CNF V} {C : Clause V} (hC : C ∈ countingNormalize φ) : ∃ D ∈ removeTautologies φ, List.toFinset C = List.toFinset D

Every clause of countingNormalize φ has the literals of a nontautological clause of φ.

theorem Cslib.Logic.PL.CNF.Sparsification.length_countingNormalize_le {V : Type u_1} [DecidableEq V] (φ : CNF V) : List.length (countingNormalize φ) ≤ List.length φ

The number of clauses of countingNormalize φ is at most that of φ.

theorem Cslib.Logic.PL.CNF.Sparsification.mem_vars_of_mem_countingNormalize {V : Type u_1} [DecidableEq V] {φ : CNF V} (C : Finset (Literal V)) : C ∈ (countingNormalize φ).toClauseSet → ∀ l ∈ C, l.1 ∈ φ.vars.toFinset

Every variable occurring in countingNormalize φ occurs in φ.

theorem Cslib.Logic.PL.CNF.Sparsification.countingNormalized_countingNormalize {V : Type u_1} [DecidableEq V] {k : ℕ} {φ : CNF V} (hφ : ∀ C ∈ φ, List.length C ≤ k) : CountingNormalized k (countingNormalize φ)

Every formula of width k is brought into nontautological normal form by countingNormalize.

Agreement with clause-set counting operations

theorem Cslib.Logic.PL.CNF.Sparsification.toClauseSet_negatedHeartUnits {V : Type u_1} [DecidableEq V] (H : Clause V) : (negatedHeartUnits H).toClauseSet = ClauseSet.Sparsification.negatedHeartUnits (List.toFinset H)

The clause set of negatedHeartUnits H is ClauseSet.Sparsification.negatedHeartUnits.

theorem Cslib.Logic.PL.CNF.Sparsification.toClauseSet_countingChild {V : Type u_1} [DecidableEq V] {ψ : CNF V} (hnd : ∀ C ∈ ψ, List.Nodup C) (c : ℕ) (H : Clause V) (b : Bool) : (countingChild ψ c H b).toClauseSet = ClauseSet.Sparsification.countingChild ψ.toClauseSet c (List.toFinset H) b

The list-level counting children compute the clause-set counting children.

theorem Cslib.Logic.PL.CNF.Sparsification.toClauseSet_countingNext {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {k : ℕ} {ψ : CNF V} (h : Normalized k ψ) (b : Bool) : (countingNext θ k ψ b).toClauseSet = ClauseSet.Sparsification.countingChild ψ.toClauseSet (choice θ k ψ).1 (List.toFinset (choice θ k ψ).2) b

The clause set of countingNext θ k ψ b equals the clause-set counting child for the computed choice.

theorem Cslib.Logic.PL.CNF.Sparsification.modelCountOn_countingChild {V : Type u_1} [DecidableEq V] {ψ : CNF V} (hnd : ∀ C ∈ ψ, List.Nodup C) (c : ℕ) (H : Clause V) (declared : Finset V) : ψ.modelCountOn declared = (countingChild ψ c H false).modelCountOn declared + (countingChild ψ c H true).modelCountOn declared

Additive model-count conservation for countingChild. On any formula ψ without repeated literals in its clauses, the declared-variable model count equals the sum of the counts of its two counting children.

theorem Cslib.Logic.PL.CNF.Sparsification.modelCountOn_countingNext {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {k : ℕ} {ψ : CNF V} (h : Normalized k ψ) (declared : Finset V) : ψ.modelCountOn declared = (countingNext θ k ψ false).modelCountOn declared + (countingNext θ k ψ true).modelCountOn declared

Additive model-count conservation for countingNext. On any k-normalized formula ψ, one deterministic counting-sparsification step splits the declared-variable model count additively across its false and true branches.

Preservation of normal form under the counting step

theorem Cslib.Logic.PL.CNF.Sparsification.countingNormalized_countingChild {V : Type u_1} [DecidableEq V] {k : ℕ} {ψ : CNF V} (hk : 1 ≤ k) (h : CountingNormalized k ψ) {c : ℕ} {H : Clause V} (hH_nodup : List.Nodup H) (hH_len : List.length H ≤ k) (hH_nontaut : ∀ l ∈ H, Std.Sat.Literal.negate l ∉ H) (b : Bool) : CountingNormalized k (countingChild ψ c H b)

The counting children preserve CountingNormalized k whenever 1 ≤ k and the heart H is a duplicate-free nontautological clause of width at most k.

theorem Cslib.Logic.PL.CNF.Sparsification.countingNormalized_countingNext {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) {k : ℕ} (hk : 1 ≤ k) {ψ : CNF V} (h : CountingNormalized k ψ) (b : Bool) : CountingNormalized k (countingNext θ k ψ b)

One counting-sparsification step preserves CountingNormalized k.

theorem Cslib.Logic.PL.CNF.Sparsification.support_countingChild {V : Type u_1} [DecidableEq V] {ψ : CNF V} {c : ℕ} {H : Clause V} {declared : Finset V} (hψ : ∀ C ∈ ψ, ∀ l ∈ C, l.1 ∈ declared) (hH : ∀ l ∈ H, l.1 ∈ declared) (b : Bool) (C : Clause V) : C ∈ countingChild ψ c H b → ∀ l ∈ C, l.1 ∈ declared

Every literal occurring in countingChild ψ c H b occurs in ψ or has its variable in H.

theorem Cslib.Logic.PL.CNF.Sparsification.support_countingNext {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (k : ℕ) {ψ : CNF V} {declared : Finset V} (hψ : ∀ C ∈ ψ, ∀ l ∈ C, l.1 ∈ declared) (b : Bool) (C : Clause V) : C ∈ countingNext θ k ψ b → ∀ l ∈ C, l.1 ∈ declared

Every literal occurring in countingNext θ k ψ b has its variable in declared whenever ψ does.