diff --git a/Complexity.lean b/Complexity.lean index d43d4cf12..64ee60b84 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -762,6 +762,7 @@ public import Complexity.Computability.Complexity.Fagin.Verifier public import Complexity.Computability.Complexity.FineGrained public import Complexity.Computability.Complexity.FineGrained.Assignment public import Complexity.Computability.Complexity.FineGrained.BruteForce +public import Complexity.Computability.Complexity.FineGrained.CountingEndpoint public import Complexity.Computability.Complexity.FineGrained.CountingScale public import Complexity.Computability.Complexity.FineGrained.ExhaustiveSearch public import Complexity.Computability.Complexity.FineGrained.Exponents @@ -2191,6 +2192,7 @@ public import Complexity.Logics.Propositional.CNF.ImplicationChain public import Complexity.Logics.Propositional.CNF.ImplicationCycle public import Complexity.Logics.Propositional.CNF.ModelCount public import Complexity.Logics.Propositional.CNF.ModelCount.Declared +public import Complexity.Logics.Propositional.CNF.ModelCount.DenseRelabel public import Complexity.Logics.Propositional.CNF.ModelCount.Relabel public import Complexity.Logics.Propositional.CNF.Occurrence public import Complexity.Logics.Propositional.CNF.Parity @@ -2217,8 +2219,10 @@ public import Complexity.Logics.Propositional.ClauseSet.Sparsification.Bounds public import Complexity.Logics.Propositional.ClauseSet.Sparsification.Counting public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingDeletion public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingInsertions +public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingList public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingOccurrences public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParameters +public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingPolyTime public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingSurvival public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingTree public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingUnits diff --git a/Complexity/Computability/Complexity/FineGrained/CountingEndpoint.lean b/Complexity/Computability/Complexity/FineGrained/CountingEndpoint.lean new file mode 100644 index 000000000..9fa0c3073 --- /dev/null +++ b/Complexity/Computability/Complexity/FineGrained/CountingEndpoint.lean @@ -0,0 +1,300 @@ +/- +Copyright (c) 2026 OpenAI, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: OpenAI, Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.FineGrained.CountingScale +public import Complexity.Computability.Complexity.FineGrained.Reduction +public import Complexity.Logics.Propositional.CNF.ModelCount.DenseRelabel +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary + +/-! +# From sublinear interpolation-scale counting to `satExponent k = 0`, `¬ETH`, and `¬SETH` + +Bridges the sublinear exponent `Cslib.Complexity.SubexponentialSAT.interpolationScale` of +Section 6.4, Proposition 6.4 (pp. 43–44) [OpenAI2026ETH] and dense variable relabeling +(`Cslib.Logic.PL.CNF.denseRelabel`) to the fine-grained satisfiability endpoints +(`DecidableInSubexpTime (KSAT k) encCNF CNF.numVars`, `satExponent k = 0`, `¬ETH`, and `¬SETH`). + +### Source relation and library adaptations + +* **Proposition 6.4 (§6.4, pp. 43–44) vs. Theorem 1.1:** Proposition 6.4 states that for every fixed + integer $k \ge 2$, there is a deterministic algorithm that, given a $k$-CNF formula $F$ on + $n \ge 20$ variables with $m$ clauses, outputs the exact number of satisfying assignments of $F$ + in $\{0, 1\}^n$ in time $(n + m)^{O_k(1)} \cdot 2^{O_k(\rho(n))}$, where + $\rho(n) = n (\log\log n)^2 / \sqrt{\log n}$ (formalized for all $n \in \mathbb{N}$ with the + $+16$ domain shift as `interpolationScale n`), whereas Theorem 1.1 states the sharper + single-$\log\log$ headline bound. This module uses Proposition 6.4's `interpolationScale`, which + is already $o(n)$ (`isLittleO_interpolationScale`). +* **Library adaptations:** First-occurrence dense variable numbering + (`CNF.denseRelabel φ = φ.relabel φ.distinctVars.idxOf`, mapping occurring variables onto + `Finset.range φ.numVars` while preserving `φ.modelCount` as + `φ.denseRelabel.modelCountOn (Finset.range φ.numVars)`) and the conditional complexity-class + reduction wrappers below are library adaptations connecting a dense-variable model counter to + `Cslib.Complexity`'s existing `KSAT`, `DecidableInSubexpTime`, `satExponent`, `ETH`, and `SETH` + definitions. This module assumes such a dense counter as a hypothesis and does not construct it. + +Specifically: +1. Any problem decidable in time `O(2 ^ (A₀ * interpolationScale (μ a)) * (|enc a| + 1) ^ d)` is + `DecidableInSubexpTime` with respect to `μ` (`DecidableInSubexpTime.of_interpolationScale`, + `DecidableInSubexpTime.of_computableInO_interpolationScale`). +2. Any model-counting routine `count : CNF ℕ → ℕ` that computes + `ψ.modelCountOn (Finset.range ψ.numVars)` on dense width-`≤ k` formulas (`ψ.vars.toFinset = + Finset.range ψ.numVars`) within time `O(2 ^ (A₀ * interpolationScale ψ.numVars) * (|ψ| + 1) ^ e)` + yields `DecidableInSubexpTime (KSAT k) encCNF CNF.numVars` via polynomial-time dense relabeling + and clause-width checking (`DecidableInSubexpTime.KSAT_of_dense_modelCount_interpolationScale`). +3. Subexponential-time decidability of `KSAT k` is equivalent to `satExponent k = 0` + (`satExponent_eq_zero_iff_decidableInSubexpTime`), refutes `ETH` at `k = 3` + (`not_ETH_of_decidableInSubexpTime`), and refutes `SETH` when established for all `k` + (`not_SETH_of_forall_decidableInSubexpTime`). + +## Main results + +* `Cslib.Logic.PL.CNF.denseRelabel_mem_KSAT_iff`: dense relabeling preserves `KSAT k`. +* `Cslib.Complexity.DecidableInSubexpTime.of_interpolationScale`, + `Cslib.Complexity.DecidableInSubexpTime.of_computableInO_interpolationScale`: subexponential + time from `interpolationScale` runtime bounds. +* `Cslib.Complexity.DecidableInSubexpTime.KSAT_of_dense_modelCount_interpolationScale`: + `DecidableInSubexpTime (KSAT k)` from a dense-variable model counter at `interpolationScale`. +* `Cslib.Complexity.satExponent_eq_zero_of_decidableInSubexpTime`, + `Cslib.Complexity.satExponent_eq_zero_iff_decidableInSubexpTime`: `satExponent k = 0`. +* `Cslib.Complexity.not_ETH_of_decidableInSubexpTime`, + `Cslib.Complexity.not_SETH_of_forall_decidableInSubexpTime`: refutation of `ETH` and `SETH`. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Section 6.4, + Proposition 6.4, pp. 43–44. +* [R. Impagliazzo, R. Paturi, *On the complexity of k-SAT*][ImpagliazzoPaturi2001] +-/ + +@[expose] public section + +namespace Cslib.Logic.PL.CNF + +open Cslib.Complexity + +/-- Dense variable relabeling preserves membership in `KSAT k` for every `k` (including `k = 0, 1`, +empty formulas, and formulas with repeated literals or gaps in variable numbering). -/ +@[simp] +theorem denseRelabel_mem_KSAT_iff {k : ℕ} {φ : CNF ℕ} : + φ.denseRelabel ∈ KSAT k ↔ φ ∈ KSAT k := by + simp only [KSAT, Set.mem_ofPred_eq, all_length_le_denseRelabel, satisfiable_denseRelabel] + +end Cslib.Logic.PL.CNF + +namespace Cslib.Complexity + +open Cslib.Logic.PL Turing.MultiTapeTM SubexponentialSAT + +/-! ### From `interpolationScale` bounds to `DecidableInSubexpTime` -/ + +/-- Any problem decidable in time `O(2 ^ (A₀ * interpolationScale (μ a)) * (|enc a| + 1) ^ d)` is +decidable in subexponential time in `μ`. -/ +theorem DecidableInSubexpTime.of_interpolationScale {α : Type} {enc : α ↪ List Bool} + {A : Set α} {μ : α → ℕ} {A₀ : ℝ} {d : ℕ} + (h : DecidableInTimeO A enc (fun a => + (2 : ℝ) ^ (A₀ * interpolationScale (μ a)) * (((enc a).length : ℝ) + 1) ^ d)) : + DecidableInSubexpTime A enc μ := by + intro δ hδ + obtain ⟨K, _, hK⟩ := exists_two_pow_mul_interpolationScale_le A₀ hδ + refine ⟨d, h.mono ⌈K⌉₊ (fun a => ?_) fun a => by positivity⟩ + have hceil : K ≤ ⌈K⌉₊ := Nat.le_ceil K + have h1 : (2 : ℝ) ^ (A₀ * interpolationScale (μ a)) ≤ ⌈K⌉₊ * (2 : ℝ) ^ (δ * μ a) := + (hK (μ a)).trans (mul_le_mul_of_nonneg_right hceil (by positivity)) + have h2 := mul_le_mul_of_nonneg_right h1 + (by positivity : (0 : ℝ) ≤ (((enc a).length : ℝ) + 1) ^ d) + linarith + +/-- If `f : α → Bool` decides `A` in `ComputableInO` time bounded by +`c * (2 ^ (A₀ * interpolationScale (μ a)) * (|enc a| + 1) ^ e) + c`, then `A` is decidable in +subexponential time in `μ`. -/ +theorem DecidableInSubexpTime.of_computableInO_interpolationScale {α : Type} {enc : α ↪ List Bool} + {A : Set α} {μ : α → ℕ} {f : α → Bool} {t : α → ℕ} + (hf : ComputableInO f enc encBool t t) (hfA : ∀ a, a ∈ A ↔ f a = true) + {A₀ : ℝ} {c e : ℕ} + (ht : ∀ a, (t a : ℝ) ≤ + c * ((2 : ℝ) ^ (A₀ * interpolationScale (μ a)) * (((enc a).length : ℝ) + 1) ^ e) + c) : + DecidableInSubexpTime A enc μ := by + intro δ hδ + obtain ⟨K, _, hK⟩ := exists_two_pow_mul_interpolationScale_le A₀ hδ + refine DecidableInExpTime.of_computableInO hf hfA (c * ⌈K⌉₊ + c) e fun a => ?_ + refine (ht a).trans ?_ + have hceil : K ≤ ⌈K⌉₊ := Nat.le_ceil K + have hX1 : (1 : ℝ) ≤ (2 : ℝ) ^ (δ * μ a) := Real.one_le_rpow (by norm_num) (by positivity) + have hP1 : (1 : ℝ) ≤ (((enc a).length : ℝ) + 1) ^ e := + one_le_pow₀ (by linarith [(Nat.cast_nonneg (enc a).length : (0 : ℝ) ≤ _)]) + have hXP1 : (1 : ℝ) ≤ (2 : ℝ) ^ (δ * μ a) * (((enc a).length : ℝ) + 1) ^ e := + one_le_mul_of_one_le_of_one_le hX1 hP1 + have hcXP : (c : ℝ) ≤ (c : ℝ) * ((2 : ℝ) ^ (δ * μ a) * (((enc a).length : ℝ) + 1) ^ e) := + le_mul_of_one_le_right (Nat.cast_nonneg c) hXP1 + have h1 : (2 : ℝ) ^ (A₀ * interpolationScale (μ a)) ≤ ⌈K⌉₊ * (2 : ℝ) ^ (δ * μ a) := + (hK (μ a)).trans (mul_le_mul_of_nonneg_right hceil (by positivity)) + have h2 := mul_le_mul_of_nonneg_right h1 + (by positivity : (0 : ℝ) ≤ (((enc a).length : ℝ) + 1) ^ e) + rw [mul_assoc] at h2 + have h3 := mul_le_mul_of_nonneg_left h2 (Nat.cast_nonneg c) + push_cast + linarith + +/-! ### From dense-variable model counting to `DecidableInSubexpTime (KSAT k)` -/ + +open ComputableTidilyInPolyTime in +private theorem computableInPolyTime_pos_nat : + ComputableInPolyTime (fun n : ℕ => decide (0 < n)) encNat encBool := by + have heq : (fun n : ℕ => decide (0 < n)) = fun n => !(n == 0) := by + funext n + cases n <;> rfl + rw [heq] + refine .of_tidy ?_ + fun_prop + +/-- **From dense-variable model counting at `interpolationScale` to subexponential `k`-SAT.** +Suppose `count : CNF ℕ → ℕ` runs in time +`O(2 ^ (A₀ * interpolationScale ψ.numVars) * (|encCNF ψ| + 1) ^ e)` and computes the +declared-variable model count `ψ.modelCountOn (Finset.range ψ.numVars)` on every width-`≤ k` +formula `ψ` whose occurring variables are `Finset.range ψ.numVars`. Then `KSAT k` is decidable in +subexponential time in the number of occurring variables (`CNF.numVars`). -/ +theorem DecidableInSubexpTime.KSAT_of_dense_modelCount_interpolationScale {k : ℕ} + {count : CNF ℕ → ℕ} {t : CNF ℕ → ℕ} + (hcount : ComputableInO count encCNF encNat t t) + (hspec : ∀ ψ : CNF ℕ, (∀ c ∈ ψ, c.length ≤ k) → + ψ.vars.toFinset = Finset.range ψ.numVars → + count ψ = ψ.modelCountOn (Finset.range ψ.numVars)) + {A₀ : ℝ} {c e : ℕ} + (ht : ∀ ψ : CNF ℕ, (t ψ : ℝ) ≤ + c * ((2 : ℝ) ^ (A₀ * interpolationScale ψ.numVars) * (((encCNF ψ).length : ℝ) + 1) ^ e) + c) : + DecidableInSubexpTime (KSAT k) encCNF CNF.numVars := by + have hcount_tidy := hcount.tidy + obtain ⟨dpos, _, hpos⟩ := computableInPolyTime_pos_nat.tidy.exists_degree + have hposO := hpos.inO + obtain ⟨l, hl⟩ := hcount_tidy.length_le_time + have hcomp : ComputableInO (fun ψ : CNF ℕ => decide (0 < count ψ)) encCNF encBool _ _ := + .of_tidy (hposO.comp hcount_tidy) + let B : Set (CNF ℕ) := {ψ | decide (0 < count ψ) = true} + have hB_subexp : DecidableInSubexpTime B encCNF CNF.numVars := by + set A₁ : ℝ := max A₀ 0 * (dpos + 1) + set E : ℕ := e * (dpos + 1) + set C₀ : ℕ := (2 * c + 1) + (2 * l + 1) ^ dpos * (2 * c + 2) ^ dpos + refine DecidableInSubexpTime.of_computableInO_interpolationScale hcomp (fun _ => Iff.rfl) + (A₀ := A₁) (c := C₀) (e := E) fun ψ => ?_ + set L : ℝ := ((encCNF ψ).length : ℝ) + set X₀ : ℝ := (2 : ℝ) ^ (max A₀ 0 * interpolationScale ψ.numVars) + set P₀ : ℝ := (L + 1) ^ e + have hX₀1 : 1 ≤ X₀ := Real.one_le_rpow (by norm_num) + (mul_nonneg (le_max_right _ _) (interpolationScale_nonneg _)) + have hP₀1 : 1 ≤ P₀ := + one_le_pow₀ (by linarith [(Nat.cast_nonneg (encCNF ψ).length : (0 : ℝ) ≤ L)]) + have hXP1 : 1 ≤ X₀ * P₀ := one_le_mul_of_one_le_of_one_le hX₀1 hP₀1 + have hX_mono : (2 : ℝ) ^ (A₀ * interpolationScale ψ.numVars) ≤ X₀ := + Real.rpow_le_rpow_of_exponent_le (by norm_num) + (mul_le_mul_of_nonneg_right (le_max_left _ _) (interpolationScale_nonneg _)) + have ht_le : (t ψ : ℝ) ≤ (2 * c + 1) * (X₀ * P₀) := by + have h1 := ht ψ + have h2 : (2 : ℝ) ^ (A₀ * interpolationScale ψ.numVars) * P₀ ≤ X₀ * P₀ := + mul_le_mul_of_nonneg_right hX_mono (by positivity) + have h3 := mul_le_mul_of_nonneg_left h2 (Nat.cast_nonneg c) + have h4 : (c : ℝ) ≤ c * (X₀ * P₀) := le_mul_of_one_le_right (Nat.cast_nonneg c) hXP1 + linarith + have hlen_le : ((encNat (count ψ)).length : ℝ) + 1 ≤ + (2 * l + 1) * (2 * c + 2) * (X₀ * P₀) := by + have h1 : ((encNat (count ψ)).length : ℝ) ≤ l * ((t ψ : ℝ) + 1) := by + exact_mod_cast hl ψ + have h2 : (t ψ : ℝ) + 1 ≤ (2 * c + 2) * (X₀ * P₀) := by linarith + have h3 := mul_le_mul_of_nonneg_left h2 (Nat.cast_nonneg l) + nlinarith + have hpow_le : (((encNat (count ψ)).length : ℝ) + 1) ^ dpos ≤ + ((2 * l + 1) ^ dpos * (2 * c + 2) ^ dpos) * (X₀ * P₀) ^ dpos := by + calc (((encNat (count ψ)).length : ℝ) + 1) ^ dpos + ≤ ((2 * l + 1) * (2 * c + 2) * (X₀ * P₀)) ^ dpos := + pow_le_pow_left₀ (by positivity) hlen_le dpos + _ = ((2 * l + 1) ^ dpos * (2 * c + 2) ^ dpos) * (X₀ * P₀) ^ dpos := by + rw [mul_pow, mul_pow] + have hXP_dpos : (X₀ * P₀) ^ dpos ≤ (X₀ * P₀) ^ (dpos + 1) := + pow_le_pow_right₀ hXP1 (Nat.le_succ dpos) + have hXP_one : X₀ * P₀ ≤ (X₀ * P₀) ^ (dpos + 1) := + le_self_pow₀ hXP1 (Nat.succ_ne_zero dpos) + have hXP_Rewrite : (X₀ * P₀) ^ (dpos + 1) = + (2 : ℝ) ^ (A₁ * interpolationScale ψ.numVars) * (L + 1) ^ E := by + rw [mul_pow] + congr 1 + · simp only [X₀, A₁, ← Real.rpow_natCast] + rw [← Real.rpow_mul (by norm_num)] + congr 1 + push_cast + ring + · simp only [P₀, E, ← pow_mul] + have htot : (t ψ : ℝ) + (((encNat (count ψ)).length : ℝ) + 1) ^ dpos ≤ + C₀ * ((X₀ * P₀) ^ (dpos + 1)) := by + have ht_le' : (t ψ : ℝ) ≤ (c + 1 + c) * (X₀ * P₀) ^ (dpos + 1) := by + have := mul_le_mul_of_nonneg_left hXP_one (by positivity : (0 : ℝ) ≤ 2 * c + 1) + linarith + have hpow_le' : (((encNat (count ψ)).length : ℝ) + 1) ^ dpos ≤ + ((2 * l + 1) ^ dpos * (2 * c + 2) ^ dpos) * (X₀ * P₀) ^ (dpos + 1) := by + refine hpow_le.trans (mul_le_mul_of_nonneg_left hXP_dpos (by positivity)) + simp only [C₀] + push_cast + linarith + push_cast at htot ⊢ + rw [← hXP_Rewrite] + have hC₀ : (0 : ℝ) ≤ C₀ := Nat.cast_nonneg C₀ + linarith + have hB'_subexp : DecidableInSubexpTime {φ : CNF ℕ | φ.denseRelabel ∈ B} encCNF CNF.numVars := + hB_subexp.of_reduction SAT.computableInPolyTime_denseRelabel (fun _ => Iff.rfl) (c := 1) + fun φ => by rw [CNF.numVars_denseRelabel]; omega + intro δ hδ + have hKSAT_eq : KSAT k = {φ : CNF ℕ | (φ.all fun c => decide (c.length ≤ k)) = true} ∩ + {φ : CNF ℕ | φ.denseRelabel ∈ B} := by + ext φ + simp only [KSAT, B, Set.mem_inter_iff, Set.mem_ofPred_eq, List.all_eq_true, decide_eq_true_eq] + refine and_congr_right fun hφ => ?_ + have hvars : φ.denseRelabel.vars.toFinset = Finset.range φ.denseRelabel.numVars := by + rw [CNF.numVars_denseRelabel, CNF.vars_denseRelabel_toFinset] + rw [hspec φ.denseRelabel ((CNF.all_length_le_denseRelabel φ).mpr hφ) hvars, + CNF.numVars_denseRelabel, CNF.modelCountOn_denseRelabel, CNF.modelCount_pos_iff] + rw [hKSAT_eq] + exact (hB'_subexp δ hδ).inter (computableInPolyTime_all_length_le k) hδ.le + +/-! ### Exponent and ETH/SETH consequences -/ + +/-- If `KSAT k` is decidable in subexponential time in the number of variables, then +`satExponent k = 0`. -/ +theorem satExponent_eq_zero_of_decidableInSubexpTime {k : ℕ} + (h : DecidableInSubexpTime (KSAT k) encCNF CNF.numVars) : + satExponent k = 0 := by + refine le_antisymm (le_of_not_gt fun hpos => ?_) (satExponent_nonneg k) + exact not_decidableInExpTime_of_lt_satExponent (half_pos hpos).le (half_lt_self hpos) + (h (satExponent k / 2) (half_pos hpos)) + +/-- `satExponent k = 0` if and only if `KSAT k` is decidable in subexponential time in the number +of variables. -/ +theorem satExponent_eq_zero_iff_decidableInSubexpTime {k : ℕ} : + satExponent k = 0 ↔ DecidableInSubexpTime (KSAT k) encCNF CNF.numVars := by + refine ⟨fun h δ hδ => ?_, satExponent_eq_zero_of_decidableInSubexpTime⟩ + by_contra hndec + have hle := le_satExponent_of_not_decidableInExpTime hndec + linarith + +/-- Subexponential-time decidability of 3-SAT refutes the Exponential Time Hypothesis (`¬ETH`). -/ +theorem not_ETH_of_decidableInSubexpTime + (h : DecidableInSubexpTime (KSAT 3) encCNF CNF.numVars) : ¬ETH := by + rw [ETH_iff_satExponent_pos, satExponent_eq_zero_of_decidableInSubexpTime h] + exact lt_irrefl 0 + +/-- Subexponential-time decidability of `k`-SAT for all `k` refutes the Strong Exponential Time +Hypothesis (`¬SETH`). -/ +theorem not_SETH_of_forall_decidableInSubexpTime + (h : ∀ k, DecidableInSubexpTime (KSAT k) encCNF CNF.numVars) : ¬SETH := by + rintro hSETH + obtain ⟨k, hk⟩ := hSETH (1 / 2) (by norm_num) + have h12 : (1 : ℝ) - 1 / 2 = 1 / 2 := by norm_num + rw [h12] at hk + exact hk (h k (1 / 2) (by norm_num)) + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/FineGrained/CountingScale.lean b/Complexity/Computability/Complexity/FineGrained/CountingScale.lean index fd4d1d6fa..606596edb 100644 --- a/Complexity/Computability/Complexity/FineGrained/CountingScale.lean +++ b/Complexity/Computability/Complexity/FineGrained/CountingScale.lean @@ -79,4 +79,33 @@ theorem eventually_mul_interpolationScale_le (A : ℝ) {ε : ℝ} (hε : 0 < ε) have h := mul_le_mul_of_nonneg_right hn.le (Nat.cast_nonneg n : (0 : ℝ) ≤ n) simpa only [interpolationScale, mul_div_assoc, mul_assoc, mul_left_comm, mul_comm] using h +/-- The interpolation scale is nonnegative at every natural input. -/ +theorem interpolationScale_nonneg (n : ℕ) : 0 ≤ interpolationScale n := by + unfold interpolationScale + positivity + +/-- For any multiplier `A` and any `ε > 0`, `2 ^ (A * interpolationScale n)` is globally bounded +by a constant multiple of `2 ^ (ε * n)`. -/ +theorem exists_two_pow_mul_interpolationScale_le (A : ℝ) {ε : ℝ} (hε : 0 < ε) : + ∃ K : ℝ, 1 ≤ K ∧ ∀ n : ℕ, (2 : ℝ) ^ (A * interpolationScale n) ≤ K * (2 : ℝ) ^ (ε * n) := by + obtain ⟨N₀, hN₀⟩ := eventually_atTop.mp (eventually_mul_interpolationScale_le A hε) + let K : ℝ := 1 + ∑ m ∈ Finset.range N₀, (2 : ℝ) ^ (A * interpolationScale m) + have hsum_nonneg : 0 ≤ ∑ m ∈ Finset.range N₀, (2 : ℝ) ^ (A * interpolationScale m) := + Finset.sum_nonneg fun m _ => by positivity + have hK1 : 1 ≤ K := by dsimp [K]; linarith + refine ⟨K, hK1, fun n => ?_⟩ + have h2ε : (1 : ℝ) ≤ (2 : ℝ) ^ (ε * n) := Real.one_le_rpow (by norm_num) (by positivity) + by_cases hn : n < N₀ + · have hmem : n ∈ Finset.range N₀ := Finset.mem_range.mpr hn + have hle_sum : (2 : ℝ) ^ (A * interpolationScale n) ≤ + ∑ m ∈ Finset.range N₀, (2 : ℝ) ^ (A * interpolationScale m) := + Finset.single_le_sum (f := fun m => (2 : ℝ) ^ (A * interpolationScale m)) + (fun m _ => by positivity) hmem + have hle_K : (2 : ℝ) ^ (A * interpolationScale n) ≤ K := by dsimp [K]; linarith + exact hle_K.trans (le_mul_of_one_le_right (by positivity) h2ε) + · have hle : A * interpolationScale n ≤ ε * n := hN₀ n (not_lt.mp hn) + have hrpow : (2 : ℝ) ^ (A * interpolationScale n) ≤ (2 : ℝ) ^ (ε * n) := + Real.rpow_le_rpow_of_exponent_le (by norm_num) hle + exact hrpow.trans (le_mul_of_one_le_left (by positivity) hK1) + end Cslib.Complexity.SubexponentialSAT diff --git a/Complexity/Logics/Propositional/CNF/ModelCount/DenseRelabel.lean b/Complexity/Logics/Propositional/CNF/ModelCount/DenseRelabel.lean new file mode 100644 index 000000000..b16783da0 --- /dev/null +++ b/Complexity/Logics/Propositional/CNF/ModelCount/DenseRelabel.lean @@ -0,0 +1,205 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Logics.Propositional.CNF.ModelCount.Declared +public import Complexity.Logics.Propositional.CNF.Compact.Relabel +public import Complexity.Computability.Complexity.Problems.SAT.PolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain + +/-! +# Dense variable numbering for CNF formulas + +`CNF.denseRelabel φ` renames each variable of a CNF formula `φ` by its index in `φ.distinctVars`. +Unlike `CNF.compact` (which uses first positions in `φ.vars` and can leave gaps when variables +repeat), `CNF.denseRelabel φ` maps the occurring variables bijectively onto `0, …, φ.numVars - 1` +in order of first occurrence (a library adaptation to the declared-variable model of +[OpenAI2026ETH]). + +The renaming preserves clause lengths, clause count, `numVars`, `Satisfiable`, `modelCount`, and +gives `φ.denseRelabel.modelCountOn (Finset.range φ.numVars) = φ.modelCount`. It is computable in +polynomial time for any variable encoding, both into unary variable indices and into binary +natural-number indices (`encCNF`). + +## Main definitions + +* `Cslib.Logic.PL.CNF.denseRelabel`: rename variables by their positions in `distinctVars`. + +## Main results + +* `Cslib.Logic.PL.CNF.vars_denseRelabel_toFinset`, + `Cslib.Logic.PL.CNF.numVars_denseRelabel`, + `Cslib.Logic.PL.CNF.distinctVars_denseRelabel`: the occurring variables of `φ.denseRelabel` are + `0, …, φ.numVars - 1` in order. +* `Cslib.Logic.PL.CNF.satisfiable_denseRelabel`, + `Cslib.Logic.PL.CNF.modelCount_denseRelabel`, + `Cslib.Logic.PL.CNF.modelCountOn_denseRelabel`: satisfiability and model counts are preserved. +* `Cslib.Logic.PL.CNF.computableInPolyTime_denseRelabel_unary`, + `Cslib.Logic.PL.CNF.computableInPolyTime_denseRelabel`, + `Cslib.Complexity.SAT.computableInPolyTime_denseRelabel`: dense relabeling is computable in + polynomial time. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH] +-/ + +@[expose] public section + +namespace Cslib.Logic.PL.CNF + +open Turing.MultiTapeTM ComputableTidilyInPolyTime + +variable {V : Type*} [DecidableEq V] + +/-- Rename each variable of `φ` by its index in `φ.distinctVars`, producing dense variable indices +`0, …, φ.numVars - 1`. -/ +def denseRelabel (φ : CNF V) : CNF ℕ := + φ.relabel φ.distinctVars.idxOf + +/-- Dense relabeling preserves all clause lengths in order. -/ +@[simp] +theorem map_length_denseRelabel (φ : CNF V) : + φ.denseRelabel.map List.length = φ.map List.length := by + simp [denseRelabel, CNF.relabel, Clause.relabel, List.map_map, Function.comp_def] + +/-- Dense relabeling preserves the number of clauses. -/ +@[simp] +theorem length_denseRelabel (φ : CNF V) : + φ.denseRelabel.length = φ.length := by + simp [denseRelabel, CNF.relabel] + +/-- Dense relabeling preserves any uniform upper bound on clause lengths. -/ +theorem all_length_le_denseRelabel {k : ℕ} (φ : CNF V) : + (∀ c ∈ φ.denseRelabel, c.length ≤ k) ↔ ∀ c ∈ φ, c.length ≤ k := by + simp [denseRelabel, CNF.relabel] + +/-- The occurring variables of `φ.denseRelabel` are `Finset.range φ.numVars`. -/ +@[simp] +theorem vars_denseRelabel_toFinset (φ : CNF V) : + φ.denseRelabel.vars.toFinset = Finset.range φ.numVars := + vars_dense_relabel φ + +/-- Every variable occurring in `φ.denseRelabel` is strictly below `φ.numVars`. -/ +theorem mem_vars_denseRelabel_lt (φ : CNF V) {v : ℕ} (hv : v ∈ φ.denseRelabel.vars) : + v < φ.numVars := by + have hv' : v ∈ φ.denseRelabel.vars.toFinset := List.mem_toFinset.mpr hv + rwa [vars_denseRelabel_toFinset, Finset.mem_range] at hv' + +/-- Dense relabeling preserves the number of distinct occurring variables. -/ +@[simp] +theorem numVars_denseRelabel (φ : CNF V) : + φ.denseRelabel.numVars = φ.numVars := by + rw [numVars, vars_denseRelabel_toFinset, Finset.card_range] + +private theorem map_idxOf_of_nodup {α : Type*} [DecidableEq α] (l : List α) (hl : l.Nodup) : + l.map l.idxOf = List.range l.length := by + refine List.ext_getElem (by simp) fun i h₁ h₂ => ?_ + simp only [List.getElem_map, List.getElem_range] + exact List.Nodup.idxOf_getElem hl i _ + +/-- The distinct variables of `φ.denseRelabel` in order of first occurrence are +`0, …, φ.numVars - 1`. -/ +@[simp] +theorem distinctVars_denseRelabel (φ : CNF V) : + φ.denseRelabel.distinctVars = List.range φ.numVars := by + have hinj : Set.InjOn φ.distinctVars.idxOf {v | v ∈ φ.vars} := + fun _ ha _ _ h => (List.idxOf_inj (mem_distinctVars.mpr ha)).mp h + rw [denseRelabel, distinctVars_relabel_of_injOn φ φ.distinctVars.idxOf hinj, + map_idxOf_of_nodup φ.distinctVars φ.nodup_distinctVars, length_distinctVars] + +/-- Reading original variable values at their `distinctVars` indices recovers the evaluation of +`φ`. -/ +theorem eval_denseRelabel (φ : CNF V) (σ : V → Bool) : + φ.denseRelabel.eval (fun i => φ.distinctVars[i]?.elim false σ) = φ.eval σ := by + rw [denseRelabel, CNF.eval_relabel] + apply CNF.eval_congr + intro v hv + have hv' : v ∈ φ.distinctVars := mem_distinctVars.mpr hv + simp [List.getElem?_idxOf hv'] + +/-- Dense relabeling preserves satisfiability. -/ +@[simp] +theorem satisfiable_denseRelabel (φ : CNF V) : + φ.denseRelabel.Satisfiable ↔ φ.Satisfiable := by + constructor + · rintro ⟨σ, hσ⟩ + exact ⟨σ ∘ φ.distinctVars.idxOf, by simpa only [denseRelabel, CNF.eval_relabel] using hσ⟩ + · rintro ⟨σ, hσ⟩ + exact ⟨fun i => φ.distinctVars[i]?.elim false σ, (eval_denseRelabel φ σ).trans hσ⟩ + +/-- Dense relabeling preserves the occurring-variable model count. -/ +@[simp] +theorem modelCount_denseRelabel (φ : CNF V) : + φ.denseRelabel.modelCount = φ.modelCount := + modelCount_dense_relabel φ + +/-- Dense relabeling preserves the declared-variable model count on `Finset.range φ.numVars`. -/ +theorem modelCountOn_denseRelabel (φ : CNF V) : + φ.denseRelabel.modelCountOn (Finset.range φ.numVars) = φ.modelCount := + modelCountOn_dense_relabel φ + +section PolyTime + +variable {W : Type} [DecidableEq W] + +attribute [local fun_prop] ComputableInPolyTime.tidy in +/-- Dense relabeling is polynomial-time into unary variable indices for any variable encoding. -/ +@[fun_prop] +theorem computableInPolyTime_denseRelabel_unary (enc : W ↪ List Bool) : + ComputableInPolyTime (CNF.denseRelabel (V := W)) + (encList (encList (encPair enc encBool))) + (encList (encList (encPair encUnary encBool))) := by + have hd : ComputableTidilyInPolyTime (CNF.distinctVars (V := W)) + (encList (encList (encPair enc encBool))) (encList enc) := + (CNF.computableInPolyTime_distinctVars enc).tidy + refine .of_tidy ?_ + unfold CNF.denseRelabel CNF.relabel Clause.relabel Prod.map + fun_prop + +attribute [local fun_prop] ComputableInPolyTime.tidy in +/-- Dense relabeling is polynomial-time into binary natural-number variable indices (`encCNF`) for +any variable encoding. -/ +@[fun_prop] +theorem computableInPolyTime_denseRelabel (enc : W ↪ List Bool) : + ComputableInPolyTime (CNF.denseRelabel (V := W)) + (encList (encList (encPair enc encBool))) + Cslib.Complexity.encCNF := by + have h1 : ComputableTidilyInPolyTime (CNF.denseRelabel (V := W)) + (encList (encList (encPair enc encBool))) + (encList (encList (encPair encUnary encBool))) := + (computableInPolyTime_denseRelabel_unary enc).tidy + have h2 : ComputableTidilyInPolyTime (CNF.relabel (id : ℕ → ℕ)) + (encList (encList (encPair encUnary encBool))) + (encList (encList (encPair encNat encBool))) := + (CNF.computableInPolyTime_relabel (encV := encUnary) (encW := encNat) + (.of_tidy unary_to_binary)).tidy + have heq : (CNF.denseRelabel (V := W)) = fun φ => (CNF.denseRelabel φ).relabel id := by + funext φ + exact (CNF.relabel_id _).symm + rw [heq] + exact .of_tidy (h2.comp h1) + +end PolyTime + +end Cslib.Logic.PL.CNF + +namespace Cslib.Complexity.SAT + +open Cslib.Logic.PL Turing.MultiTapeTM + +/-- Dense variable relabeling on `CNF ℕ` is computable in polynomial time. -/ +@[fun_prop] +theorem computableInPolyTime_denseRelabel : + ComputableInPolyTime (CNF.denseRelabel (V := ℕ)) encCNF encCNF := + CNF.computableInPolyTime_denseRelabel encNat + +end Cslib.Complexity.SAT diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingList.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingList.lean new file mode 100644 index 000000000..208131c33 --- /dev/null +++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingList.lean @@ -0,0 +1,399 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Logics.Propositional.ClauseSet.Sparsification.Counting +public import Complexity.Logics.Propositional.ClauseSet.Sparsification.List + +/-! +# Counting sparsification on CNF formulas + +List-level operations for the counting sparsification refinement of Appendix A.1 [OpenAI2026ETH]: +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][OpenAI2026ETH] +-/ + +@[expose] public section + +namespace Cslib.Logic.PL.CNF.Sparsification + +open Finset ClauseSet.Sparsification +open scoped List + +variable {V : Type*} [DecidableEq V] + +/-! ### Tautology removal and counting normalization -/ + +/-- Whether a clause contains both a literal and its negation. -/ +def Clause.isTautology (C : Clause V) : Bool := + C.any fun l => C.any (· == Std.Sat.Literal.negate l) + +/-- Remove tautological clauses from a CNF formula. -/ +def removeTautologies (φ : CNF V) : CNF V := + φ.filter fun C => !Clause.isTautology C + +/-- Bring a formula into nontautological normal form: remove tautological clauses, deduplicate +literals and clauses, and reduce by strict subset containment. -/ +def countingNormalize (φ : CNF V) : CNF V := + normalize (removeTautologies φ) + +/-- Singleton clauses `[-l]` for each literal `l` of a heart `H`. -/ +def negatedHeartUnits (H : Clause V) : CNF V := + H.map fun l => [Std.Sat.Literal.negate l] + +/-- The clauses introduced by a counting-sparsification branch: the heart (`false`) or the petals +together with the singleton negated-heart units (`true`). -/ +def countingIntro (ψ : CNF V) (c : ℕ) (H : Clause V) (b : Bool) : CNF V := + if b then petals ψ c H ++ negatedHeartUnits H else [H] + +/-- A counting child of a branching node: append the introduced clauses, deduplicate clauses with +identical literal sets, and reduce by strict subset containment. -/ +def countingChild (ψ : CNF V) (c : ℕ) (H : Clause V) (b : Bool) : CNF V := + reduce (dedupClauses (ψ ++ countingIntro ψ c H b)) + +/-- One deterministic counting-sparsification step using the computed choice `choice θ k ψ`. -/ +def countingNext (θ : ℕ → ℕ) (k : ℕ) (ψ : CNF V) (b : Bool) : CNF V := + countingChild ψ (choice θ k ψ).1 (choice θ k ψ).2 b + +/-- 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)). -/ +def countingThreshold (M j : ℕ) : ℕ := M ^ j + +/-- For `1 ≤ M`, every counting threshold is positive. -/ +theorem one_le_countingThreshold {M : ℕ} (hM : 1 ≤ M) (j : ℕ) : + 1 ≤ countingThreshold M j := + Nat.one_le_pow j M hM + +/-! ### Nontautological normal form -/ + +/-- A CNF formula is *nontautological* if no clause contains both a literal and its negation. -/ +def Nontautological (ψ : CNF V) : Prop := + ∀ C ∈ ψ, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C + +/-- The normal form for list-level counting sparsification at width `k`: `Normalized k ψ` together +with `Nontautological ψ`. -/ +structure CountingNormalized (k : ℕ) (ψ : CNF V) : Prop extends Normalized k ψ where + nontautological : Nontautological ψ + +theorem Clause.isTautology_eq_true_iff {C : Clause V} : + Clause.isTautology C = true ↔ ∃ l ∈ C, Std.Sat.Literal.negate l ∈ C := by + simp [Clause.isTautology] + +theorem Clause.isTautology_eq_false_iff {C : Clause V} : + Clause.isTautology C = false ↔ ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C := by + rw [← Bool.not_eq_true, Clause.isTautology_eq_true_iff] + push Not + rfl + +/-- Any tautological clause evaluates to `true` under every assignment. -/ +theorem eval_eq_true_of_isTautology {C : Clause V} (h : Clause.isTautology C = true) + (σ : V → Bool) : C.eval σ = true := by + obtain ⟨⟨v, b⟩, hl, hneg⟩ := Clause.isTautology_eq_true_iff.mp h + rw [Clause.eval_eq_true_iff] + by_cases hσ : σ v = b + · exact ⟨(v, b), hl, hσ⟩ + · refine ⟨Std.Sat.Literal.negate (v, b), hneg, ?_⟩ + cases b <;> cases hσ' : σ v <;> simp_all [Std.Sat.Literal.negate] + +/-- `removeTautologies φ` is a sublist of `φ`. -/ +theorem removeTautologies_sublist (φ : CNF V) : removeTautologies φ <+ φ := + List.filter_sublist + +/-- Removing tautological clauses preserves evaluation under every assignment. -/ +@[simp] +theorem eval_removeTautologies (φ : CNF V) (σ : V → Bool) : + (removeTautologies φ).eval σ = φ.eval σ := by + rw [Bool.eq_iff_iff, CNF.eval_eq_true_iff, CNF.eval_eq_true_iff] + constructor + · intro h C hC + rcases Bool.eq_false_or_eq_true (Clause.isTautology C) with htrue | hfalse + · exact eval_eq_true_of_isTautology htrue σ + · exact h C (List.mem_filter.mpr ⟨hC, by simp [hfalse]⟩) + · intro h C hC + exact h C (List.mem_filter.mp hC).1 + +/-- Removing tautological clauses preserves the declared-variable model count. -/ +@[simp] +theorem modelCountOn_removeTautologies (φ : CNF V) (declared : Finset V) : + (removeTautologies φ).modelCountOn declared = φ.modelCountOn declared := by + simp only [CNF.modelCountOn, eval_removeTautologies] + +/-- `removeTautologies φ` is nontautological. -/ +theorem nontautological_removeTautologies (φ : CNF V) : + Nontautological (removeTautologies φ) := by + intro C hC + have h := (List.mem_filter.mp hC).2 + rw [Bool.not_eq_true'] at h + exact Clause.isTautology_eq_false_iff.mp h + +/-- The clause set of `countingNormalize φ` has the same satisfying assignments as `φ`. -/ +theorem sat_toClauseSet_countingNormalize_iff (φ : CNF V) (σ : V → Bool) : + (countingNormalize φ).toClauseSet.Sat σ ↔ φ.eval σ = true := by + rw [countingNormalize, sat_toClauseSet_normalize_iff, eval_removeTautologies] + +/-- `countingNormalize φ` evaluates identically to `φ` under every assignment. -/ +@[simp] +theorem eval_countingNormalize (φ : CNF V) (σ : V → Bool) : + (countingNormalize φ).eval σ = φ.eval σ := by + rw [Bool.eq_iff_iff, ← CNF.sat_toClauseSet_iff, sat_toClauseSet_countingNormalize_iff] + +/-- `countingNormalize φ` preserves the declared-variable model count. -/ +@[simp] +theorem modelCountOn_countingNormalize (φ : CNF V) (declared : Finset V) : + (countingNormalize φ).modelCountOn declared = φ.modelCountOn declared := by + simp only [CNF.modelCountOn, eval_countingNormalize] + +/-- Every clause of `countingNormalize φ` has the literals of a nontautological clause of `φ`. -/ +theorem exists_of_mem_countingNormalize {φ : CNF V} {C : Clause V} + (hC : C ∈ countingNormalize φ) : + ∃ D ∈ removeTautologies φ, C.toFinset = D.toFinset := by + have hsub : countingNormalize φ <+ (removeTautologies φ).map dedup := + (reduce_sublist _).trans (dedupClauses_sublist _) + obtain ⟨D, hD, rfl⟩ := List.mem_map.mp (hsub.subset hC) + exact ⟨D, hD, toFinset_dedup D⟩ + +/-- The number of clauses of `countingNormalize φ` is at most that of `φ`. -/ +theorem length_countingNormalize_le (φ : CNF V) : + (countingNormalize φ).length ≤ φ.length := + ((reduce_sublist _).trans (dedupClauses_sublist _)).length_le.trans + ((List.length_map _).le.trans (removeTautologies_sublist φ).length_le) + +/-- Every variable occurring in `countingNormalize φ` occurs in `φ`. -/ +theorem mem_vars_of_mem_countingNormalize {φ : CNF V} : + ∀ C ∈ (countingNormalize φ).toClauseSet, ∀ l ∈ C, l.1 ∈ φ.vars.toFinset := by + intro C hC l hl + obtain ⟨C', hC', rfl⟩ := mem_toClauseSet.mp hC + obtain ⟨D, hD, hDeq⟩ := exists_of_mem_countingNormalize hC' + rw [hDeq, List.mem_toFinset] at hl + have hDφ := (removeTautologies_sublist φ).subset hD + exact List.mem_toFinset.mpr (List.mem_map.mpr ⟨l, List.mem_flatten.mpr ⟨D, hDφ, hl⟩, rfl⟩) + +/-- Every formula of width `k` is brought into nontautological normal form by +`countingNormalize`. -/ +theorem countingNormalized_countingNormalize {k : ℕ} {φ : CNF V} + (hφ : ∀ C ∈ φ, C.length ≤ k) : CountingNormalized k (countingNormalize φ) := by + refine ⟨normalized_normalize fun C hC => hφ C ((removeTautologies_sublist φ).subset hC), + fun C hC l hl hneg => ?_⟩ + obtain ⟨D, hD, hCD⟩ := exists_of_mem_countingNormalize hC + have hlD : l ∈ D := List.mem_toFinset.mp (hCD ▸ List.mem_toFinset.mpr hl) + have hnegD : Std.Sat.Literal.negate l ∈ D := + List.mem_toFinset.mp (hCD ▸ List.mem_toFinset.mpr hneg) + exact nontautological_removeTautologies φ D hD l hlD hnegD + +/-! ### Agreement with clause-set counting operations -/ + +/-- The clause set of `negatedHeartUnits H` is `ClauseSet.Sparsification.negatedHeartUnits`. -/ +theorem toClauseSet_negatedHeartUnits (H : Clause V) : + (negatedHeartUnits H).toClauseSet = + ClauseSet.Sparsification.negatedHeartUnits H.toFinset := by + ext C + simp [negatedHeartUnits, ClauseSet.Sparsification.negatedHeartUnits, CNF.toClauseSet] + +/-- The list-level counting children compute the clause-set counting children. -/ +theorem toClauseSet_countingChild {ψ : CNF V} (hnd : ∀ C ∈ ψ, C.Nodup) (c : ℕ) (H : Clause V) + (b : Bool) : + (countingChild ψ c H b).toClauseSet = + ClauseSet.Sparsification.countingChild ψ.toClauseSet c H.toFinset b := by + rw [countingChild, toClauseSet_reduce, toClauseSet_dedupClauses, toClauseSet_append] + cases b + · simp [countingIntro, ClauseSet.Sparsification.countingChild, + ClauseSet.Sparsification.child, ClauseSet.Sparsification.intro, CNF.toClauseSet] + · simp only [countingIntro, ite_true, toClauseSet_append, toClauseSet_petals hnd, + toClauseSet_negatedHeartUnits, ClauseSet.Sparsification.countingChild, Finset.union_assoc] + +/-- The clause set of `countingNext θ k ψ b` equals the clause-set counting child for the computed +choice. -/ +theorem toClauseSet_countingNext {θ : ℕ → ℕ} {k : ℕ} {ψ : CNF V} (h : Normalized k ψ) (b : Bool) : + (countingNext θ k ψ b).toClauseSet = ClauseSet.Sparsification.countingChild ψ.toClauseSet + (choice θ k ψ).1 (choice θ k ψ).2.toFinset b := + toClauseSet_countingChild h.nodup _ _ b + +/-- A formula and the canonical CNF of its clause set have the same declared-variable model +count. -/ +theorem modelCountOn_toCNF_toClauseSet (ψ : CNF V) (declared : Finset V) : + ψ.toClauseSet.toCNF.modelCountOn declared = ψ.modelCountOn declared := by + simp only [CNF.modelCountOn] + congr 1 + ext σ + simp only [Finset.mem_filter, Finset.mem_univ, true_and, ClauseSet.eval_toCNF_eq_true_iff, + CNF.sat_toClauseSet_iff] + +/-- **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 modelCountOn_countingChild {ψ : CNF V} (hnd : ∀ C ∈ ψ, C.Nodup) (c : ℕ) (H : Clause V) + (declared : Finset V) : + ψ.modelCountOn declared = + (countingChild ψ c H false).modelCountOn declared + + (countingChild ψ c H true).modelCountOn declared := by + rw [← modelCountOn_toCNF_toClauseSet ψ, + ← modelCountOn_toCNF_toClauseSet (countingChild ψ c H false), + ← modelCountOn_toCNF_toClauseSet (countingChild ψ c H true), + toClauseSet_countingChild hnd c H false, + toClauseSet_countingChild hnd c H true] + exact ClauseSet.Sparsification.modelCountOn_countingChild ψ.toClauseSet c H.toFinset 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. -/ +theorem modelCountOn_countingNext {θ : ℕ → ℕ} {k : ℕ} {ψ : CNF V} (h : Normalized k ψ) + (declared : Finset V) : + ψ.modelCountOn declared = + (countingNext θ k ψ false).modelCountOn declared + + (countingNext θ k ψ true).modelCountOn declared := + modelCountOn_countingChild h.nodup _ _ declared + +/-! ### Preservation of normal form under the counting step -/ + +omit [DecidableEq V] in +private theorem literal_negate_ne_self (l : Literal V) : Std.Sat.Literal.negate l ≠ l := by + rcases l with ⟨v, b⟩ + cases b <;> simp [Std.Sat.Literal.negate] + +/-- 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 countingNormalized_countingChild {k : ℕ} {ψ : CNF V} (hk : 1 ≤ k) + (h : CountingNormalized k ψ) {c : ℕ} {H : Clause V} (hH_nodup : H.Nodup) + (hH_len : H.length ≤ k) (hH_nontaut : ∀ l ∈ H, Std.Sat.Literal.negate l ∉ H) (b : Bool) : + CountingNormalized k (countingChild ψ c H b) := by + have hsub : countingChild ψ c H b <+ ψ ++ countingIntro ψ c H b := + (reduce_sublist _).trans (dedupClauses_sublist _) + have hintro : ∀ C ∈ countingIntro ψ c H b, + C.Nodup ∧ C.length ≤ k ∧ ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C := by + intro C hC + cases b + · simp only [countingIntro, Bool.false_eq_true, ite_false, List.mem_singleton] at hC + subst hC + exact ⟨hH_nodup, hH_len, hH_nontaut⟩ + · simp only [countingIntro, ite_true, List.mem_append, petals, negatedHeartUnits, + List.mem_map] at hC + rcases hC with ⟨D, hD, rfl⟩ | ⟨l₀, _, rfl⟩ + · have hDψ : D ∈ ψ := List.filter_sublist.subset hD + refine ⟨(h.nodup D hDψ).filter _, ?_, fun l hl hneg => ?_⟩ + · exact (List.length_filter_le _ D).trans (h.length_le D hDψ) + · exact h.nontautological D hDψ l (List.mem_filter.mp hl).1 (List.mem_filter.mp hneg).1 + · refine ⟨List.nodup_singleton _, by simpa using hk, fun l hl hneg => ?_⟩ + rw [List.mem_singleton] at hl hneg + subst hl + exact literal_negate_ne_self _ hneg + refine ⟨⟨fun C hC => ?_, fun C hC => ?_, ?_, ?_⟩, fun C hC => ?_⟩ + · rcases List.mem_append.mp (hsub.subset hC) with hC | hC + · exact h.nodup C hC + · exact (hintro C hC).1 + · rcases List.mem_append.mp (hsub.subset hC) with hC | hC + · exact h.length_le C hC + · exact (hintro C hC).2.1 + · exact ((reduce_sublist _).map _).nodup (nodup_toFinset_dedupClauses _) + · rw [countingChild, toClauseSet_reduce] + exact reduced_reduce _ + · rcases List.mem_append.mp (hsub.subset hC) with hC | hC + · exact h.nontautological C hC + · exact (hintro C hC).2.2 + +private theorem choice_snd_sublist_or_nil (θ : ℕ → ℕ) (k : ℕ) (ψ : CNF V) : + (choice θ k ψ).2 = [] ∨ ∃ C ∈ ψ, (choice θ k ψ).2 <+ C := by + unfold choice + rcases hhead : ((List.range ((k + 1) * (k + 1) + 1)).flatMap fun r => + ((candidates k ψ).filter (heavy θ ψ)).filter fun x => rank k x == r).head? with _ | x + · exact Or.inl rfl + · refine Or.inr ?_ + have hx := List.mem_of_mem_head? hhead + obtain ⟨r, -, hxr⟩ := List.mem_flatMap.mp hx + have hxcand := (List.mem_filter.mp (List.mem_filter.mp hxr).1).1 + obtain ⟨C, hC, hxH⟩ := List.mem_flatMap.mp hxcand + obtain ⟨H, hH, rfl⟩ := List.mem_map.mp hxH + exact ⟨C, hC, mem_hearts hH⟩ + +/-- **One counting-sparsification step preserves `CountingNormalized k`.** -/ +theorem countingNormalized_countingNext (θ : ℕ → ℕ) {k : ℕ} (hk : 1 ≤ k) {ψ : CNF V} + (h : CountingNormalized k ψ) (b : Bool) : + CountingNormalized k (countingNext θ k ψ b) := by + rcases choice_snd_sublist_or_nil θ k ψ with hnil | ⟨C, hC, hsub⟩ + · refine countingNormalized_countingChild hk h ?_ ?_ ?_ b <;> simp [hnil] + · refine countingNormalized_countingChild hk h (hsub.nodup (h.nodup C hC)) + (hsub.length_le.trans (h.length_le C hC)) + (fun l hl hneg => h.nontautological C hC l (hsub.subset hl) (hsub.subset hneg)) b + +/-- Every literal occurring in `countingChild ψ c H b` occurs in `ψ` or has its variable in `H`. -/ +theorem support_countingChild {ψ : 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 ∈ countingChild ψ c H b, ∀ l ∈ C, l.1 ∈ declared := by + have hsub : countingChild ψ c H b <+ ψ ++ countingIntro ψ c H b := + (reduce_sublist _).trans (dedupClauses_sublist _) + intro C hC l hl + rcases List.mem_append.mp (hsub.subset hC) with hC | hC + · exact hψ C hC l hl + · cases b + · simp only [countingIntro, Bool.false_eq_true, ite_false, List.mem_singleton] at hC + subst hC + exact hH l hl + · simp only [countingIntro, ite_true, List.mem_append, petals, negatedHeartUnits, + List.mem_map] at hC + rcases hC with ⟨D, hD, rfl⟩ | ⟨l₀, hl₀, rfl⟩ + · exact hψ D (List.filter_sublist.subset hD) l (List.mem_filter.mp hl).1 + · rw [List.mem_singleton] at hl + subst hl + exact hH l₀ hl₀ + +/-- Every literal occurring in `countingNext θ k ψ b` has its variable in `declared` whenever `ψ` +does. -/ +theorem support_countingNext (θ : ℕ → ℕ) (k : ℕ) {ψ : CNF V} {declared : Finset V} + (hψ : ∀ C ∈ ψ, ∀ l ∈ C, l.1 ∈ declared) (b : Bool) : + ∀ C ∈ countingNext θ k ψ b, ∀ l ∈ C, l.1 ∈ declared := by + refine support_countingChild hψ (fun l hl => ?_) b + rcases choice_snd_sublist_or_nil θ k ψ with hnil | ⟨C, hC, hsub⟩ + · simp [hnil] at hl + · exact hψ C hC l (hsub.subset hl) + +end Cslib.Logic.PL.CNF.Sparsification diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingPolyTime.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingPolyTime.lean new file mode 100644 index 000000000..b4041e310 --- /dev/null +++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingPolyTime.lean @@ -0,0 +1,100 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingList +public import Complexity.Logics.Propositional.ClauseSet.Sparsification.PolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain + +/-! +# Counting sparsification -- the step is polynomial-time + +The list-level counting-sparsification step (`Cslib.Logic.PL.CNF.Sparsification.countingNext`), +tautology removal (`Cslib.Logic.PL.CNF.Sparsification.removeTautologies`), nontautological +normalization (`Cslib.Logic.PL.CNF.Sparsification.countingNormalize`), and comparison with the +counting thresholds `countingThreshold M j = M ^ j` +(`Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingThreshold_le`) are polynomial-time +on the framed encoding of formulas, for any encoding of the variables [OpenAI2026ETH, Appendix A.1]. + +## Main results + +* `Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingThreshold_le`: comparisons with + `countingThreshold M`. +* `Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_removeTautologies`, + `Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingNormalize`: tautology removal and + nontautological normalization. +* `Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_countingNext`: the list-level counting + step. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*, Appendix A.1][OpenAI2026ETH] +-/ + +@[expose] public section + +open Turing.MultiTapeTM ComputableTidilyInPolyTime + +namespace Cslib.Logic.PL.CNF.Sparsification + +/-- Comparing the counting thresholds `countingThreshold M j = M ^ j` with a number is +polynomial-time in unary. -/ +theorem computableInPolyTime_countingThreshold_le (M : ℕ) : + ComputableInPolyTime (fun p : ℕ × ℕ => decide (countingThreshold M p.1 ≤ p.2)) + (encPair encUnary encUnary) encBool := by + unfold countingThreshold + fun_prop + +variable {V : Type} [DecidableEq V] (encV : V ↪ List Bool) + +/-- The framed encoding of clauses. -/ +local notation "encC" => encList (encPair encV encBool) + +/-- The framed encoding of formulas. -/ +local notation "encF" => encList (encList (encPair encV encBool)) + +/-- Tautology testing on a clause is polynomial-time. -/ +theorem computableInPolyTime_isTautology : + ComputableInPolyTime (Clause.isTautology (V := V)) encC encBool := by + refine .of_tidy ?_ + unfold Clause.isTautology Std.Sat.Literal.negate + fun_prop + +/-- Removing tautological clauses from a formula is polynomial-time. -/ +theorem computableInPolyTime_removeTautologies : + ComputableInPolyTime (removeTautologies (V := V)) encF encF := by + refine .of_tidy ?_ + have htaut := (computableInPolyTime_isTautology encV).tidy + unfold removeTautologies + fun_prop + +/-- Nontautological normalization (`countingNormalize`) is polynomial-time. -/ +theorem computableInPolyTime_countingNormalize : + ComputableInPolyTime (countingNormalize (V := V)) encF encF := by + have hrem := (computableInPolyTime_removeTautologies encV).tidy + have hnorm := (computableInPolyTime_normalize encV).tidy + exact .of_tidy (hnorm.comp hrem) + +/-- **The list-level counting-sparsification step is polynomial-time.** -/ +theorem computableInPolyTime_countingNext {θ : ℕ → ℕ} + (hθ : ComputableInPolyTime (fun p : ℕ × ℕ => decide (θ p.1 ≤ p.2)) + (encPair encUnary encUnary) encBool) (k : ℕ) : + ComputableInPolyTime (fun p : CNF V × Bool => countingNext θ k p.1 p.2) + (encPair encF encBool) encF := by + refine .of_tidy ?_ + have := (computableInPolyTime_choice encV hθ k).tidy + have := (computableInPolyTime_reduce encV).tidy + have := (computableInPolyTime_dedupClauses encV).tidy + have := (computableInPolyTime_flower encV).tidy + unfold countingNext countingChild countingIntro petals negatedHeartUnits Std.Sat.Literal.negate + fun_prop + +end Cslib.Logic.PL.CNF.Sparsification diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/List.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/List.lean index c48bccdcc..cd7b9e3e2 100644 --- a/Complexity/Logics/Propositional/ClauseSet/Sparsification/List.lean +++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification/List.lean @@ -178,7 +178,7 @@ private theorem not_and_not_subclause_iff {D C : Clause V} : cases subclause D C <;> cases subclause C D <;> simp /-- The list-level reduction computes the reduction of clause sets. -/ -private theorem toClauseSet_reduce (ψ : CNF V) : +theorem toClauseSet_reduce (ψ : CNF V) : (reduce ψ).toClauseSet = ClauseSet.Sparsification.reduce ψ.toClauseSet := by have hkeep (C : Clause V) : (ψ.all fun D => !(subclause D C && !subclause C D)) = true ↔ ∀ D' ∈ ψ.toClauseSet, ¬ D' ⊂ C.toFinset := by @@ -199,7 +199,8 @@ private theorem toClauseSet_reduce (ψ : CNF V) : obtain ⟨C, hC, rfl⟩ := mem_toClauseSet.mp hC' exact ⟨C, List.mem_filter.mpr ⟨hC, (hkeep C).mpr hk⟩, rfl⟩ -private theorem toClauseSet_flower {ψ : CNF V} (hnd : ∀ C ∈ ψ, C.Nodup) (c : ℕ) (H : Clause V) : +/-- The list-level flower computes the clause-set flower when clauses have no repeated literals. -/ +theorem toClauseSet_flower {ψ : CNF V} (hnd : ∀ C ∈ ψ, C.Nodup) (c : ℕ) (H : Clause V) : (flower ψ c H).toClauseSet = ClauseSet.Sparsification.flower ψ.toClauseSet c H.toFinset := by ext C' rw [mem_toClauseSet, ClauseSet.Sparsification.mem_flower, mem_toClauseSet] @@ -221,7 +222,8 @@ theorem toFinset_filter_not_mem (C H : Clause V) : rw [Bool.not_eq_true', List.any_eq_false] exact ⟨fun h hl => h l hl (beq_self_eq_true l), fun h l' hl' heq => h (beq_iff_eq.mp heq ▸ hl')⟩ -private theorem toClauseSet_petals {ψ : CNF V} (hnd : ∀ C ∈ ψ, C.Nodup) (c : ℕ) (H : Clause V) : +/-- The list-level petals compute the clause-set petals when clauses have no repeated literals. -/ +theorem toClauseSet_petals {ψ : CNF V} (hnd : ∀ C ∈ ψ, C.Nodup) (c : ℕ) (H : Clause V) : (petals ψ c H).toClauseSet = ClauseSet.Sparsification.petals ψ.toClauseSet c H.toFinset := by ext C' rw [mem_toClauseSet, ClauseSet.Sparsification.mem_petals, ← toClauseSet_flower hnd] @@ -289,7 +291,8 @@ private theorem heavy_eq_true_iff {θ : ℕ → ℕ} {k : ℕ} {ψ : CNF V} (h : /-! ### Candidates -/ omit [DecidableEq V] in -private theorem mem_hearts {k : ℕ} {C H : Clause V} (hH : H ∈ hearts k C) : H <+ C := by +/-- Every candidate heart of `C` is a sublist of `C`. -/ +theorem mem_hearts {k : ℕ} {C H : Clause V} (hH : H ∈ hearts k C) : H <+ C := by obtain ⟨S, -, rfl⟩ := List.mem_map.mp hH conv_rhs => rw [← List.zipIdx_map_fst 0 C] exact List.filter_sublist.map _ @@ -606,7 +609,8 @@ private theorem pairwise_zipIdx (ψ : CNF V) : simp only [List.getElem_zipIdx, Nat.zero_add] exact hij -private theorem nodup_toFinset_dedupClauses (ψ : CNF V) : +/-- Deduplicating clauses produces clauses with pairwise distinct literal sets. -/ +theorem nodup_toFinset_dedupClauses (ψ : CNF V) : ((dedupClauses ψ).map List.toFinset).Nodup := by rw [dedupClauses, List.map_map, List.nodup_iff_pairwise_ne, List.pairwise_map] refine ((pairwise_zipIdx ψ).filter _).imp_of_mem fun {p q} _ hq hpq heq => ?_ @@ -618,7 +622,8 @@ private theorem nodup_toFinset_dedupClauses (ψ : CNF V) : have h₂ : subclause q.1 p.1 = true := subclause_eq_true_iff.mpr heq.ge simp [hpq, h₁, h₂] at this -private theorem toClauseSet_dedupClauses (ψ : CNF V) : +/-- Deduplicating clauses preserves the clause set. -/ +theorem toClauseSet_dedupClauses (ψ : CNF V) : (dedupClauses ψ).toClauseSet = ψ.toClauseSet := by refine Finset.Subset.antisymm (toClauseSet_mono (dedupClauses_sublist ψ).subset) ?_ intro C' hC' diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/PolyTime.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/PolyTime.lean index 74bdac967..9e1a3cd24 100644 --- a/Complexity/Logics/Propositional/ClauseSet/Sparsification/PolyTime.lean +++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification/PolyTime.lean @@ -74,23 +74,36 @@ local notation "encC" => encList (encPair encV encBool) local notation "encF" => encList (encList (encPair encV encBool)) /-- The list-level reduction is polynomial-time. -/ -private theorem computableTidilyInPolyTime_reduce : - ComputableTidilyInPolyTime (reduce (V := V)) encF encF := by +theorem computableInPolyTime_reduce : + ComputableInPolyTime (reduce (V := V)) encF encF := by + refine .of_tidy ?_ unfold reduce subclause fun_prop -private theorem computableTidilyInPolyTime_flower : - ComputableTidilyInPolyTime (fun p : CNF V × (ℕ × Clause V) => flower p.1 p.2.1 p.2.2) +/-- Removing duplicate clauses with identical literal sets is polynomial-time. -/ +theorem computableInPolyTime_dedupClauses : + ComputableInPolyTime (dedupClauses (V := V)) encF encF := by + refine .of_tidy ?_ + unfold dedupClauses subclause + fun_prop + +/-- Computing the flower of a clause size and heart is polynomial-time. -/ +theorem computableInPolyTime_flower : + ComputableInPolyTime (fun p : CNF V × (ℕ × Clause V) => flower p.1 p.2.1 p.2.2) (encPair encF (encPair encUnary encC)) encF := by + refine .of_tidy ?_ unfold flower subclause fun_prop -private theorem computableTidilyInPolyTime_heavy {θ : ℕ → ℕ} - (hθ : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => decide (θ p.1 ≤ p.2)) +/-- Testing whether a candidate `(c, H)` is heavy is polynomial-time. -/ +theorem computableInPolyTime_heavy {θ : ℕ → ℕ} + (hθ : ComputableInPolyTime (fun p : ℕ × ℕ => decide (θ p.1 ≤ p.2)) (encPair encUnary encUnary) encBool) : - ComputableTidilyInPolyTime (fun p : CNF V × (ℕ × Clause V) => heavy θ p.1 p.2) + ComputableInPolyTime (fun p : CNF V × (ℕ × Clause V) => heavy θ p.1 p.2) (encPair encF (encPair encUnary encC)) encBool := by - have := computableTidilyInPolyTime_flower encV + have hθ := hθ.tidy + refine .of_tidy ?_ + have := (computableInPolyTime_flower encV).tidy have h₁ : ComputableTidilyInPolyTime (fun p : CNF V × (ℕ × Clause V) => decide (1 ≤ p.2.2.length) && decide (p.2.2.length < p.2.1)) (encPair encF (encPair encUnary encC)) encBool := by @@ -102,8 +115,10 @@ private theorem computableTidilyInPolyTime_heavy {θ : ℕ → ℕ} exact bool_and.comp (h₁.prod (hθ.comp h₂)) omit [DecidableEq V] in -private theorem computableTidilyInPolyTime_candidates (k : ℕ) : - ComputableTidilyInPolyTime (candidates (V := V) k) encF (encList (encPair encUnary encC)) := by +/-- Listing the candidate pairs `(c, H)` of a formula is polynomial-time. -/ +theorem computableInPolyTime_candidates (k : ℕ) : + ComputableInPolyTime (candidates (V := V) k) encF (encList (encPair encUnary encC)) := by + refine .of_tidy ?_ have : ComputableTidilyInPolyTime (hearts (V := V) k) encC (encList encC) := by unfold hearts fun_prop @@ -111,14 +126,15 @@ private theorem computableTidilyInPolyTime_candidates (k : ℕ) : fun_prop /-- The computed choice is polynomial-time. -/ -private theorem computableTidilyInPolyTime_choice {θ : ℕ → ℕ} - (hθ : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => decide (θ p.1 ≤ p.2)) +theorem computableInPolyTime_choice {θ : ℕ → ℕ} + (hθ : ComputableInPolyTime (fun p : ℕ × ℕ => decide (θ p.1 ≤ p.2)) (encPair encUnary encUnary) encBool) (k : ℕ) : - ComputableTidilyInPolyTime (choice (V := V) θ k) encF (encPair encUnary encC) := by + ComputableInPolyTime (choice (V := V) θ k) encF (encPair encUnary encC) := by + refine .of_tidy ?_ have hc : ComputableTidilyInPolyTime (fun ψ : CNF V => (candidates k ψ).filter (heavy θ ψ)) encF (encList (encPair encUnary encC)) := - filterWithInput (computableTidilyInPolyTime_candidates encV k) - (computableTidilyInPolyTime_heavy encV hθ) + filterWithInput (computableInPolyTime_candidates encV k).tidy + (computableInPolyTime_heavy encV hθ).tidy have hr : ComputableTidilyInPolyTime (fun x : ℕ × Clause V => rank k x) (encPair encUnary encC) encUnary := by unfold rank @@ -136,11 +152,10 @@ theorem computableInPolyTime_isSparse {θ : ℕ → ℕ} (hθ : ComputableInPolyTime (fun p : ℕ × ℕ => decide (θ p.1 ≤ p.2)) (encPair encUnary encUnary) encBool) (k : ℕ) : ComputableInPolyTime (isSparse (V := V) θ k) encF encBool := by - have hθ := hθ.tidy refine .of_tidy ?_ unfold isSparse - exact bool_not.comp (anyWithInput (computableTidilyInPolyTime_candidates encV k) - (computableTidilyInPolyTime_heavy encV hθ)) + exact bool_not.comp (anyWithInput (computableInPolyTime_candidates encV k).tidy + (computableInPolyTime_heavy encV hθ).tidy) /-- **The list-level step is polynomial-time.** -/ theorem computableInPolyTime_next {θ : ℕ → ℕ} @@ -148,11 +163,10 @@ theorem computableInPolyTime_next {θ : ℕ → ℕ} (encPair encUnary encUnary) encBool) (k : ℕ) : ComputableInPolyTime (fun p : CNF V × Bool => next θ k p.1 p.2) (encPair encF encBool) encF := by - have hθ := hθ.tidy refine .of_tidy ?_ - have := computableTidilyInPolyTime_choice encV hθ k - have := computableTidilyInPolyTime_reduce encV - have := computableTidilyInPolyTime_flower encV + have := (computableInPolyTime_choice encV hθ k).tidy + have := (computableInPolyTime_reduce encV).tidy + have := (computableInPolyTime_flower encV).tidy unfold next child intro petals fun_prop @@ -160,11 +174,12 @@ theorem computableInPolyTime_next {θ : ℕ → ℕ} theorem computableInPolyTime_normalize : ComputableInPolyTime (normalize (V := V)) encF encF := by refine .of_tidy ?_ - have := computableTidilyInPolyTime_reduce encV + have := (computableInPolyTime_reduce encV).tidy + have := (computableInPolyTime_dedupClauses encV).tidy have hdedup : ComputableTidilyInPolyTime (dedup (V := V)) encC encC := by unfold dedup fun_prop - unfold normalize dedupClauses subclause + unfold normalize fun_prop end Cslib.Logic.PL.CNF.Sparsification diff --git a/ComplexityTests/Computability/Complexity/FineGrained/CountingSparsifyPolyTime.lean b/ComplexityTests/Computability/Complexity/FineGrained/CountingSparsifyPolyTime.lean new file mode 100644 index 000000000..9e8ca74af --- /dev/null +++ b/ComplexityTests/Computability/Complexity/FineGrained/CountingSparsifyPolyTime.lean @@ -0,0 +1,116 @@ +/- +Copyright (c) 2026 OpenAI, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: OpenAI, Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.FineGrained.CountingEndpoint +public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingPolyTime + +/-! +# Tests for dense CNF relabeling, list-level counting sparsification, and fine-grained endpoints + +Concrete regression tests and edge-case checks for: +* `Cslib.Logic.PL.CNF.denseRelabel` vs `CNF.compact` on gapped/repeated-literal formulas, empty + formulas, and width-`0`/`1` `KSAT` instances; +* `Cslib.Logic.PL.CNF.Sparsification.removeTautologies`, `countingNormalize`, `countingChild`, and + `countingNext`, including additive `modelCountOn` conservation and `CountingNormalized` + preservation; +* Polynomial-time certificates and fine-grained endpoint reductions in + `Complexity.Computability.Complexity.FineGrained.CountingEndpoint`. +-/ + +@[expose] public section + +namespace Cslib.Complexity.Tests + +open Cslib.Logic.PL Cslib.Logic.PL.CNF.Sparsification Turing.MultiTapeTM + +/-! ### 1. Concrete dense-relabeling vs compaction checks -/ + +/-- A concrete formula whose variable occurrences `[10, 10, 20, 5]` have a duplicate before `20` and +non-monotone variable numbers. -/ +def gappedFormula : CNF ℕ := + [[(10, true), (10, true)], [(20, false), (5, true)]] + +/-- `CNF.compact` uses first occurrence positions in `vars`, leaving a gap at `1` (`[0, 2, 3]`). -/ +example : gappedFormula.compact = [[(0, true), (0, true)], [(2, false), (3, true)]] := by + decide + +/-- `CNF.denseRelabel` uses indices in `distinctVars`, producing dense indices `[0, 1, 2]`. -/ +example : gappedFormula.denseRelabel = [[(0, true), (0, true)], [(1, false), (2, true)]] := by + decide + +example : gappedFormula.denseRelabel.distinctVars = List.range gappedFormula.numVars := + CNF.distinctVars_denseRelabel gappedFormula + +example : gappedFormula.denseRelabel.modelCountOn (Finset.range gappedFormula.numVars) = + gappedFormula.modelCount := + CNF.modelCountOn_denseRelabel gappedFormula + +/-- Edge cases: empty formula and empty-clause formula at `k = 0` and `k = 1`. -/ +example : CNF.denseRelabel ([] : CNF ℕ) = [] := rfl +example : CNF.denseRelabel ([[]] : CNF ℕ) = [[]] := rfl +example : CNF.denseRelabel ([] : CNF ℕ) ∈ KSAT 0 ↔ ([] : CNF ℕ) ∈ KSAT 0 := + CNF.denseRelabel_mem_KSAT_iff +example : CNF.denseRelabel ([[]] : CNF ℕ) ∈ KSAT 1 ↔ ([[]] : CNF ℕ) ∈ KSAT 1 := + CNF.denseRelabel_mem_KSAT_iff + +/-! ### 2. Concrete list-level counting sparsification checks -/ + +/-- A 2-CNF formula with a tautological clause `[(0, true), (0, false)]` and a size-2 flower of +2-clauses sharing the heart `[(0, true)]`. -/ +def flowerWithTautology : CNF ℕ := + [[(0, true), (0, false)], [(0, true), (1, true)], [(0, true), (2, false)]] + +/-- `removeTautologies` drops the tautological clause and keeps the two nontautological clauses. -/ +example : removeTautologies flowerWithTautology = + [[(0, true), (1, true)], [(0, true), (2, false)]] := by + decide + +/-- `countingNormalize` produces a `CountingNormalized 2` formula with the same 3-variable model +count. -/ +example : CountingNormalized 2 (countingNormalize flowerWithTautology) := + countingNormalized_countingNormalize (by decide) + +example : (countingNormalize flowerWithTautology).modelCountOn (Finset.range 3) = + flowerWithTautology.modelCountOn (Finset.range 3) := + modelCountOn_countingNormalize flowerWithTautology (Finset.range 3) + +/-- At threshold `M = 2` (`θ 1 = 2`), `choice (countingThreshold 2) 2` selects the heavy heart +`[(0, true)]` at clause size `2`. -/ +example : choice (countingThreshold 2) 2 (countingNormalize flowerWithTautology) = + (2, [(0, true)]) := by + decide + +/-- The `false` (A) branch reduces to the unit heart `[[(0, true)]]`, while the `true` (B) branch +introduces the petals `[[(1, true)], [(2, false)]]` and the negated-heart unit `[[(0, false)]]`. -/ +example : countingNext (countingThreshold 2) 2 (countingNormalize flowerWithTautology) false = + [[(0, true)]] := by + decide + +example : countingNext (countingThreshold 2) 2 (countingNormalize flowerWithTautology) true = + [[(1, true)], [(2, false)], [(0, false)]] := by + decide + +/-- Both counting children preserve `CountingNormalized 2` and partition the 5 satisfying +assignments on `{0, 1, 2}` into `4 + 1 = 5`. -/ +example : CountingNormalized 2 + (countingNext (countingThreshold 2) 2 (countingNormalize flowerWithTautology) true) := + countingNormalized_countingNext (countingThreshold 2) (by decide) + (countingNormalized_countingNormalize (by decide)) true + +example : (countingNormalize flowerWithTautology).modelCountOn (Finset.range 3) = + CNF.modelCountOn + (countingNext (countingThreshold 2) 2 (countingNormalize flowerWithTautology) false) + (Finset.range 3) + + CNF.modelCountOn + (countingNext (countingThreshold 2) 2 (countingNormalize flowerWithTautology) true) + (Finset.range 3) := + modelCountOn_countingNext + (countingNormalized_countingNormalize (k := 2) (by decide)).toNormalized (Finset.range 3) + +end Cslib.Complexity.Tests