diff --git a/Complexity.lean b/Complexity.lean index 5830f638a9..a634d7a03f 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1427,6 +1427,7 @@ public import Complexity.Computability.Complexity.FineGrained.SparseCountingScal public import Complexity.Computability.Complexity.FineGrained.SparseParitySchedule public import Complexity.Computability.Complexity.FineGrained.Sparsification public import Complexity.Computability.Complexity.FineGrained.ThreeOccurrenceReduction +public import Complexity.Computability.Complexity.FineGrained.WideClauseCounting public import Complexity.Computability.Complexity.HardnessEncoding.PolyTime public import Complexity.Computability.Complexity.HardnessEncoding.Program public import Complexity.Computability.Complexity.Parameterized diff --git a/Complexity/Computability/Complexity/FineGrained/ContractionCounting.lean b/Complexity/Computability/Complexity/FineGrained/ContractionCounting.lean index abfbca7ba2..fef7336cff 100644 --- a/Complexity/Computability/Complexity/FineGrained/ContractionCounting.lean +++ b/Complexity/Computability/Complexity/FineGrained/ContractionCounting.lean @@ -28,7 +28,11 @@ time `2 ^ (A (m + 1) / √⌊log₂ (n + 2)⌋)` times a polynomial in the encod polynomial space, where `m` is the number of clauses and `n` the number of variables (`ContractionCounting.exists_modelCounter`). For formulas with at most `D n` clauses this is time `2 ^ O_{k,D}(n / √log n)` times a polynomial, the fixed-density bound of Theorem 1.1 of -[OpenAI2026ETH] (`ContractionCounting.exists_modelCounter_fixedDensity`). +[OpenAI2026ETH] (`ContractionCounting.exists_modelCounter_fixedDensity`). Measured by the number +`N` of literal occurrences instead, the time is `2 ^ (A (N + 1) / √⌊log₂ (N + 2)⌋)` times a +polynomial (`ContractionCounting.exists_modelCounter_occurrences`), with no logarithm of the number +of variables in the exponent; this form extends to formulas of unbounded clause width +(`Cslib.Complexity.ContractionCounting.exists_modelCounter_unboundedWidth`). The machine is the proof of Appendix D.2: it writes out the clause network of the formula (`Cslib.Circuits.Frontier.ClauseNetwork.clauseNetwork`), whose contraction is the model count, @@ -49,6 +53,8 @@ them. * `Cslib.Complexity.ContractionCounting.exists_modelCounter`: the counter, with exponent `A (m + 1) / √⌊log₂ (n + 2)⌋`. +* `Cslib.Complexity.ContractionCounting.exists_modelCounter_occurrences`: the counter, with exponent + `A (N + 1) / √⌊log₂ (N + 2)⌋` for `N` literal occurrences. * `Cslib.Complexity.ContractionCounting.exists_modelCounter_fixedDensity`: for each density bound `D`, exponent `A (n + 1) / √⌊log₂ (n + 2)⌋` on formulas with at most `D n` clauses. @@ -199,16 +205,24 @@ theorem exponent_le {k K N m n : ℕ} (hN : 1 ≤ N) (hNm : N ≤ k * m) (hnN : nlinarith · exact Nat.sqrt_eq_zero.not.mpr (Nat.log_pos (by norm_num) (by omega)).ne' -/-- **Model counting by tensor contraction.** For each clause width `k`, one machine computes -`φ.modelCount` on every formula `φ` whose clauses have at most `k` literals, in time -`2 ^ (A (m + 1) / √⌊log₂ (n + 2)⌋)` times a polynomial in the encoding length and in polynomial -space, where `m` is the number of clauses and `n` the number of variables. -/ -theorem exists_modelCounter (k : ℕ) : - ∃ (count : CNF ℕ → ℕ) (A e b : ℕ), - (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) → count φ = φ.modelCount) ∧ - ComputableInO count encCNF encNat - (fun φ => 2 ^ (A * (φ.length + 1) / Nat.sqrt (Nat.log 2 (φ.numVars + 2))) * - ((encCNF φ).length + 1) ^ e) +/-- The exponent of the contraction is at most `3 K (N + 1) / √⌊log₂ (N + 2)⌋` for `N ≥ 1` literal +occurrences. -/ +theorem exponent_le_occurrences {K N : ℕ} (hN : 1 ≤ N) : + K * (3 * N) / Nat.sqrt (Nat.log 2 (3 * N)) ≤ + 3 * K * (N + 1) / Nat.sqrt (Nat.log 2 (N + 2)) := by + refine Nat.div_le_div ?_ (Nat.sqrt_le_sqrt (Nat.log_mono_right (by omega))) ?_ + · nlinarith + · exact Nat.sqrt_eq_zero.not.mpr (Nat.log_pos (by norm_num) (by omega)).ne' + +/-- The machine runs in polynomial space, and in time `2 ^ F φ` times a polynomial for every +exponent `F` that bounds the contraction's exponent `K s / √⌊log₂ s⌋` at the network size +`s = 3 N` on the formulas handed to the contraction algorithm. -/ +private theorem computableInO_count (k : ℕ) : + ∃ K e b : ℕ, ∀ F : CNF ℕ → ℕ, + (∀ φ, guard k φ = true → + K * (3 * φ.vars.length) / Nat.sqrt (Nat.log 2 (3 * φ.vars.length)) ≤ F φ) → + ComputableInO (count k) encCNF encNat + (fun φ => 2 ^ F φ * ((encCNF φ).length + 1) ^ e) (fun φ => ((encCNF φ).length + 1) ^ b) := by obtain ⟨K, hK⟩ := fastContractionAlgorithm.bound (k + 4) 1 have hg := NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_guard k) @@ -223,7 +237,7 @@ theorem exists_modelCounter (k : ℕ) : obtain ⟨p, q, hlen⟩ := (computableInPolyTime_contractionInput k).polyBounded_length.exists_le set e := dg + dp + df + q * K set b := dg' + dp' + df' + q * K - refine ⟨count k, 3 * k * K, e, b, fun φ hk => count_eq hk, + refine ⟨K, e, b, fun F hF => (certificate k).computes.mono (cg + cp + cf + K * (p + 1) ^ K + cg' + cp' + cf' + 1) (fun φ => ?_) (fun φ => ?_)⟩ all_goals @@ -241,7 +255,7 @@ theorem exists_modelCounter (k : ℕ) : calc _ ≤ ((p + 1) * Y ^ q) ^ K := Nat.pow_le_pow_left hn' K _ = _ := by rw [mul_pow, pow_mul] · -- time - set E := 3 * k * K * (φ.length + 1) / Nat.sqrt (Nat.log 2 (φ.numVars + 2)) + set E := F φ have h2E : 1 ≤ 2 ^ E := Nat.one_le_two_pow set Z := 2 ^ E * Y ^ e have hZ {d : ℕ} (h : d ≤ e) : Y ^ d ≤ Z := @@ -256,14 +270,11 @@ theorem exists_modelCounter (k : ℕ) : ≤ K * (p + 1) ^ K * Z := by intro hgφ obtain ⟨hne, hcl⟩ := guard_eq_true_iff.mp hgφ - have hk : ∀ c ∈ φ, c.length ≤ k := fun c hc => (hcl c hc).2 have h1 : 1 ≤ φ.length := List.length_pos_iff.mpr hne have hm := length_le_length_vars fun c hc => (hcl c hc).1 - have hNm := CNF.length_vars_le_mul_length hk - have hnN := CNF.numVars_le_length_vars φ have hb := (hK (3 * φ.vars.length) (3 * φ.vars.length) (clauseNetwork k φ) (by omega) (by omega) (by omega) (explicitAdmissible_clauseNetwork hgφ)).1 - have hexp := exponent_le (K := K) (by omega) hNm hnN + have hexp := hF φ hgφ calc fastContractionAlgorithm.certificate.time (contractionInput k φ) ≤ K * ((p + 1) ^ K * Y ^ (q * K)) * 2 ^ E := by refine hb.trans ?_ @@ -323,6 +334,45 @@ theorem exists_modelCounter (k : ℕ) : _ = (cg' + cf') * Y ^ b := by ring _ ≤ _ := hC _ (by omega) +/-- **Model counting by tensor contraction.** For each clause width `k`, one machine computes +`φ.modelCount` on every formula `φ` whose clauses have at most `k` literals, in time +`2 ^ (A (m + 1) / √⌊log₂ (n + 2)⌋)` times a polynomial in the encoding length and in polynomial +space, where `m` is the number of clauses and `n` the number of variables. -/ +theorem exists_modelCounter (k : ℕ) : + ∃ (count : CNF ℕ → ℕ) (A e b : ℕ), + (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) → count φ = φ.modelCount) ∧ + ComputableInO count encCNF encNat + (fun φ => 2 ^ (A * (φ.length + 1) / Nat.sqrt (Nat.log 2 (φ.numVars + 2))) * + ((encCNF φ).length + 1) ^ e) + (fun φ => ((encCNF φ).length + 1) ^ b) := by + obtain ⟨K, e, b, h⟩ := computableInO_count k + refine ⟨count k, 3 * k * K, e, b, fun φ hk => count_eq hk, h _ fun φ hg => ?_⟩ + obtain ⟨hne, hcl⟩ := guard_eq_true_iff.mp hg + have h1 : 1 ≤ φ.length := List.length_pos_iff.mpr hne + have hm := length_le_length_vars fun c hc => (hcl c hc).1 + exact exponent_le (by omega) (CNF.length_vars_le_mul_length fun c hc => (hcl c hc).2) + (CNF.numVars_le_length_vars φ) + +/-- **Model counting by tensor contraction, measured by literal occurrences.** For each clause +width `k`, one machine computes `φ.modelCount` on every formula `φ` whose clauses have at most `k` +literals, in time `2 ^ (A (N + 1) / √⌊log₂ (N + 2)⌋)` times a polynomial in the encoding length +and in polynomial space, where `N` is the number of literal occurrences. Unlike +`exists_modelCounter`, the exponent does not divide by the logarithm of the number of variables, +so it stays `O(N / √log N)` for formulas with many clauses on few variables. -/ +theorem exists_modelCounter_occurrences (k : ℕ) : + ∃ (count : CNF ℕ → ℕ) (A e b : ℕ), + (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) → count φ = φ.modelCount) ∧ + ComputableInO count encCNF encNat + (fun φ => 2 ^ (A * (φ.vars.length + 1) / Nat.sqrt (Nat.log 2 (φ.vars.length + 2))) * + ((encCNF φ).length + 1) ^ e) + (fun φ => ((encCNF φ).length + 1) ^ b) := by + obtain ⟨K, e, b, h⟩ := computableInO_count k + refine ⟨count k, 3 * K, e, b, fun φ hk => count_eq hk, h _ fun φ hg => ?_⟩ + obtain ⟨hne, hcl⟩ := guard_eq_true_iff.mp hg + have h1 : 1 ≤ φ.length := List.length_pos_iff.mpr hne + have hm := length_le_length_vars fun c hc => (hcl c hc).1 + exact exponent_le_occurrences (by omega) + /-- **The fixed-density bound of Theorem 1.1.** For each clause width `k`, one machine computes `φ.modelCount` on every formula `φ` whose clauses have at most `k` literals, in polynomial space, and for each density `D` its time on formulas with at most `D n` clauses, for `n` variables, is diff --git a/Complexity/Computability/Complexity/FineGrained/WideClauseCounting.lean b/Complexity/Computability/Complexity/FineGrained/WideClauseCounting.lean new file mode 100644 index 0000000000..0b544e872e --- /dev/null +++ b/Complexity/Computability/Complexity/FineGrained/WideClauseCounting.lean @@ -0,0 +1,157 @@ +/- +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.Computability.Complexity.FineGrained.ContractionCounting +import Complexity.Computability.Complexity.Problems.SharpThreeSAT +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.FunProp +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Bounds + +/-! +# Model counting by tensor contraction for unbounded clause width + +One native machine computes the number of satisfying assignments `CNF.modelCount φ` of **every** +formula `φ` in conjunctive normal form, with no bound on the width of its clauses, in time +`2 ^ (A (N + 1) / √⌊log₂ (N + 2)⌋)` times a polynomial in the encoding length and in polynomial +space, where `N` is the number of literal occurrences of `φ` (`φ.vars.length`) +(`ContractionCounting.exists_modelCounter_unboundedWidth`). For formulas with at most `D n` literal +occurrences on `n` variables this is `2 ^ O_D(n / √log n)` times a polynomial +(`ContractionCounting.exists_modelCounter_unboundedWidth_linearLength`), so sparse formulas are +counted in time `2 ^ o(n)` even when their clauses are long. + +**The machine.** It splits every clause into binary OR gates (`Cslib.Complexity.toSharpThreeSAT`, +the count-preserving split of §2.8 of [OpenAI2026ETH], p. 18). The result has clauses of at most +three literals, the same number of satisfying assignments, and between `N` and `7 N` literal +occurrences (`Cslib.Complexity.length_vars_toSharpThreeSAT`). Then it runs the contraction counter +for width three (`ContractionCounting.exists_modelCounter_occurrences`), whose exponent is +`O(N / √log N)` in the number of literal occurrences. + +After the split, every vertex of the contracted network has at most four ports and an explicit +table, so the form of Theorem D.1 with entries computed by procedures, which allows degree +`⌈s ^ (9/10)⌉`, is not needed; without a split it would not cover clauses wider than that bound +either. + +**Source relation.** Theorem 1.1 of [OpenAI2026ETH] (p. 2) is stated for `k`-CNF with fixed `k`, +in terms of the numbers of variables and clauses; its fixed-density case is proved in Appendix D.2 +(p. 54) from Theorem D.1 (p. 53). The bound here, for unbounded width and in terms of the number of +literal occurrences, combines that proof with the split of §2.8; the combination is a library +extension, not a statement of the manuscript. + +## Main results + +* `Cslib.Complexity.ContractionCounting.exists_modelCounter_unboundedWidth`: the counter for every + formula, with exponent `A (N + 1) / √⌊log₂ (N + 2)⌋`. +* `Cslib.Complexity.ContractionCounting.exists_modelCounter_unboundedWidth_linearLength`: for each + `D`, exponent `A (n + 1) / √⌊log₂ (n + 2)⌋` on formulas with at most `D n` literal occurrences. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem 1.1 (p. 2), + §2.8 (p. 18), Theorem D.1 (p. 53) and Appendix D.2 (p. 54). +-/ + +public section + +namespace Cslib.Complexity.ContractionCounting + +open Cslib.Logic.PL Turing.MultiTapeTM + +/-- The exponent after splitting: between `N` and `7 N` literal occurrences, the exponent +`A (N' + 1) / √⌊log₂ (N' + 2)⌋` is at most `7 A (N + 1) / √⌊log₂ (N + 2)⌋`. -/ +private theorem exponent_le_of_le {A N N' : ℕ} (h₁ : N ≤ N') (h₂ : N' ≤ 7 * N) : + A * (N' + 1) / Nat.sqrt (Nat.log 2 (N' + 2)) ≤ + 7 * A * (N + 1) / Nat.sqrt (Nat.log 2 (N + 2)) := by + refine Nat.div_le_div ?_ (Nat.sqrt_le_sqrt (Nat.log_mono_right (by omega))) ?_ + · have : A * (N' + 1) ≤ A * (7 * (N + 1)) := Nat.mul_le_mul_left _ (by omega) + nlinarith + · exact Nat.sqrt_eq_zero.not.mpr (Nat.log_pos (by norm_num) (by omega)).ne' + +/-- **Model counting by tensor contraction for unbounded clause width.** One machine computes +`φ.modelCount` on every formula `φ`, in time `2 ^ (A (N + 1) / √⌊log₂ (N + 2)⌋)` times a +polynomial in the encoding length and in polynomial space, where `N` is the number of literal +occurrences of `φ`. -/ +theorem exists_modelCounter_unboundedWidth : + ∃ (count : CNF ℕ → ℕ) (A e b : ℕ), + (∀ φ : CNF ℕ, count φ = φ.modelCount) ∧ + ComputableInO count encCNF encNat + (fun φ => 2 ^ (A * (φ.vars.length + 1) / Nat.sqrt (Nat.log 2 (φ.vars.length + 2))) * + ((encCNF φ).length + 1) ^ e) + (fun φ => ((encCNF φ).length + 1) ^ b) := by + obtain ⟨count, A, e, b, hcount, hc⟩ := exists_modelCounter_occurrences 3 + obtain ⟨d, _, hdeg⟩ := computableInPolyTime_toSharpThreeSAT.exists_degree + obtain ⟨p, q, hlen⟩ := computableInPolyTime_toSharpThreeSAT.polyBounded_length.exists_le + refine ⟨fun φ => count (toSharpThreeSAT φ), 7 * A, d + q * e, d + q * b, + fun φ => (hcount _ fun _ hc => length_le_three_of_mem_toSharpThreeSAT hc).trans + (modelCount_toSharpThreeSAT φ), + (hc.comp' hdeg.inO).mono ((p + 1) ^ e + (p + 1) ^ b + 1) (fun φ => ?_) (fun φ => ?_)⟩ + all_goals + obtain ⟨Y, hY⟩ : ∃ Y, Y = (encCNF φ).length + 1 := ⟨_, rfl⟩ + have hY1 : 1 ≤ Y := by omega + have hψ : (encCNF (toSharpThreeSAT φ)).length + 1 ≤ (p + 1) * Y ^ q := by + have h1 : (encCNF (toSharpThreeSAT φ)).length ≤ p * Y ^ q := by rw [hY]; exact hlen φ + have h2 : 1 ≤ Y ^ q := Nat.one_le_pow _ _ hY1 + nlinarith + have hψpow (c : ℕ) : ((encCNF (toSharpThreeSAT φ)).length + 1) ^ c ≤ + (p + 1) ^ c * Y ^ (q * c) := by + calc _ ≤ ((p + 1) * Y ^ q) ^ c := Nat.pow_le_pow_left hψ c + _ = _ := by rw [mul_pow, pow_mul] + simp only [← hY] + · -- time + obtain ⟨E, hE⟩ : ∃ E, E = 7 * A * (φ.vars.length + 1) / Nat.sqrt (Nat.log 2 + (φ.vars.length + 2)) := ⟨_, rfl⟩ + rw [← hE] + obtain ⟨hN₁, hN₂⟩ := length_vars_toSharpThreeSAT φ + have hexp := hE ▸ exponent_le_of_le (A := A) hN₁ hN₂ + have h2E : 1 ≤ 2 ^ E := Nat.one_le_two_pow + have hd : Y ^ d ≤ 2 ^ E * Y ^ (d + q * e) := + (Nat.pow_le_pow_right hY1 (by omega)).trans (Nat.le_mul_of_pos_left _ h2E) + have hc' : 2 ^ (A * ((toSharpThreeSAT φ).vars.length + 1) / + Nat.sqrt (Nat.log 2 ((toSharpThreeSAT φ).vars.length + 2))) * + ((encCNF (toSharpThreeSAT φ)).length + 1) ^ e ≤ + (p + 1) ^ e * (2 ^ E * Y ^ (d + q * e)) := + calc _ ≤ 2 ^ E * ((p + 1) ^ e * Y ^ (q * e)) := + Nat.mul_le_mul (Nat.pow_le_pow_right (by norm_num) hexp) (hψpow e) + _ ≤ 2 ^ E * ((p + 1) ^ e * Y ^ (d + q * e)) := + Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hY1 (by omega))) + _ = (p + 1) ^ e * (2 ^ E * Y ^ (d + q * e)) := by ring + calc _ ≤ 2 ^ E * Y ^ (d + q * e) + (p + 1) ^ e * (2 ^ E * Y ^ (d + q * e)) := + Nat.add_le_add hd hc' + _ = (1 + (p + 1) ^ e) * (2 ^ E * Y ^ (d + q * e)) := by ring + _ ≤ _ := Nat.mul_le_mul (by omega) (Nat.le_succ _) + · -- space + have hd : Y ^ d ≤ Y ^ (d + q * b) := Nat.pow_le_pow_right hY1 (by omega) + have hb : ((encCNF (toSharpThreeSAT φ)).length + 1) ^ b ≤ (p + 1) ^ b * Y ^ (d + q * b) := + (hψpow b).trans (Nat.mul_le_mul_left _ (Nat.pow_le_pow_right hY1 (by omega))) + calc _ ≤ Y ^ (d + q * b) + (p + 1) ^ b * Y ^ (d + q * b) := Nat.add_le_add hd hb + _ = (1 + (p + 1) ^ b) * Y ^ (d + q * b) := by ring + _ ≤ _ := Nat.mul_le_mul (by omega) (Nat.le_succ _) + +/-- **Linearly many literal occurrences.** One machine computes `φ.modelCount` on every formula +`φ`, in polynomial space, and for each `D` its time on formulas with at most `D n` literal +occurrences, for `n` variables, is `2 ^ (A (n + 1) / √⌊log₂ (n + 2)⌋)` times a polynomial in the +encoding length. The machine, its time and space functions and the degree `e` of the polynomial +are fixed before `D`; only `A` depends on `D`. -/ +theorem exists_modelCounter_unboundedWidth_linearLength : + ∃ (count : CNF ℕ → ℕ) (T S : CNF ℕ → ℕ) (e b : ℕ), + (∀ φ : CNF ℕ, count φ = φ.modelCount) ∧ + ComputableInO count encCNF encNat T S ∧ + (∀ φ, S φ = ((encCNF φ).length + 1) ^ b) ∧ + ∀ D : ℕ, ∃ A : ℕ, ∀ φ : CNF ℕ, φ.vars.length ≤ D * φ.numVars → + T φ ≤ 2 ^ (A * (φ.numVars + 1) / Nat.sqrt (Nat.log 2 (φ.numVars + 2))) * + ((encCNF φ).length + 1) ^ e := by + obtain ⟨count, A, e, b, hcount, hc⟩ := exists_modelCounter_unboundedWidth + refine ⟨count, _, _, e, b, hcount, hc, fun _ => rfl, fun D => ⟨A * (D + 1), fun φ hφ => ?_⟩⟩ + refine Nat.mul_le_mul_right _ (Nat.pow_le_pow_right (by norm_num) ?_) + have hn := CNF.numVars_le_length_vars φ + refine Nat.div_le_div ?_ (Nat.sqrt_le_sqrt (Nat.log_mono_right (by omega))) + (Nat.sqrt_eq_zero.not.mpr (Nat.log_pos (by norm_num) (by omega)).ne') + have : φ.vars.length + 1 ≤ (D + 1) * (φ.numVars + 1) := by nlinarith + calc A * (φ.vars.length + 1) ≤ A * ((D + 1) * (φ.numVars + 1)) := Nat.mul_le_mul_left _ this + _ = A * (D + 1) * (φ.numVars + 1) := by ring + +end Cslib.Complexity.ContractionCounting diff --git a/Complexity/Computability/Complexity/Problems/SharpThreeSAT.lean b/Complexity/Computability/Complexity/Problems/SharpThreeSAT.lean index f8aa3372eb..c6a41a42c5 100644 --- a/Complexity/Computability/Complexity/Problems/SharpThreeSAT.lean +++ b/Complexity/Computability/Complexity/Problems/SharpThreeSAT.lean @@ -40,6 +40,10 @@ parsimonious reduction to `#SAT ∈ #P`. ## Main results +* `Cslib.Complexity.length_le_three_of_mem_toSharpThreeSAT`, + `Cslib.Complexity.modelCount_toSharpThreeSAT`, `Cslib.Complexity.length_vars_toSharpThreeSAT`: + the reduction has width three, preserves model counts and at most multiplies the number of + literal occurrences by seven. * `Cslib.Complexity.sharpThreeSAT_toSharpThreeSAT`: the reduction preserves counts. * `Cslib.Complexity.computableInPolyTime_toSharpThreeSAT`: it is polynomial-time. * `Cslib.Complexity.parsimoniousReducible_SharpSAT_SharpThreeSAT`: `#SAT` reduces @@ -63,16 +67,31 @@ open Cslib.Logic.PL Turing.MultiTapeTM number the original and gate variables injectively. -/ def toSharpThreeSAT (φ : CNF ℕ) : CNF ℕ := φ.toExact3CNF.relabel splitVarToNat +/-- Every clause of `toSharpThreeSAT φ` has at most three literals. -/ +theorem length_le_three_of_mem_toSharpThreeSAT {φ : CNF ℕ} {c : Clause ℕ} + (hc : c ∈ toSharpThreeSAT φ) : c.length ≤ 3 := by + obtain ⟨d, hd, rfl⟩ := List.mem_map.1 hc + simpa using CNF.length_le_three_of_mem_toExact3CNF hd + +/-- `toSharpThreeSAT` preserves the number of satisfying assignments. -/ +theorem modelCount_toSharpThreeSAT (φ : CNF ℕ) : + (toSharpThreeSAT φ).modelCount = φ.modelCount := by + rw [toSharpThreeSAT, CNF.modelCount_relabel splitVarToNat_injective, CNF.modelCount_toExact3CNF] + +/-- `toSharpThreeSAT φ` has between one and seven times as many literal occurrences as `φ`. -/ +theorem length_vars_toSharpThreeSAT (φ : CNF ℕ) : + φ.vars.length ≤ (toSharpThreeSAT φ).vars.length ∧ + (toSharpThreeSAT φ).vars.length ≤ 7 * φ.vars.length := by + rw [toSharpThreeSAT, CNF.vars_relabel, List.length_map] + exact ⟨CNF.length_vars_le_length_vars_toExact3CNF φ, CNF.length_vars_toExact3CNF_le φ⟩ + /-- `toSharpThreeSAT` has width at most three and the same number of satisfying assignments. -/ theorem sharpThreeSAT_toSharpThreeSAT (φ : CNF ℕ) : SharpThreeSAT (toSharpThreeSAT φ) = SharpSAT φ := by have hw : ((toSharpThreeSAT φ).all fun c => decide (c.length ≤ 3)) = true := by - simp only [List.all_eq_true, decide_eq_true_eq, toSharpThreeSAT, CNF.relabel, List.mem_map] - rintro _ ⟨c, hc, rfl⟩ - simpa using CNF.length_le_three_of_mem_toExact3CNF hc - simp only [SharpThreeSAT, hw, ↓reduceIte] - simp only [SharpSAT, toSharpThreeSAT, CNF.modelCount_relabel splitVarToNat_injective, - CNF.modelCount_toExact3CNF] + simp only [List.all_eq_true, decide_eq_true_eq] + exact fun c hc => length_le_three_of_mem_toSharpThreeSAT hc + simp only [SharpThreeSAT, hw, ↓reduceIte, SharpSAT, modelCount_toSharpThreeSAT] /-- The reduction `toSharpThreeSAT` is computable in polynomial time under `encCNF`. -/ @[fun_prop] diff --git a/Complexity/Logics/Propositional/CNF/ThreeCNF/Exact.lean b/Complexity/Logics/Propositional/CNF/ThreeCNF/Exact.lean index 4c4e5a3cd6..d657f6eb33 100644 --- a/Complexity/Logics/Propositional/CNF/ThreeCNF/Exact.lean +++ b/Complexity/Logics/Propositional/CNF/ThreeCNF/Exact.lean @@ -50,8 +50,9 @@ times. assignments. * `Cslib.Logic.PL.CNF.satisfiable_toExact3CNF`: hence it preserves satisfiability. * `Cslib.Logic.PL.CNF.length_toExact3CNF`, `Cslib.Logic.PL.CNF.length_vars_toExact3CNF`, - `Cslib.Logic.PL.CNF.length_vars_toExact3CNF_le`: the size, linear in the number of literal - occurrences. + `Cslib.Logic.PL.CNF.length_vars_toExact3CNF_le`, + `Cslib.Logic.PL.CNF.length_vars_le_length_vars_toExact3CNF`: the size, between one and seven + times the number of literal occurrences. ## References @@ -470,4 +471,10 @@ theorem CNF.length_vars_toExact3CNF_le (φ : CNF V) : rw [CNF.length_vars_toExact3CNF, CNF.length_vars, ← List.sum_map_mul_left] exact List.sum_le_sum fun c _ => by omega +/-- Splitting keeps every literal occurrence. -/ +theorem CNF.length_vars_le_length_vars_toExact3CNF (φ : CNF V) : + φ.vars.length ≤ φ.toExact3CNF.vars.length := by + rw [CNF.length_vars_toExact3CNF, CNF.length_vars] + exact List.sum_le_sum fun c _ => by omega + end Cslib.Logic.PL diff --git a/ComplexityTests/WideClauseCounting.lean b/ComplexityTests/WideClauseCounting.lean new file mode 100644 index 0000000000..d92a06ad0d --- /dev/null +++ b/ComplexityTests/WideClauseCounting.lean @@ -0,0 +1,56 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.Complexity.FineGrained.WideClauseCounting +import Complexity.Computability.Complexity.Problems.SharpThreeSAT + +/-! # Model counting for unbounded clause width: checked instances + +A formula with a clause of width six, its count-preserving split into width three, and the +counter of `ContractionCounting.exists_modelCounter_unboundedWidth` evaluated on it. -/ + +namespace ComplexityTests.WideClauseCounting + +open Cslib.Logic.PL Cslib.Complexity Cslib.Complexity.ContractionCounting + +/-- `(x₀ ∨ x₁ ∨ x₂ ∨ x₃ ∨ x₄ ∨ x₅) ∧ (¬x₀ ∨ x₆)`: a clause of width six, eight literal occurrences +and seven variables. -/ +def φ₁ : CNF ℕ := + [[(0, true), (1, true), (2, true), (3, true), (4, true), (5, true)], [(0, false), (6, true)]] + +/-- Of the `2 ^ 7` assignments, two falsify the wide clause (`x₀ = ⋯ = x₅ = false`) and `2 ^ 5` +falsify the second (`x₀ = true`, `x₆ = false`); no assignment falsifies both. -/ +theorem modelCount_φ₁ : φ₁.modelCount = 94 := by decide + +example : φ₁.vars.length = 8 ∧ φ₁.numVars = 7 := by decide + +-- The split: width three, `6 + 6 · 3 + 2 = 26 ≤ 7 · 8` literal occurrences, the same count. +example : (toSharpThreeSAT φ₁).all (fun c => decide (c.length ≤ 3)) = true := by decide + +example : (toSharpThreeSAT φ₁).vars.length = 26 := by decide + +example : (toSharpThreeSAT φ₁).modelCount = 94 := by + rw [modelCount_toSharpThreeSAT, modelCount_φ₁] + +-- The counter for every width counts `φ₁`. +example : ∃ (count : CNF ℕ → ℕ) (A e b : ℕ), count φ₁ = 94 ∧ + Turing.MultiTapeTM.ComputableInO count encCNF Turing.MultiTapeTM.encNat + (fun φ => 2 ^ (A * (φ.vars.length + 1) / Nat.sqrt (Nat.log 2 (φ.vars.length + 2))) * + ((encCNF φ).length + 1) ^ e) + (fun φ => ((encCNF φ).length + 1) ^ b) := by + obtain ⟨count, A, e, b, hcount, hc⟩ := exists_modelCounter_unboundedWidth + exact ⟨count, A, e, b, (hcount φ₁).trans modelCount_φ₁, hc⟩ + +-- `φ₁` meets the linear-length hypothesis `N ≤ D n` with `D = 2`, although its widest clause has +-- six literals; formulas with many occurrences of few variables do not. +example : φ₁.vars.length ≤ 2 * φ₁.numVars := by decide + +/-- `x₀ ∧ x₀ ∧ x₀`: three occurrences of one variable. -/ +def φ₂ : CNF ℕ := [[(0, true)], [(0, true)], [(0, true)]] + +example : ¬ φ₂.vars.length ≤ 2 * φ₂.numVars := by decide + +end ComplexityTests.WideClauseCounting