From cdd9f296ca3ef3283107d9ef268605b4108494c5 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 08:29:46 -0400 Subject: [PATCH 1/4] feat(FineGrained): fixed-density #k-SAT counting by tensor contraction (Theorem 1.1, D.2) The clause network of a CNF (one row vertex per clause, an equality chain per variable subdivided by link vertices) has contraction equal to the model count, is rows-first bipartite with degree at most max k 4, and is built in polynomial time. Contracting it with the Theorem D.1 algorithm gives, for each clause width k, one machine counting models in time 2^(A(m+1)/sqrt(floor(log2(n+2)))) times a polynomial and polynomial space; for m <= Dn this is Theorem 1.1's fixed-density bound 2^O_{k,D}(n/sqrt(log n)). The arbitrary-density bound (Appendix D.3, truncation order l = n + 1) remains open. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 3 + .../Frontier/TensorNetwork/ClauseNetwork.lean | 823 ++++++++++++++++++ .../TensorNetwork/ClauseNetworkPolyTime.lean | 213 +++++ .../FineGrained/ContractionCounting.lean | 353 ++++++++ ComplexityTests/ContractionCounting.lean | 65 ++ 5 files changed, 1457 insertions(+) create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetwork.lean create mode 100644 Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetworkPolyTime.lean create mode 100644 Complexity/Computability/Complexity/FineGrained/ContractionCounting.lean create mode 100644 ComplexityTests/ContractionCounting.lean diff --git a/Complexity.lean b/Complexity.lean index 7404b542b3..fd66ede951 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -929,6 +929,8 @@ public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildCurso public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildEntries public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildNumbering public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ChildSize +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ClauseNetwork +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.ClauseNetworkPolyTime public import Complexity.Computability.Circuit.Frontier.TensorNetwork.CoeffScheme public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Constraint public import Complexity.Computability.Circuit.Frontier.TensorNetwork.Deformation @@ -1380,6 +1382,7 @@ 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.CircuitCounting +public import Complexity.Computability.Complexity.FineGrained.ContractionCounting public import Complexity.Computability.Complexity.FineGrained.CountingCSP public import Complexity.Computability.Complexity.FineGrained.CountingEndpoint public import Complexity.Computability.Complexity.FineGrained.CountingFiniteCSP diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetwork.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetwork.lean new file mode 100644 index 0000000000..61008dd754 --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetwork.lean @@ -0,0 +1,823 @@ +/- +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.Circuit.Frontier.TensorNetwork.Explicit +public import Complexity.Logics.Propositional.CNF.ModelCount +import Mathlib.Data.List.GetD + +/-! +# The clause network of a CNF formula + +The explicit Boolean tensor network of the fixed-density case of Theorem 1.1 of [OpenAI2026ETH] +(Appendix D.2): its contraction is the number of satisfying assignments of the formula, it is +bipartite with its rows first, and its degree is bounded by the clause width. + +Number the literal occurrences of a formula `φ` with `m` clauses `0, …, N - 1` in order +(`Cslib.Logic.PL.occurrences`). Occurrence `u` has three edges, `3 u`, `3 u + 1` and `3 u + 2`. + +* **Rows.** Clause `i` is a vertex whose ports are the edges `3 u` of its occurrences `u`; its + tensor is one except at the single assignment that falsifies every literal of the clause + (`ClauseNetwork.clauseEntry`). Occurrence `u` has a *link* vertex with the two ports `3 u + 1` + and `3 u + 2` and the equality tensor. +* **Columns.** Occurrence `u` has an *equality* vertex with the ports `3 u` and `3 u + 1`, and + `3 w + 2` for every occurrence `w` whose previous occurrence of the same variable is `u` + (`ClauseNetwork.prev`, which is `w` itself at a first occurrence). Its tensor is equality + (`ClauseNetwork.eqEntry`). + +So the occurrences of a variable form a chain of equality vertices, subdivided by the link +vertices, and every edge joins a row to a column. An assignment of the edges has weight one +exactly when the three edges of every occurrence carry the value of its variable and every clause +has a true literal, so the contraction is the model count +(`ClauseNetwork.contraction_clauseNetwork`). +This is the network of Appendix D.2 with equality chains in place of equality trees: its +equality vertices have degree at most four (`ClauseNetwork.length_qPorts_le`), which is all that +Theorem D.1 needs, and the subdivision is built in. It does not merge repeated variables of a +clause; their edges are joined by the chain. + +The tables are listed from the first `2 ^ B` numbers (`ClauseNetwork.boundedTable`), for a bound +`B` on the degrees, so that the network is computed from constant-length lists; for the clause +network of width `k` formulas, `B = max k 4` (`ClauseNetwork.clauseNetwork`). + +## Main definitions + +* `Cslib.Circuits.Frontier.ClauseNetwork.prev`: the previous occurrence of the same variable. +* `Cslib.Circuits.Frontier.ClauseNetwork.clausePorts`, + `Cslib.Circuits.Frontier.ClauseNetwork.qPorts`: the ports of the clause and equality vertices. +* `Cslib.Circuits.Frontier.ClauseNetwork.network`: the network of an occurrence list. +* `Cslib.Circuits.Frontier.ClauseNetwork.clauseNetwork`: the clause network of a formula, with + its number of rows. + +## Main results + +* `Cslib.Circuits.Frontier.ClauseNetwork.count_map_fst_occurrences`: a clause has as many + occurrences as literals. +* `Cslib.Circuits.Frontier.ClauseNetwork.contraction_clauseNetwork`: the contraction is the model + count. +* `Cslib.Circuits.Frontier.ClauseNetwork.isRowsFirstBipartite_clauseNetwork`: the bipartition. +* `Cslib.Circuits.Frontier.ClauseNetwork.maxDegree_clauseNetwork_le`: degree at most `max k 4`. +* `Cslib.Circuits.Frontier.ClauseNetwork.numEdges_clauseNetwork`, + `Cslib.Circuits.Frontier.ClauseNetwork.length_vertices_clauseNetwork`, + `Cslib.Circuits.Frontier.ClauseNetwork.length_table_clauseNetwork`: its size and full tables. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Appendix D.2 (p. 54). +-/ + +public section + +namespace Cslib.Circuits.Frontier.ClauseNetwork + +open Cslib.Logic.PL + +/-! ### Occurrences -/ + +private theorem count_map_fst_flatMap_zipIdx (φ : CNF ℕ) (s i : ℕ) : + (((φ.zipIdx s).flatMap fun c => c.1.zipIdx.map fun l => (c.2, l.2, l.1)).map Prod.fst).count + i = if s ≤ i then (φ.getD (i - s) []).length else 0 := by + induction φ generalizing s with + | nil => simp + | cons c φ ih => + simp only [List.zipIdx_cons, List.flatMap_cons, List.map_append, List.map_map, + List.count_append, ih] + have hc : (c.zipIdx.map (Prod.fst ∘ fun l => (s, l.2, l.1))).count i = + if i = s then c.length else 0 := by + simp only [Function.comp_def, List.map_const', List.count_replicate, List.length_zipIdx] + split_ifs <;> simp_all + rw [hc] + by_cases his : i = s + · subst his + simp + · by_cases hsi : s ≤ i + · have he : i - s = (i - (s + 1)) + 1 := by omega + simp [his, hsi, show s + 1 ≤ i by omega, he] + · simp [his, hsi, show ¬s + 1 ≤ i by omega] + +/-- Clause `i` has as many occurrences as literals. -/ +theorem count_map_fst_occurrences (φ : CNF ℕ) (i : ℕ) : + ((occurrences φ).map Prod.fst).count i = (φ.getD i []).length := by + have h := count_map_fst_flatMap_zipIdx φ 0 i + simp only [Nat.zero_le, ite_true, Nat.sub_zero] at h + exact h + +/-! ### Occurrence data -/ + +variable (os : List (Occurrence ℕ)) + +/-- Occurrence `u`: its clause, its position in the clause and its literal, with a default past the +end. -/ +@[expose] def occ (u : ℕ) : Occurrence ℕ := os.getD u (0, 0, (0, false)) + +/-- The variable of occurrence `u`. -/ +@[expose] def var (u : ℕ) : ℕ := (occ os u).2.2.1 + +/-- The polarity of occurrence `u`. -/ +@[expose] def pol (u : ℕ) : Bool := (occ os u).2.2.2 + +/-- The clause of occurrence `u`. -/ +@[expose] def clauseOf (u : ℕ) : ℕ := (occ os u).1 + +/-- The previous occurrence of the variable of occurrence `u`, or `u` itself if there is none. -/ +@[expose] def prev (u : ℕ) : ℕ := + ((List.range u).reverse.find? fun w => decide (var os w = var os u)).getD u + +/-! ### The network -/ + +/-- A table of the `2 ^ w` values `f 0, …, f (2 ^ w - 1)` when `w ≤ B`, listed by keeping the +numbers below `2 ^ w` among the first `2 ^ B`. -/ +@[expose] def boundedTable (B w : ℕ) (f : ℕ → ℕ) : List ℕ := + ((List.range (2 ^ B)).filter fun idx => idx < 2 ^ w).map f + +/-- The equality tensor on `w` ports: one at the all-`false` and the all-`true` words. -/ +@[expose] def eqEntry (w idx : ℕ) : ℕ := if idx = 0 ∨ idx + 1 = 2 ^ w then 1 else 0 + +/-- The clause tensor: zero at the one word `z` that falsifies every literal, one elsewhere. -/ +@[expose] def clauseEntry (z idx : ℕ) : ℕ := if idx = z then 0 else 1 + +/-- The ports of clause `i`: the edges `3 u` of its occurrences `u`. -/ +@[expose] def clausePorts (i : ℕ) : List ℕ := + ((List.range os.length).filter fun u => clauseOf os u = i).map fun u => 3 * u + +/-- The ports of the equality vertex of occurrence `w`: `3 w`, `3 w + 1`, and `3 u + 2` for the +occurrences `u` whose previous occurrence is `w`. -/ +@[expose] def qPorts (w : ℕ) : List ℕ := + [3 * w, 3 * w + 1] ++ + ((List.range os.length).filter fun u => prev os u = w).map fun u => 3 * u + 2 + +/-- The falsifying word of a clause vertex with the ports `ps`, as a number. -/ +@[expose] def falsifier (ps : List ℕ) : ℕ := BitString.lsbValue (ps.map fun j => !pol os (j / 3)) + +/-- The clause vertex `i`. -/ +@[expose] def clauseVertex (B i : ℕ) : List ℕ × List ℕ := + (clausePorts os i, + boundedTable B (clausePorts os i).length (clauseEntry (falsifier os (clausePorts os i)))) + +/-- The link vertex of occurrence `u`. -/ +@[expose] def linkVertex (u : ℕ) : List ℕ × List ℕ := ([3 * u + 1, 3 * u + 2], [1, 0, 0, 1]) + +/-- The equality vertex of occurrence `w`. -/ +@[expose] def qVertex (B w : ℕ) : List ℕ × List ℕ := + (qPorts os w, boundedTable B (qPorts os w).length (eqEntry (qPorts os w).length)) + +/-- **The network of an occurrence list** with `m` clauses and degree bound `B`, with its number +of rows `m + N`: the clause vertices, the link vertices, and then the equality vertices. -/ +@[expose] def network (B m : ℕ) : ℕ × ExplicitTensorNetwork ℕ := + (m + os.length, ⟨3 * os.length, + (List.range m).map (clauseVertex os B) ++ (List.range os.length).map linkVertex ++ + (List.range os.length).map (qVertex os B)⟩) + +/-- **The clause network** of a formula, for clause width at most `k`. -/ +@[expose] def clauseNetwork (k : ℕ) (φ : CNF ℕ) : ℕ × ExplicitTensorNetwork ℕ := + network (occurrences φ) (max k 4) φ.length + +/-! ### The occurrence data -/ + +theorem occ_eq_getElem {u : ℕ} (hu : u < os.length) : occ os u = os[u] := + List.getD_eq_getElem _ _ hu + +/-- Listing the occurrences by number gives the occurrence list back. -/ +theorem map_occ_range : (List.range os.length).map (occ os) = os := by + refine List.ext_getElem (by simp) fun u h₁ h₂ => ?_ + simp only [List.getElem_map, List.getElem_range] + exact occ_eq_getElem os h₂ + +/-- The occurrence with a given number, as a member of the list. -/ +theorem occ_mem {u : ℕ} (hu : u < os.length) : occ os u ∈ os := by + rw [occ_eq_getElem os hu] + exact List.getElem_mem hu + +/-- **The previous occurrence.** Either `prev u < u` is an occurrence of the same variable with no +occurrence of that variable strictly between, or `u` is the first occurrence of its variable. -/ +theorem prev_spec (u : ℕ) : + (prev os u < u ∧ var os (prev os u) = var os u ∧ + ∀ w, prev os u < w → w < u → var os w ≠ var os u) ∨ + (prev os u = u ∧ ∀ w < u, var os w ≠ var os u) := by + unfold prev + cases h : (List.range u).reverse.find? fun w => decide (var os w = var os u) with + | none => + right + simp only [Option.getD_none] + refine ⟨by simp, fun w hw => ?_⟩ + have := List.find?_eq_none.mp h w (by simpa using hw) + simpa using this + | some b => + left + simp only [Option.getD_some] + obtain ⟨hb, as, bs, hl, has⟩ := List.find?_eq_some_iff_append.mp h + have hbmem : b ∈ (List.range u).reverse := by rw [hl]; simp + have hbu : b < u := by simpa using hbmem + refine ⟨hbu, by simpa using hb, fun w hbw hwu => ?_⟩ + have hwmem : w ∈ as ++ b :: bs := by rw [← hl]; simpa using hwu + have hpw : List.Pairwise (fun x y => y < x) (as ++ b :: bs) := by + rw [← hl, List.pairwise_reverse] + exact List.pairwise_lt_range + rcases List.mem_append.mp hwmem with hw | hw + · simpa using has w hw + · rcases List.mem_cons.mp hw with rfl | hw + · omega + · have := ((List.pairwise_append.mp hpw).2.1) + have := (List.pairwise_cons.mp this).1 w hw + omega + +theorem prev_le (u : ℕ) : prev os u ≤ u := by + rcases prev_spec os u with ⟨h, -⟩ | ⟨h, -⟩ <;> omega + +theorem var_prev (u : ℕ) : var os (prev os u) = var os u := by + rcases prev_spec os u with ⟨-, h, -⟩ | ⟨h, -⟩ + · exact h + · rw [h] + +/-- Two occurrences `u < u'` whose previous occurrence is the same `w` include `w` itself. -/ +theorem eq_of_prev_eq {w u u' : ℕ} (hu : prev os u = w) (hu' : prev os u' = w) (hne : u ≠ w) + (hne' : u' ≠ w) : u = u' := by + have key : ∀ a b, prev os a = w → prev os b = w → a ≠ w → b ≠ w → a < b → False := by + intro a b ha hb haw hbw hab + rcases prev_spec os a with ⟨ha1, ha2, -⟩ | ⟨ha1, -⟩ + · rcases prev_spec os b with ⟨hb1, hb2, hb3⟩ | ⟨hb1, -⟩ + · exact hb3 a (by omega) hab (by rw [← ha2, ← hb2, ha, hb]) + · omega + · omega + rcases lt_trichotomy u u' with h | h | h + · exact (key u u' hu hu' hne hne' h).elim + · exact h + · exact (key u' u hu' hu hne' hne h).elim + +/-! ### Tables -/ + +/-- For `w ≤ B`, the bounded table is the table of `f` on `0, …, 2 ^ w - 1`. -/ +theorem boundedTable_eq {B w : ℕ} (f : ℕ → ℕ) (h : w ≤ B) : + boundedTable B w f = (List.range (2 ^ w)).map f := by + have hle : 2 ^ w ≤ 2 ^ B := Nat.pow_le_pow_right (by norm_num) h + unfold boundedTable + congr 1 + obtain ⟨c, hc⟩ := Nat.exists_eq_add_of_le hle + rw [hc, List.range_add, List.filter_append, List.filter_eq_self.mpr (by simp), + List.filter_eq_nil_iff.mpr (by simp), List.append_nil] + +theorem length_boundedTable {B w : ℕ} (f : ℕ → ℕ) (h : w ≤ B) : + (boundedTable B w f).length = 2 ^ w := by + simp [boundedTable_eq f h] + +/-- Looking up a bounded table at a word of length at most `B` evaluates its function at the +value of the word. -/ +theorem entry_boundedTable {B : ℕ} (f : ℕ → ℕ) {bs : List Bool} (h : bs.length ≤ B) : + ExplicitTensorNetwork.entry (boundedTable B bs.length f) bs = f (BitString.lsbValue bs) := by + rw [ExplicitTensorNetwork.entry, boundedTable_eq f h, + List.getD_eq_getElem _ _ (by simpa using BitString.lsbValue_lt bs)] + simp + +private theorem eq_replicate_or_iff (bs : List Bool) : + (bs = List.replicate bs.length false ∨ bs = List.replicate bs.length true) ↔ + ∀ a ∈ bs, ∀ b ∈ bs, a = b := by + constructor + · rintro (h | h) a ha b hb <;> rw [h] at ha hb <;> + rw [List.eq_of_mem_replicate ha, List.eq_of_mem_replicate hb] + · intro h + cases bs with + | nil => simp + | cons a bs => + have hall : ∀ b ∈ a :: bs, b = a := fun b hb => h b hb a List.mem_cons_self + cases a + · exact Or.inl (List.eq_replicate_iff.mpr ⟨rfl, hall⟩) + · exact Or.inr (List.eq_replicate_iff.mpr ⟨rfl, hall⟩) + +/-- The equality tensor at a word: one exactly when all its bits are equal. -/ +theorem eqEntry_lsbValue (bs : List Bool) : + eqEntry bs.length (BitString.lsbValue bs) = if ∀ a ∈ bs, ∀ b ∈ bs, a = b then 1 else 0 := by + have h0 : BitString.lsbValue bs = 0 ↔ bs = List.replicate bs.length false := by + constructor + · intro h + exact BitString.lsbValue_injective (by simp) (by simp [h]) + · intro h + rw [h, BitString.lsbValue_replicate_false] + have h1 : BitString.lsbValue bs + 1 = 2 ^ bs.length ↔ bs = List.replicate bs.length true := by + have hr := BitString.lsbValue_replicate_true bs.length + constructor + · intro h + exact BitString.lsbValue_injective (by simp) (by omega) + · intro h + rw [h] + simpa using hr + unfold eqEntry + simp only [h0, h1, eq_replicate_or_iff] + +/-- The clause tensor at a word of the length of its falsifying word: zero exactly at that +word. -/ +theorem clauseEntry_lsbValue {bs zs : List Bool} (h : bs.length = zs.length) : + clauseEntry (BitString.lsbValue zs) (BitString.lsbValue bs) = if bs = zs then 0 else 1 := by + unfold clauseEntry + congr 1 + exact propext ⟨BitString.lsbValue_injective h, fun h => h ▸ rfl⟩ + +/-! ### Ports -/ + +variable {os} + +theorem mem_clausePorts {i j : ℕ} : + j ∈ clausePorts os i ↔ ∃ u < os.length, clauseOf os u = i ∧ 3 * u = j := by + simp [clausePorts, and_assoc] + +theorem nodup_clausePorts (i : ℕ) : (clausePorts os i).Nodup := + (List.nodup_range.filter _).map fun _ _ h => by omega + +theorem mem_qPorts {w j : ℕ} : + j ∈ qPorts os w ↔ + j = 3 * w ∨ j = 3 * w + 1 ∨ ∃ u < os.length, prev os u = w ∧ 3 * u + 2 = j := by + simp [qPorts, and_assoc] + +theorem nodup_qPorts (w : ℕ) : (qPorts os w).Nodup := by + unfold qPorts + refine List.Nodup.append (by simp) ((List.nodup_range.filter _).map fun _ _ h => by omega) ?_ + intro a ha hb + simp only [List.mem_cons, List.not_mem_nil, or_false] at ha + obtain ⟨u, -, rfl⟩ := List.mem_map.mp hb + omega + +/-- The number of ports of clause `i` is its number of occurrences. -/ +theorem length_clausePorts (i : ℕ) : + (clausePorts os i).length = (os.map Prod.fst).count i := by + rw [clausePorts, List.length_map, ← List.countP_eq_length_filter, List.count] + conv_rhs => rw [← map_occ_range os] + rw [List.map_map, List.countP_map] + congr 1 + +/-- An equality vertex has at most four ports. -/ +theorem length_qPorts_le (w : ℕ) : (qPorts os w).length ≤ 4 := by + classical + have hnd : ((List.range os.length).filter fun u => prev os u = w).Nodup := + List.nodup_range.filter _ + set l := (List.range os.length).filter fun u => prev os u = w + have hsplit : l.toFinset ⊆ {w} ∪ (l.toFinset.filter fun u => u ≠ w) := by + intro u hu + by_cases h : u = w + · simp [h] + · simp [hu, h] + have hcard : (l.toFinset.filter fun u => u ≠ w).card ≤ 1 := by + refine Finset.card_le_one.mpr fun a ha b hb => ?_ + simp only [Finset.mem_filter, List.mem_toFinset, l, List.mem_filter, List.mem_range, + decide_eq_true_eq] at ha hb + exact eq_of_prev_eq os ha.1.2 hb.1.2 ha.2 hb.2 + have hl : l.length ≤ 2 := by + rw [← List.toFinset_card_of_nodup hnd] + calc l.toFinset.card ≤ ({w} ∪ (l.toFinset.filter fun u => u ≠ w)).card := + Finset.card_le_card hsplit + _ ≤ ({w} : Finset ℕ).card + (l.toFinset.filter fun u => u ≠ w).card := + Finset.card_union_le _ _ + _ ≤ 2 := by simp only [Finset.card_singleton]; omega + have hq : (qPorts os w).length = 2 + l.length := by + simp only [qPorts, l, List.length_append, List.length_cons, List.length_nil, List.length_map] + omega + +/-! ### The network: sizes and bipartition -/ + +variable (os) + +@[simp] theorem fst_network (B m : ℕ) : (network os B m).1 = m + os.length := rfl + +@[simp] theorem numEdges_network (B m : ℕ) : (network os B m).2.numEdges = 3 * os.length := rfl + +theorem vertices_network (B m : ℕ) : (network os B m).2.vertices = + (List.range m).map (clauseVertex os B) ++ (List.range os.length).map linkVertex ++ + (List.range os.length).map (qVertex os B) := rfl + +@[simp] theorem length_vertices_network (B m : ℕ) : + (network os B m).2.vertices.length = m + 2 * os.length := by + simp [vertices_network] + omega + +private theorem sum_range_ite (m a : ℕ) (c : Prop) [Decidable c] : + ((List.range m).map fun i => if c ∧ a = i then 1 else 0).sum = if c ∧ a < m then 1 else 0 := by + induction m with + | zero => simp + | succ m ih => + rw [List.range_succ, List.map_append, List.sum_append, ih] + by_cases hc : c + · rcases lt_trichotomy a m with h | rfl | h + · simp [hc, h, Nat.lt_succ_of_lt h, h.ne] + · simp [hc] + · simp [hc, show ¬ a < m by omega, show ¬ a < m + 1 by omega, show a ≠ m by omega] + · simp [hc] + +private theorem sum_range_ite' (m a : ℕ) : + ((List.range m).map fun i => if a = i then 1 else 0).sum = if a < m then 1 else 0 := by + simpa using sum_range_ite m a True + +private theorem count_clausePorts (i j : ℕ) : + (clausePorts os i).count j = + if (j % 3 = 0 ∧ j / 3 < os.length) ∧ clauseOf os (j / 3) = i then 1 else 0 := by + rw [List.Nodup.count (nodup_clausePorts i)] + have key : j ∈ clausePorts os i ↔ + (j % 3 = 0 ∧ j / 3 < os.length) ∧ clauseOf os (j / 3) = i := by + rw [mem_clausePorts] + constructor + · rintro ⟨u, hu, rfl, rfl⟩ + refine ⟨⟨by omega, by omega⟩, ?_⟩ + rw [show 3 * u / 3 = u by omega] + · rintro ⟨⟨h0, hlt⟩, rfl⟩ + exact ⟨j / 3, hlt, rfl, by omega⟩ + by_cases h : (j % 3 = 0 ∧ j / 3 < os.length) ∧ clauseOf os (j / 3) = i <;> simp [h, key] + +private theorem count_link (u j : ℕ) : + (linkVertex u).1.count j = if (j % 3 ≠ 0) ∧ j / 3 = u then 1 else 0 := by + rw [List.Nodup.count (by simp [linkVertex])] + have key : j ∈ (linkVertex u).1 ↔ (j % 3 ≠ 0) ∧ j / 3 = u := by + simp only [linkVertex, List.mem_cons, List.not_mem_nil, or_false] + omega + by_cases h : (j % 3 ≠ 0) ∧ j / 3 = u <;> simp [h, key] + +private theorem count_qPorts (w j : ℕ) : + (qPorts os w).count j = + if (j < 3 * os.length) ∧ (if j % 3 = 2 then prev os (j / 3) else j / 3) = w then 1 else 0 + + if (3 * os.length ≤ j) ∧ (j = 3 * w ∨ j = 3 * w + 1) then 1 else 0 := by + rw [List.Nodup.count (nodup_qPorts w)] + have key : j ∈ qPorts os w ↔ + ((j < 3 * os.length) ∧ (if j % 3 = 2 then prev os (j / 3) else j / 3) = w) ∨ + ((3 * os.length ≤ j) ∧ (j = 3 * w ∨ j = 3 * w + 1)) := by + rw [mem_qPorts] + constructor + · rintro (rfl | rfl | ⟨u, hu, rfl, rfl⟩) + · by_cases hw : 3 * w < 3 * os.length + · left + simp [hw] + · right + omega + · by_cases hw : 3 * w + 1 < 3 * os.length + · left + simp [hw, show (3 * w + 1) / 3 = w by omega] + · right + omega + · left + simp [show 3 * u + 2 < 3 * os.length by omega, show (3 * u + 2) % 3 = 2 by omega, + show (3 * u + 2) / 3 = u by omega] + · rintro (⟨hj, h⟩ | ⟨-, h⟩) + · split_ifs at h with h2 + · exact Or.inr (Or.inr ⟨j / 3, by omega, h, by omega⟩) + · subst h + omega + · omega + by_cases h1 : (j < 3 * os.length) ∧ (if j % 3 = 2 then prev os (j / 3) else j / 3) = w + · have h2 : ¬ ((3 * os.length ≤ j) ∧ (j = 3 * w ∨ j = 3 * w + 1)) := fun h => by omega + simp [key, h1, h2] + · by_cases h2 : (3 * os.length ≤ j) ∧ (j = 3 * w ∨ j = 3 * w + 1) <;> simp [key, h1, h2] + +/-- **The network is rows-first bipartite** when every occurrence names one of the `m` +clauses. -/ +theorem isRowsFirstBipartite_network (B m : ℕ) (hcl : ∀ o ∈ os, o.1 < m) : + (network os B m).2.IsRowsFirstBipartite (network os B m).1 := by + have hcl' : ∀ u < os.length, clauseOf os u < m := fun u hu => hcl _ (occ_mem os hu) + refine ⟨?_, fun j hj => ⟨?_, ?_⟩⟩ + · intro v hv i hi + simp only [vertices_network, List.mem_append, List.mem_map, List.mem_range] at hv + rcases hv with (⟨i', -, rfl⟩ | ⟨u, hu, rfl⟩) | ⟨w, hw, rfl⟩ + · obtain ⟨u, hu, -, rfl⟩ := mem_clausePorts.mp hi + simp only [numEdges_network] + omega + · simp only [linkVertex, List.mem_cons, List.not_mem_nil, or_false] at hi + simp only [numEdges_network] + omega + · rcases mem_qPorts.mp hi with rfl | rfl | ⟨u, hu, -, rfl⟩ <;> simp only [numEdges_network] <;> + omega + · simp only [numEdges_network] at hj + rw [fst_network, vertices_network, List.take_left' (by simp), List.map_append, + List.sum_append, List.map_map, List.map_map] + simp only [Function.comp_def, clauseVertex, count_clausePorts, count_link] + rw [sum_range_ite, sum_range_ite] + by_cases h0 : j % 3 = 0 + · simp [h0, hcl' (j / 3) (by omega), show j / 3 < os.length by omega] + · simp [h0, show j / 3 < os.length by omega] + · simp only [numEdges_network] at hj + rw [fst_network, vertices_network, List.drop_left' (by simp), List.map_map] + simp only [Function.comp_def, qVertex, count_qPorts, hj, true_and, show ¬ 3 * os.length ≤ j by + omega, false_and, ite_false, Nat.add_zero] + rw [sum_range_ite'] + have : (if j % 3 = 2 then prev os (j / 3) else j / 3) < os.length := by + split_ifs + · exact (prev_le os _).trans_lt (by omega) + · omega + simp [this] + +/-! ### Degrees -/ + +/-- **The degree bound**: if every clause has at most `B` occurrences, every vertex has at most +`max B 4` ports. -/ +theorem maxDegree_network_le (B m : ℕ) (hB : ∀ i, (os.map Prod.fst).count i ≤ B) : + (network os (max B 4) m).2.maxDegree ≤ max B 4 := by + refine (ExplicitTensorNetwork.maxDegree_le_iff _).mpr fun v hv => ?_ + simp only [vertices_network, List.mem_append, List.mem_map, List.mem_range] at hv + rcases hv with (⟨i, -, rfl⟩ | ⟨u, -, rfl⟩) | ⟨w, -, rfl⟩ + · simp only [clauseVertex, length_clausePorts] + exact (hB i).trans (le_max_left _ _) + · simp [linkVertex] + · exact (length_qPorts_le w).trans (le_max_right _ _) + +/-- **Full tables**: under the degree bound, every table lists `2 ^ (number of ports)` values. -/ +theorem length_table_network (B m : ℕ) (hB : ∀ i, (os.map Prod.fst).count i ≤ B) : + ∀ v ∈ (network os (max B 4) m).2.vertices, v.2.length = 2 ^ v.1.length := by + intro v hv + have hdeg := (network os (max B 4) m).2.length_le_maxDegree hv + have hmax := maxDegree_network_le os B m hB + simp only [vertices_network, List.mem_append, List.mem_map, List.mem_range] at hv + rcases hv with (⟨i, -, rfl⟩ | ⟨u, -, rfl⟩) | ⟨w, -, rfl⟩ + · exact length_boundedTable _ (hdeg.trans hmax) + · rfl + · exact length_boundedTable _ (hdeg.trans hmax) + +/-! ### The contraction -/ + +private theorem prod_map_boole {α : Type*} (l : List α) (p : α → Prop) [DecidablePred p] : + (l.map fun a => if p a then (1 : ℕ) else 0).prod = if ∀ a ∈ l, p a then 1 else 0 := by + induction l with + | nil => simp + | cons a l ih => + rw [List.map_cons, List.prod_cons, ih] + by_cases ha : p a <;> simp [ha] + +/-- The bits on the edges, read as a function of the edge numbers. -/ +private def bitAt {E : ℕ} (x : Fin E → Bool) (j : ℕ) : Bool := if h : j < E then x ⟨j, h⟩ else false + +/-- The weight conditions of an assignment: every clause has an edge differing from its falsifying +word, every link vertex sees equal bits, and every equality vertex sees equal bits. -/ +private def Good (m : ℕ) (X : ℕ → Bool) : Prop := + (∀ i < m, ¬ ∀ j ∈ clausePorts os i, X j = !pol os (j / 3)) ∧ + (∀ u < os.length, X (3 * u + 1) = X (3 * u + 2)) ∧ + ∀ w < os.length, ∀ a ∈ qPorts os w, ∀ b ∈ qPorts os w, X a = X b + +private instance (m : ℕ) (X : ℕ → Bool) : Decidable (Good os m X) := by + unfold Good + infer_instance + +/-- The entry of a clause vertex: one exactly when some port differs from the falsifying word. -/ +private theorem entry_clauseVertex {B i : ℕ} (X : ℕ → Bool) (h : (clausePorts os i).length ≤ B) : + ExplicitTensorNetwork.entry (clauseVertex os B i).2 ((clauseVertex os B i).1.map X) = + if ¬ ∀ j ∈ clausePorts os i, X j = !pol os (j / 3) then 1 else 0 := by + simp only [clauseVertex] + rw [show (clausePorts os i).length = ((clausePorts os i).map X).length by simp, + entry_boundedTable _ (by simpa using h), falsifier, clauseEntry_lsbValue (by simp)] + simp only [List.map_inj_left] + by_cases hc : ∀ j ∈ clausePorts os i, X j = !pol os (j / 3) + · simp only [eq_true hc, not_true_eq_false, ite_true, ite_false] + · simp only [eq_false hc, not_false_eq_true, ite_true, ite_false] + +private theorem entry_linkVertex (u : ℕ) (X : ℕ → Bool) : + ExplicitTensorNetwork.entry (linkVertex u).2 ((linkVertex u).1.map X) = + if X (3 * u + 1) = X (3 * u + 2) then 1 else 0 := by + simp only [linkVertex, List.map_cons, List.map_nil, ExplicitTensorNetwork.entry, + BitString.lsbValue] + cases X (3 * u + 1) <;> cases X (3 * u + 2) <;> rfl + +private theorem entry_qVertex {B w : ℕ} (X : ℕ → Bool) (h : (qPorts os w).length ≤ B) : + ExplicitTensorNetwork.entry (qVertex os B w).2 ((qVertex os B w).1.map X) = + if ∀ a ∈ qPorts os w, ∀ b ∈ qPorts os w, X a = X b then 1 else 0 := by + simp only [qVertex] + rw [show (qPorts os w).length = ((qPorts os w).map X).length by simp, + entry_boundedTable _ (by simpa using h), eqEntry_lsbValue] + simp + +/-- The contraction counts the assignments satisfying the weight conditions. -/ +private theorem contraction_network_eq (B m : ℕ) (hB : ∀ i, (os.map Prod.fst).count i ≤ B) : + (network os (max B 4) m).2.contraction = + (Finset.univ.filter fun x : Fin (3 * os.length) → Bool => Good os m (bitAt x)).card := by + rw [ExplicitTensorNetwork.contraction, ← Nat.cast_id (Finset.card _), ← Finset.sum_boole] + refine Finset.sum_congr rfl fun x _ => ?_ + have hpb : ∀ ps : List ℕ, (network os (max B 4) m).2.portBits x ps = ps.map (bitAt x) := + fun _ => rfl + simp only [hpb] + rw [vertices_network, List.map_append, List.map_append, List.prod_append, List.prod_append, + List.map_map, List.map_map, List.map_map] + have h1 : (List.range m).map ((fun v => ExplicitTensorNetwork.entry v.2 (v.1.map (bitAt x))) ∘ + clauseVertex os (max B 4)) = (List.range m).map fun i => + if ¬ ∀ j ∈ clausePorts os i, bitAt x j = !pol os (j / 3) then 1 else 0 := + List.map_congr_left fun i _ => entry_clauseVertex os (bitAt x) + ((length_clausePorts i).trans_le ((hB i).trans (le_max_left _ _))) + have h2 : (List.range os.length).map ((fun v => ExplicitTensorNetwork.entry v.2 + (v.1.map (bitAt x))) ∘ linkVertex) = (List.range os.length).map fun u => + if bitAt x (3 * u + 1) = bitAt x (3 * u + 2) then 1 else 0 := + List.map_congr_left fun u _ => entry_linkVertex u (bitAt x) + have h3 : (List.range os.length).map ((fun v => ExplicitTensorNetwork.entry v.2 + (v.1.map (bitAt x))) ∘ qVertex os (max B 4)) = (List.range os.length).map fun w => + if ∀ a ∈ qPorts os w, ∀ b ∈ qPorts os w, bitAt x a = bitAt x b then 1 else 0 := + List.map_congr_left fun w _ => entry_qVertex os (bitAt x) + ((length_qPorts_le w).trans (le_max_right _ _)) + rw [h1, h2, h3, prod_map_boole, prod_map_boole, prod_map_boole] + clear h1 h2 h3 hpb + simp only [List.mem_range, Good] + split_ifs <;> first | rfl | (exfalso; tauto) + +/-- Under the weight conditions, the three edges of an occurrence carry equal bits, equal to the +bit on the clause edge of the previous occurrence. -/ +private theorem consistent_of_good {m : ℕ} {X : ℕ → Bool} (h : Good os m X) {u : ℕ} + (hu : u < os.length) : + X (3 * u) = X (3 * u + 1) ∧ X (3 * u + 1) = X (3 * u + 2) ∧ + X (3 * u + 2) = X (3 * prev os u) := by + obtain ⟨-, hlink, hq⟩ := h + refine ⟨hq u hu _ (by simp [qPorts]) _ (by simp [qPorts]), hlink u hu, ?_⟩ + exact hq (prev os u) ((prev_le os u).trans_lt hu) _ + (mem_qPorts.mpr (Or.inr (Or.inr ⟨u, hu, rfl, rfl⟩))) _ (mem_qPorts.mpr (Or.inl rfl)) + +/-- Under the weight conditions, occurrences of the same variable carry equal bits on their +clause edges. -/ +private theorem eq_of_var_eq {m : ℕ} {X : ℕ → Bool} (h : Good os m X) {u w : ℕ} + (hu : u < os.length) (hw : w < os.length) (huw : var os u = var os w) : + X (3 * u) = X (3 * w) := by + have key : ∀ w, w < os.length → ∀ u ≤ w, var os u = var os w → X (3 * u) = X (3 * w) := by + intro w + induction w using Nat.strong_induction_on with + | _ w ih => + intro hw u huw hv + rcases Nat.eq_or_lt_of_le huw with rfl | hlt + · rfl + rcases prev_spec os w with ⟨hp, hpv, hbetween⟩ | ⟨-, hfirst⟩ + · have hup : u ≤ prev os w := by + by_contra hc + exact hbetween u (by omega) hlt hv + obtain ⟨h1, h2, h3⟩ := consistent_of_good os h hw + rw [ih (prev os w) hp (by omega) u hup (by rw [hv, hpv]), h1, h2, h3] + · exact (hfirst u hlt hv).elim + rcases le_total u w with h' | h' + · exact key w hw u h' huw + · exact (key u hu w h' huw.symm).symm + +private theorem bitAt_eq {E : ℕ} (x : Fin E → Bool) {j : ℕ} (hj : j < E) : + bitAt x j = x ⟨j, hj⟩ := by + simp [bitAt, hj] + +variable {φ : CNF ℕ} + +private theorem var_mem_vars {u : ℕ} (hu : u < (occurrences φ).length) : + var (occurrences φ) u ∈ φ.vars := by + rw [← map_occurrences] + exact List.mem_map.mpr ⟨_, occ_mem _ hu, rfl⟩ + +private theorem exists_var_eq {v : ℕ} (hv : v ∈ φ.vars) : + ∃ u < (occurrences φ).length, var (occurrences φ) u = v := by + rw [← map_occurrences] at hv + obtain ⟨o, ho, rfl⟩ := List.mem_map.mp hv + obtain ⟨u, hu, rfl⟩ := List.mem_iff_getElem.mp ho + exact ⟨u, hu, by simp [var, occ_eq_getElem _ hu]⟩ + +/-- An occurrence names a clause and one of its literals. -/ +private theorem mem_of_occ {u : ℕ} (hu : u < (occurrences φ).length) : + ∃ h : clauseOf (occurrences φ) u < φ.length, + (occ (occurrences φ) u).2.2 ∈ φ[clauseOf (occurrences φ) u] := by + obtain ⟨h₁, h₂, h₃⟩ := mem_occurrences.mp (occ_mem _ hu) + exact ⟨h₁, by rw [h₃]; exact List.getElem_mem h₂⟩ + +/-- Every literal of a clause is an occurrence. -/ +private theorem exists_occ {i : ℕ} (hi : i < φ.length) {l : Literal ℕ} (hl : l ∈ φ[i]) : + ∃ u < (occurrences φ).length, clauseOf (occurrences φ) u = i ∧ + (occ (occurrences φ) u).2.2 = l := by + obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp hl + obtain ⟨u, hu, hou⟩ := List.mem_iff_getElem.mp + ((mem_occurrences (φ := φ) (o := (i, j, φ[i][j]))).mpr ⟨hi, hj, rfl⟩) + exact ⟨u, hu, by simp [clauseOf, occ_eq_getElem _ hu, hou], + by simp [occ_eq_getElem _ hu, hou]⟩ + +/-- **The weight conditions describe the satisfying assignments**: an assignment of the edges has +weight one exactly when it puts on the three edges of every occurrence the value of its variable +under a satisfying assignment. -/ +private theorem good_iff + (hmem₁ : ∀ u < os.length, ∃ h : clauseOf os u < φ.length, (occ os u).2.2 ∈ φ[clauseOf os u]) + (hmem₂ : ∀ i (hi : i < φ.length), ∀ l ∈ φ[i], + ∃ u < os.length, clauseOf os u = i ∧ (occ os u).2.2 = l) + (x : Fin (3 * os.length) → Bool) : + Good os φ.length (bitAt x) ↔ + ∃ σ : ℕ → Bool, φ.eval σ = true ∧ (fun j => σ (var os (j.val / 3))) = x := by + constructor + · intro h + have hvs : ∀ u < os.length, (os.map fun o => o.2.2.1).idxOf (var os u) < os.length ∧ + var os ((os.map fun o => o.2.2.1).idxOf (var os u)) = var os u := by + intro u hu + have hm : var os u ∈ os.map fun o => o.2.2.1 := List.mem_map.mpr ⟨_, occ_mem os hu, rfl⟩ + have hlt := List.idxOf_lt_length_of_mem hm + have h1 := List.getElem_idxOf hlt + rw [List.length_map] at hlt + refine ⟨hlt, ?_⟩ + rw [List.getElem_map] at h1 + rw [var, occ_eq_getElem os hlt] + exact h1 + have hrep : ∀ u < os.length, + bitAt x (3 * (os.map fun o => o.2.2.1).idxOf (var os u)) = bitAt x (3 * u) := + fun u hu => eq_of_var_eq os h (hvs u hu).1 hu (hvs u hu).2 + refine ⟨fun v => bitAt x (3 * (os.map fun o => o.2.2.1).idxOf v), ?_, ?_⟩ + · rw [CNF.eval_eq_true_iff] + intro c hc + obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hc + have hcl := h.1 i hi + simp only [not_forall] at hcl + obtain ⟨j, hj, hne⟩ := hcl + obtain ⟨u, hu, hci, rfl⟩ := mem_clausePorts.mp hj + rw [show 3 * u / 3 = u by omega] at hne + have hpol : bitAt x (3 * u) = pol os u := by + revert hne + cases bitAt x (3 * u) <;> cases pol os u <;> simp + subst hci + obtain ⟨_, hocc⟩ := hmem₁ u hu + rw [Clause.eval_eq_true_iff] + exact ⟨_, hocc, (hrep u hu).trans hpol⟩ + · funext j + have hj := j.isLt + have hu : j.val / 3 < os.length := by omega + change bitAt x (3 * (os.map fun o => o.2.2.1).idxOf (var os (j.val / 3))) = x j + rw [hrep _ hu, ← bitAt_eq x hj] + obtain ⟨h1, h2, -⟩ := consistent_of_good os h hu + have hcases : j.val = 3 * (j.val / 3) ∨ j.val = 3 * (j.val / 3) + 1 ∨ + j.val = 3 * (j.val / 3) + 2 := by omega + rcases hcases with h' | h' | h' + · rw [← h'] + · rw [h1, ← h'] + · rw [h1, h2, ← h'] + · rintro ⟨σ, hσ, rfl⟩ + have hX : ∀ j < 3 * os.length, bitAt (fun j : Fin (3 * os.length) => + σ (var os (j.val / 3))) j = σ (var os (j / 3)) := fun j hj => bitAt_eq _ hj + refine ⟨fun i hi hall => ?_, fun u hu => ?_, fun w hw a ha b hb => ?_⟩ + · have hc := (CNF.eval_eq_true_iff σ φ).mp hσ _ (List.getElem_mem hi) + obtain ⟨l, hl, hsl⟩ := (Clause.eval_eq_true_iff σ _).mp hc + obtain ⟨u, hu, hci, hocc⟩ := hmem₂ i hi l hl + have h3u : 3 * u ∈ clausePorts os i := mem_clausePorts.mpr ⟨u, hu, hci, rfl⟩ + have := hall _ h3u + rw [hX _ (by omega), show 3 * u / 3 = u by omega] at this + have hv : var os u = l.1 := by rw [var, hocc] + have hp : pol os u = l.2 := by rw [pol, hocc] + rw [hv, hp, hsl] at this + cases l.2 <;> simp at this + · rw [hX _ (by omega), hX _ (by omega), show (3 * u + 1) / 3 = u by omega, + show (3 * u + 2) / 3 = u by omega] + · have hval : ∀ c ∈ qPorts os w, bitAt (fun j : Fin (3 * os.length) => + σ (var os (j.val / 3))) c = σ (var os w) := by + intro c hc + rcases mem_qPorts.mp hc with rfl | rfl | ⟨u, hu, hpu, rfl⟩ + · rw [hX _ (by omega), show 3 * w / 3 = w by omega] + · rw [hX _ (by omega), show (3 * w + 1) / 3 = w by omega] + · rw [hX _ (by omega), show (3 * u + 2) / 3 = u by omega, ← hpu, var_prev] + rw [hval a ha, hval b hb] + +/-- **The contraction of the clause network is the model count**, for formulas whose clauses have +at most `k` literals. -/ +theorem contraction_clauseNetwork {k : ℕ} (hk : ∀ c ∈ φ, c.length ≤ k) : + (clauseNetwork k φ).2.contraction = φ.modelCount := by + have hB : ∀ i, ((occurrences φ).map Prod.fst).count i ≤ k := by + intro i + rw [count_map_fst_occurrences] + by_cases hi : i < φ.length + · rw [List.getD_eq_getElem _ _ hi] + exact hk _ (List.getElem_mem hi) + · rw [List.getD_eq_default _ _ (by omega)] + exact Nat.zero_le _ + rw [clauseNetwork, contraction_network_eq _ k _ hB] + symm + refine CNF.modelCount_eq_card_filter (fun σ (j : Fin (3 * (occurrences φ).length)) => + σ (var (occurrences φ) (j.val / 3))) _ (fun σ τ _ _ => ?_) + fun x => good_iff _ (fun _ => mem_of_occ) (fun _ => exists_occ) x + constructor + · intro h v hv + obtain ⟨u, hu, rfl⟩ := exists_var_eq hv + have := congrFun h ⟨3 * u, by omega⟩ + simpa [show 3 * u / 3 = u by omega] using this + · intro h + funext j + exact h _ (var_mem_vars (by have := j.isLt; omega)) + + +/-- **The clause network is rows-first bipartite.** -/ +theorem isRowsFirstBipartite_clauseNetwork (k : ℕ) (φ : CNF ℕ) : + (clauseNetwork k φ).2.IsRowsFirstBipartite (clauseNetwork k φ).1 := + isRowsFirstBipartite_network _ _ _ fun _ ho => (mem_occurrences.mp ho).1 + +private theorem count_le_of_width {k : ℕ} (hk : ∀ c ∈ φ, c.length ≤ k) (i : ℕ) : + ((occurrences φ).map Prod.fst).count i ≤ k := by + rw [count_map_fst_occurrences] + by_cases hi : i < φ.length + · rw [List.getD_eq_getElem _ _ hi] + exact hk _ (List.getElem_mem hi) + · rw [List.getD_eq_default _ _ (by omega)] + exact Nat.zero_le _ + +/-- **The degree bound**: for clauses of at most `k` literals, every vertex has at most `max k 4` +ports. -/ +theorem maxDegree_clauseNetwork_le {k : ℕ} (hk : ∀ c ∈ φ, c.length ≤ k) : + (clauseNetwork k φ).2.maxDegree ≤ max k 4 := + maxDegree_network_le _ k _ (count_le_of_width hk) + +/-- **Full tables**, for clauses of at most `k` literals. -/ +theorem length_table_clauseNetwork {k : ℕ} (hk : ∀ c ∈ φ, c.length ≤ k) : + ∀ v ∈ (clauseNetwork k φ).2.vertices, v.2.length = 2 ^ v.1.length := + length_table_network _ k _ (count_le_of_width hk) + +/-- The clause network has three edges per literal occurrence. -/ +theorem numEdges_clauseNetwork (k : ℕ) (φ : CNF ℕ) : + (clauseNetwork k φ).2.numEdges = 3 * φ.vars.length := by + rw [← length_occurrences] + rfl + +/-- The clause network has one vertex per clause and two per literal occurrence. -/ +theorem length_vertices_clauseNetwork (k : ℕ) (φ : CNF ℕ) : + (clauseNetwork k φ).2.vertices.length = φ.length + 2 * φ.vars.length := by + rw [← length_occurrences, clauseNetwork, length_vertices_network] + +end Cslib.Circuits.Frontier.ClauseNetwork diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetworkPolyTime.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetworkPolyTime.lean new file mode 100644 index 0000000000..200113f80f --- /dev/null +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetworkPolyTime.lean @@ -0,0 +1,213 @@ +/- +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.Circuit.Frontier.TensorNetwork.ClauseNetwork +public import Complexity.Computability.Circuit.Frontier.TensorNetwork.DirectContraction +public import Complexity.Computability.Complexity.Problems.SAT +import Complexity.Computability.Complexity.Problems.SAT.PolyTime +public import Complexity.Logics.Propositional.CNF.PolyTime +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Option +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary +public import Complexity.Computability.Machines.Turing.MultiTape.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.Nat.Div +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeOptionPrimitives + +/-! +# The clause network in polynomial time + +The clause network of a formula (`Cslib.Circuits.Frontier.ClauseNetwork.clauseNetwork`) is +computable in polynomial time from the encoded formula, with its number of rows in binary and the +network in the encoding of the contraction algorithm (`ExplicitTensorNetwork.encExplicitNetwork`). +It is computed from the literal occurrences (`Cslib.Logic.PL.computableInPolyTime_occurrences`): +every port, previous occurrence and falsifying word is a search or a map over the occurrences, and +every table is a map over the first `2 ^ max k 4` numbers, a constant list. + +## Main results + +* `Cslib.Circuits.Frontier.ClauseNetwork.computableInPolyTime_clauseNetwork`: the clause network + is polynomial-time. +-/ + +public section + +namespace Cslib.Circuits.Frontier.ClauseNetwork + +open Turing.MultiTapeTM ComputableInPolyTime Cslib.Logic.PL +open Cslib.Complexity (encCNF) + +variable {α : Type} {inp : α ↪ List Bool} + +/-- The encoding of occurrence lists: unary clause and position indices and a binary literal. -/ +local notation "encOs" => encList (encOccurrence encNat) + +section Data + +variable {os : α → List (Occurrence ℕ)} (hos : ComputableInPolyTime os inp encOs) +include hos + +theorem computableInPolyTime_occ {u : α → ℕ} (hu : ComputableInPolyTime u inp encUnary) : + ComputableInPolyTime (fun a => occ (os a) (u a)) inp (encOccurrence encNat) := + listGetDWithInput hos hu _ + +theorem computableInPolyTime_var {u : α → ℕ} (hu : ComputableInPolyTime u inp encUnary) : + ComputableInPolyTime (fun a => var (os a) (u a)) inp encNat := + (fst _ _).comp ((snd _ _).comp ((snd _ _).comp (computableInPolyTime_occ hos hu))) + +theorem computableInPolyTime_pol {u : α → ℕ} (hu : ComputableInPolyTime u inp encUnary) : + ComputableInPolyTime (fun a => pol (os a) (u a)) inp encBool := + (snd _ _).comp ((snd _ _).comp ((snd _ _).comp (computableInPolyTime_occ hos hu))) + +theorem computableInPolyTime_clauseOf {u : α → ℕ} (hu : ComputableInPolyTime u inp encUnary) : + ComputableInPolyTime (fun a => clauseOf (os a) (u a)) inp encUnary := + (fst _ _).comp (computableInPolyTime_occ hos hu) + +theorem computableInPolyTime_prev {u : α → ℕ} (hu : ComputableInPolyTime u inp encUnary) : + ComputableInPolyTime (fun a => prev (os a) (u a)) inp encUnary := by + unfold prev + refine optionGetDWithInput (findWithInput (listReverseWithInput (range.comp hu)) ?_) hu + exact decide_eq' (computableInPolyTime_var (hos.comp (fst _ _)) (snd _ _)) + (computableInPolyTime_var (hos.comp (fst _ _)) (hu.comp (fst _ _))) + +theorem computableInPolyTime_length : ComputableInPolyTime (fun a => (os a).length) inp encUnary := + (length_list _).comp hos + +/-- The ports of a clause, in unary. -/ +theorem computableInPolyTime_clausePorts {i : α → ℕ} (hi : ComputableInPolyTime i inp encUnary) : + ComputableInPolyTime (fun a => clausePorts (os a) (i a)) inp (encList encUnary) := by + unfold clausePorts + refine mapWithInput (filterWithInput (range.comp (computableInPolyTime_length hos)) ?_) ?_ + · exact decide_eq' (computableInPolyTime_clauseOf (hos.comp (fst _ _)) (snd _ _)) + (hi.comp (fst _ _)) + · exact unary_mul' (const 3) (snd _ _) + +/-- The ports of an equality vertex, in unary. -/ +theorem computableInPolyTime_qPorts {w : α → ℕ} (hw : ComputableInPolyTime w inp encUnary) : + ComputableInPolyTime (fun a => qPorts (os a) (w a)) inp (encList encUnary) := by + unfold qPorts + refine listAppend' (cons' (unary_mul' (const 3) hw) + (cons' (unary_add' (unary_mul' (const 3) hw) (const 1)) (const []))) ?_ + refine mapWithInput (filterWithInput (range.comp (computableInPolyTime_length hos)) ?_) ?_ + · exact decide_eq' (computableInPolyTime_prev (hos.comp (fst _ _)) (snd _ _)) + (hw.comp (fst _ _)) + · exact unary_add' (unary_mul' (const 3) (snd _ _)) (const 2) + +end Data + +private theorem lsbValue_eq_ofBits : ∀ w : List Bool, BitString.lsbValue w = ofBits w + | [] => rfl + | c :: w => by + rw [BitString.lsbValue, lsbValue_eq_ofBits w] + simp only [ofBits, List.foldr_cons, Nat.bit_val] + ring + +/-- The falsifying word of a list of unary ports. -/ +theorem computableInPolyTime_falsifier {os : α → List (Occurrence ℕ)} + (hos : ComputableInPolyTime os inp encOs) {ps : α → List ℕ} + (hps : ComputableInPolyTime ps inp (encList encUnary)) : + ComputableInPolyTime (fun a => falsifier (os a) (ps a)) inp encNat := by + have hlist : ComputableInPolyTime (fun a => (ps a).map fun j => !pol (os a) (j / 3)) inp + (encList encBool) := + mapWithInput hps (bool_not.comp (computableInPolyTime_pol (hos.comp (fst _ _)) + (unary_div.comp ((snd _ _).prod (const 3))))) + have hbits := (bits_encList_polyTime encBool).2.comp hlist + have hnum := (ComputableInPolyTime.of_tidy ComputableTidilyInPolyTime.bitsToNat).comp hbits + simpa only [falsifier, lsbValue_eq_ofBits, Function.comp_def] using hnum + +/-- A bounded table whose entries are polynomial-time at every fixed position. -/ +theorem computableInPolyTime_boundedTable (B : ℕ) {w : α → ℕ} {f : α → ℕ → ℕ} + (hw : ComputableInPolyTime w inp encUnary) + (hf : ∀ idx, ComputableInPolyTime (fun a => f a idx) inp encNat) : + ComputableInPolyTime (fun a => boundedTable B (w a) (f a)) inp (encList encNat) := by + unfold boundedTable + exact mapFilterConst _ (fun idx _ => binary_lt' (const idx) (binary_pow' (const 2) hw)) + fun idx _ => hf idx + +private theorem binaryPorts {ps : α → List ℕ} + (hps : ComputableInPolyTime ps inp (encList encUnary)) : + ComputableInPolyTime ps inp (encList encNat) := by + simpa only [Function.comp_def, List.map_id'] using (map unary_to_binary).comp hps + +/-- **Clause vertices are polynomial-time.** -/ +theorem computableInPolyTime_clauseVertex (B : ℕ) {os : α → List (Occurrence ℕ)} + (hos : ComputableInPolyTime os inp encOs) {i : α → ℕ} + (hi : ComputableInPolyTime i inp encUnary) : + ComputableInPolyTime (fun a => clauseVertex (os a) B (i a)) inp + (encPair (encList encNat) (encList encNat)) := by + have hps := computableInPolyTime_clausePorts hos hi + have hz := computableInPolyTime_falsifier hos hps + unfold clauseVertex + refine (binaryPorts hps).prod (computableInPolyTime_boundedTable B ((length_list _).comp hps) + fun idx => ?_) + unfold clauseEntry + exact ite_decide (decide_eq' (const idx) hz) (const 0) (const 1) + +/-- **Equality vertices are polynomial-time.** -/ +theorem computableInPolyTime_qVertex (B : ℕ) {os : α → List (Occurrence ℕ)} + (hos : ComputableInPolyTime os inp encOs) {w : α → ℕ} + (hw : ComputableInPolyTime w inp encUnary) : + ComputableInPolyTime (fun a => qVertex (os a) B (w a)) inp + (encPair (encList encNat) (encList encNat)) := by + have hps := computableInPolyTime_qPorts hos hw + have hlen := (length_list _).comp hps + unfold qVertex + refine (binaryPorts hps).prod (computableInPolyTime_boundedTable B hlen fun idx => ?_) + unfold eqEntry + exact ite_decide (decide_or (decide_eq' (const (encOut := encNat) idx) (const 0)) + (decide_eq' (const (idx + 1)) (binary_pow' (const 2) hlen))) (const 1) (const 0) + +/-- **Link vertices are polynomial-time.** -/ +theorem computableInPolyTime_linkVertex {u : α → ℕ} (hu : ComputableInPolyTime u inp encUnary) : + ComputableInPolyTime (fun a => linkVertex (u a)) inp + (encPair (encList encNat) (encList encNat)) := by + unfold linkVertex + refine (binaryPorts (cons' (unary_add' (unary_mul' (const 3) hu) (const 1)) + (cons' (unary_add' (unary_mul' (const 3) hu) (const 2)) (const [])))).prod (const _) + +/-- **The network of an occurrence list is polynomial-time**, with its number of rows in binary. -/ +theorem computableInPolyTime_network (B : ℕ) {os : α → List (Occurrence ℕ)} + (hos : ComputableInPolyTime os inp encOs) {m : α → ℕ} + (hm : ComputableInPolyTime m inp encUnary) : + ComputableInPolyTime (fun a => network (os a) B (m a)) inp + (encPair encNat ExplicitTensorNetwork.encExplicitNetwork) := by + have hN := computableInPolyTime_length hos + have hout : ComputableInPolyTime (DescribedNetwork.equivProd (T := List ℕ)).symm + (encPair encUnary (encList (encPair (encList encNat) (encList encNat)))) + ExplicitTensorNetwork.encExplicitNetwork := + ComputableInPolyTime.of_eq fun _ => rfl + have hverts : ComputableInPolyTime (fun a => + (List.range (m a)).map (clauseVertex (os a) B) ++ (List.range (os a).length).map linkVertex ++ + (List.range (os a).length).map (qVertex (os a) B)) inp + (encList (encPair (encList encNat) (encList encNat))) := + listAppend' (listAppend' + (mapWithInput (range.comp hm) (computableInPolyTime_clauseVertex B (hos.comp (fst _ _)) + (snd _ _))) + (mapWithInput (range.comp hN) (computableInPolyTime_linkVertex (snd _ _)))) + (mapWithInput (range.comp hN) (computableInPolyTime_qVertex B (hos.comp (fst _ _)) + (snd _ _))) + unfold network + exact (unary_to_binary.comp (unary_add' hm hN)).prod + (hout.comp ((unary_mul' (const 3) hN).prod hverts)) + +/-- **The clause network is polynomial-time** from the encoded formula, with its number of rows in +binary. -/ +theorem computableInPolyTime_clauseNetwork (k : ℕ) : + ComputableInPolyTime (clauseNetwork k) encCNF + (encPair encNat ExplicitTensorNetwork.encExplicitNetwork) := + computableInPolyTime_network (max k 4) Complexity.SAT.computableInPolyTime_occurrences + (Complexity.SAT.computableInPolyTime_length (ComputableInPolyTime.id' (encIn := encCNF))) + +end Cslib.Circuits.Frontier.ClauseNetwork diff --git a/Complexity/Computability/Complexity/FineGrained/ContractionCounting.lean b/Complexity/Computability/Complexity/FineGrained/ContractionCounting.lean new file mode 100644 index 0000000000..b4b4b80b78 --- /dev/null +++ b/Complexity/Computability/Complexity/FineGrained/ContractionCounting.lean @@ -0,0 +1,353 @@ +/- +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.Circuit.Frontier.TensorNetwork.ClauseNetworkPolyTime +public import Complexity.Computability.Complexity.Classes.CountingSimulation.FastLeaves +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain +import Complexity.Computability.Complexity.Problems.SAT.PolyTime +import Complexity.Logics.Propositional.CNF.ModelCount.Declared +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +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.Plain +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives +import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends + +/-! +# Model counting by tensor contraction: the fixed-density bound of Theorem 1.1 + +For every fixed clause width `k`, one native machine computes the number of satisfying +assignments `CNF.modelCount φ` of 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 +(`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`). + +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, +and contracts it modulo `2 ^ (3 N)`, where `N` is the number of literal occurrences, with the +contraction algorithm of Theorem D.1 (`CountingSimulation.fastContractionAlgorithm`). The network +has `s = 3 N` edges, at most `3 N` vertices and degree at most `max k 4`, so it is admissible at +size `s` and the contraction takes `2 ^ O(s / √log s)` steps; since `n + 2 ≤ s ≤ 3 k m`, the +exponent is `O_k(m / √log n)`. Formulas that are empty, have an empty clause or have a clause +longer than `k` are answered directly. + +This does not prove the arbitrary-density bound `2 ^ O_k(n log log n / √log n)` of Theorem 1.1, +which Appendix D.3 obtains from Theorem D.1 with truncation order `ℓ = n + 1`; the contraction +algorithm here has `ℓ = 1`. For dense formulas the exponent above exceeds `n`; the +interpolation-scale counter `CountingNativeEndpoint.exists_modelCounter` remains the bound for +them. + +## Main results + +* `Cslib.Complexity.ContractionCounting.exists_modelCounter`: the counter, with exponent + `A (m + 1) / √⌊log₂ (n + 2)⌋`. +* `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. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem 1.1 (p. 2), + Appendix D.2 (p. 54) and Theorem D.1 (p. 53). +-/ + +public section + +namespace Cslib.Complexity.ContractionCounting + +open Cslib.Logic.PL Cslib.Circuits.Frontier Cslib.Circuits.Frontier.ClauseNetwork + Turing.MultiTapeTM Cslib.GenericRAM CountingSimulation + +/-- The formulas handed to the contraction algorithm: nonempty, with every clause of between one +and `k` literals. -/ +@[expose] def guard (k : ℕ) (φ : CNF ℕ) : Bool := + !φ.isEmpty && φ.all fun c => decide (1 ≤ c.length ∧ c.length ≤ k) + +/-- The input of the contraction algorithm: the precision `3 N`, for `N` literal occurrences, and +the clause network. -/ +@[expose] def contractionInput (k : ℕ) (φ : CNF ℕ) : ℕ × ℕ × ExplicitTensorNetwork ℕ := + (3 * φ.vars.length, clauseNetwork k φ) + +/-- The answer off the guard: one for the empty formula, zero otherwise. -/ +@[expose] def fallback (φ : CNF ℕ) : ℕ := if φ.isEmpty then 1 else 0 + +/-- The count computed by the machine. -/ +@[expose] def count (k : ℕ) (φ : CNF ℕ) : ℕ := + if guard k φ then (clauseNetwork k φ).2.contraction % 2 ^ (3 * φ.vars.length) else fallback φ + +theorem computableInPolyTime_guard (k : ℕ) : ComputableInPolyTime (guard k) encCNF encBool := by + unfold guard + fun_prop + +theorem computableInPolyTime_contractionInput (k : ℕ) : + ComputableInPolyTime (contractionInput k) encCNF + (encPair encNat (encPair encNat ExplicitTensorNetwork.encExplicitNetwork)) := + (ComputableInPolyTime.unary_to_binary.comp (ComputableInPolyTime.unary_mul' + (ComputableInPolyTime.const 3) + (SAT.computableInPolyTime_vars_length (ComputableInPolyTime.id' (encIn := encCNF))))).prod + (computableInPolyTime_clauseNetwork k) + +theorem computableInPolyTime_fallback : ComputableInPolyTime fallback encCNF encNat := by + unfold fallback + fun_prop + +/-- **The machine**: the guard, then the contraction algorithm on the clause network or the +direct answer. -/ +noncomputable def certificate (k : ℕ) : NativeCertificate (count k) encCNF encNat := + (NativeCertificate.branch (NativeCertificate.ofPolyTime (computableInPolyTime_guard k)) + (fastContractionAlgorithm.certificate.comp + (NativeCertificate.ofPolyTime (computableInPolyTime_contractionInput k))) + (NativeCertificate.ofPolyTime computableInPolyTime_fallback)).congr fun _ => rfl + +private theorem certificate_time (k : ℕ) (φ : CNF ℕ) : (certificate k).time φ = + (NativeCertificate.ofPolyTime (computableInPolyTime_guard k)).time φ + + if guard k φ then + (NativeCertificate.ofPolyTime (computableInPolyTime_contractionInput k)).time φ + + fastContractionAlgorithm.certificate.time (contractionInput k φ) + else (NativeCertificate.ofPolyTime computableInPolyTime_fallback).time φ := rfl + +private theorem certificate_space (k : ℕ) (φ : CNF ℕ) : (certificate k).space φ = + (NativeCertificate.ofPolyTime (computableInPolyTime_guard k)).space φ + + if guard k φ then + (NativeCertificate.ofPolyTime (computableInPolyTime_contractionInput k)).space φ + + fastContractionAlgorithm.certificate.space (contractionInput k φ) + else (NativeCertificate.ofPolyTime computableInPolyTime_fallback).space φ := rfl + +/-! ### Correctness -/ + +theorem guard_eq_true_iff {k : ℕ} {φ : CNF ℕ} : + guard k φ = true ↔ φ ≠ [] ∧ ∀ c ∈ φ, 1 ≤ c.length ∧ c.length ≤ k := by + simp [guard] + +/-- A formula has at most `2 ^ n` satisfying assignments of its `n` variables. -/ +theorem modelCount_le_two_pow (φ : CNF ℕ) : φ.modelCount ≤ 2 ^ φ.numVars := by + unfold CNF.modelCount CNF.numVars + refine (Finset.card_filter_le _ _).trans ?_ + simp only [Finset.card_univ, Fintype.card_fun, Fintype.card_bool, Fintype.card_coe, le_refl] + +/-- A formula whose clauses are nonempty has at least as many literals as clauses. -/ +theorem length_le_length_vars {φ : CNF ℕ} (h : ∀ c ∈ φ, 1 ≤ c.length) : + φ.length ≤ φ.vars.length := by + rw [CNF.length_vars] + induction φ with + | nil => simp + | cons c φ ih => + have hc := h c List.mem_cons_self + have := ih fun c' hc' => h c' (List.mem_cons_of_mem _ hc') + simp only [List.length_cons, List.map_cons, List.sum_cons] + omega + +/-- **The machine counts models** of every formula whose clauses have at most `k` literals. -/ +theorem count_eq {k : ℕ} {φ : CNF ℕ} (hk : ∀ c ∈ φ, c.length ≤ k) : + count k φ = φ.modelCount := by + unfold count + split + · next hg => + obtain ⟨hne, hcl⟩ := guard_eq_true_iff.mp hg + rw [contraction_clauseNetwork hk] + refine Nat.mod_eq_of_lt ((modelCount_le_two_pow φ).trans_lt ?_) + have h1 : 1 ≤ φ.length := List.length_pos_iff.mpr hne + have h2 := length_le_length_vars fun c hc => (hcl c hc).1 + have h3 := CNF.numVars_le_length_vars φ + exact Nat.pow_lt_pow_right (by norm_num) (by omega) + · next hg => + unfold fallback + cases φ with + | nil => + rw [← CNF.modelCountOn_vars, CNF.modelCountOn_nil] + rfl + | cons c φ => + have hnil : [] ∈ c :: φ := by + by_contra hnil + apply hg + refine guard_eq_true_iff.mpr ⟨List.cons_ne_nil _ _, fun c' hc' => ⟨?_, hk c' hc'⟩⟩ + rcases Nat.eq_zero_or_pos c'.length with h0 | h0 + · exact (hnil (List.length_eq_zero_iff.mp h0 ▸ hc')).elim + · exact h0 + rw [← CNF.modelCountOn_vars, CNF.modelCountOn_eq_zero_of_nil_mem hnil] + simp + + +/-! ### Resources -/ + +/-- **Admissibility**: the clause network of a guarded formula with `N` literal occurrences is +admissible at size `3 N`, its number of edges, with constant `k + 4`. -/ +theorem explicitAdmissible_clauseNetwork {k : ℕ} {φ : CNF ℕ} (hg : guard k φ = true) : + ExplicitAdmissible (k + 4) (3 * φ.vars.length) (clauseNetwork k φ) := by + 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 hlog : 1 ≤ Nat.log 2 (3 * φ.vars.length) := Nat.log_pos (by norm_num) (by omega) + refine ⟨isRowsFirstBipartite_clauseNetwork k φ, ?_, ?_, ?_, length_table_clauseNetwork hk, ?_⟩ + · rw [numEdges_clauseNetwork] + nlinarith + · refine (maxDegree_clauseNetwork_le hk).trans ?_ + have : max k 4 ≤ k + 4 := max_le (by omega) (by omega) + nlinarith + · rw [length_vertices_clauseNetwork] + nlinarith + · rw [numEdges_clauseNetwork] + +/-- The exponent of the contraction is at most `3 k K (m + 1) / √⌊log₂ (n + 2)⌋`. -/ +theorem exponent_le {k K N m n : ℕ} (hN : 1 ≤ N) (hNm : N ≤ k * m) (hnN : n ≤ N) : + K * (3 * N) / Nat.sqrt (Nat.log 2 (3 * N)) ≤ + 3 * k * K * (m + 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 : K * (3 * N) ≤ K * (3 * (k * m)) := 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 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, hK⟩ := fastContractionAlgorithm.bound (k + 4) 1 + have hg := NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_guard k) + have hp := NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_contractionInput k) + have hf := NativeCertificate.ofPolyTime_isPolynomial computableInPolyTime_fallback + obtain ⟨cg, dg, htg⟩ := hg.1.exists_le + obtain ⟨cg', dg', hsg⟩ := hg.2.exists_le + obtain ⟨cp, dp, htp⟩ := hp.1.exists_le + obtain ⟨cp', dp', hsp⟩ := hp.2.exists_le + obtain ⟨cf, df, htf⟩ := hf.1.exists_le + obtain ⟨cf', df', hsf⟩ := hf.2.exists_le + 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, + (certificate k).computes.mono (cg + cp + cf + K * (p + 1) ^ K + cg' + cp' + cf' + 1) + (fun φ => ?_) (fun φ => ?_)⟩ + all_goals + set Y := (encCNF φ).length + 1 with hY + have hY1 : 1 ≤ Y := Nat.le_add_left 1 _ + have hpow {d d' : ℕ} (h : d ≤ d') : Y ^ d ≤ Y ^ d' := Nat.pow_le_pow_right hY1 h + have hn' : ((encPair encNat (encPair encNat ExplicitTensorNetwork.encExplicitNetwork)) + (contractionInput k φ)).length + 1 ≤ (p + 1) * Y ^ q := by + have h1 := hlen φ + have h2 : 1 ≤ Y ^ q := Nat.one_le_pow _ _ hY1 + rw [← hY] at h1 + nlinarith + have hn'K : (((encPair encNat (encPair encNat ExplicitTensorNetwork.encExplicitNetwork)) + (contractionInput k φ)).length + 1) ^ K ≤ (p + 1) ^ K * Y ^ (q * K) := by + 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)) + 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 := + (hpow h).trans (Nat.le_mul_of_pos_left _ h2E) + have htg' : (NativeCertificate.ofPolyTime (computableInPolyTime_guard k)).time φ ≤ cg * Z := + (htg φ).trans (Nat.mul_le_mul_left _ (hZ (by omega))) + have htp' : (NativeCertificate.ofPolyTime (computableInPolyTime_contractionInput k)).time φ ≤ + cp * Z := (htp φ).trans (Nat.mul_le_mul_left _ (hZ (by omega))) + have htf' : (NativeCertificate.ofPolyTime computableInPolyTime_fallback).time φ ≤ cf * Z := + (htf φ).trans (Nat.mul_le_mul_left _ (hZ (by omega))) + have htc : guard k φ = true → fastContractionAlgorithm.certificate.time (contractionInput 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 + calc fastContractionAlgorithm.certificate.time (contractionInput k φ) + ≤ K * ((p + 1) ^ K * Y ^ (q * K)) * 2 ^ E := by + refine hb.trans ?_ + exact Nat.mul_le_mul (Nat.mul_le_mul_left _ hn'K) + (Nat.pow_le_pow_right (by norm_num) hexp) + _ ≤ K * (p + 1) ^ K * Z := by + have := hpow (show q * K ≤ e by omega) + calc K * ((p + 1) ^ K * Y ^ (q * K)) * 2 ^ E + = K * (p + 1) ^ K * (2 ^ E * Y ^ (q * K)) := by ring + _ ≤ K * (p + 1) ^ K * Z := Nat.mul_le_mul_left _ (Nat.mul_le_mul_left _ this) + rw [certificate_time] + generalize hKP : K * (p + 1) ^ K = KP at htc + have hC : ∀ c, c ≤ cg + cp + cf + KP + cg' + cp' + cf' + 1 → + c * Z ≤ (cg + cp + cf + KP + cg' + cp' + cf' + 1) * (Z + 1) := fun c hc => + (Nat.mul_le_mul_right _ hc).trans (Nat.mul_le_mul_left _ (Nat.le_succ _)) + split + · next hgφ => + calc _ ≤ cg * Z + (cp * Z + KP * Z) := Nat.add_le_add htg' (Nat.add_le_add htp' (htc hgφ)) + _ = (cg + cp + KP) * Z := by ring + _ ≤ _ := hC _ (by omega) + · calc _ ≤ cg * Z + cf * Z := Nat.add_le_add htg' htf' + _ = (cg + cf) * Z := by ring + _ ≤ _ := hC _ (by omega) + · -- space + have hsg' : (NativeCertificate.ofPolyTime (computableInPolyTime_guard k)).space φ ≤ + cg' * Y ^ b := (hsg φ).trans (Nat.mul_le_mul_left _ (hpow (by omega))) + have hsp' : (NativeCertificate.ofPolyTime (computableInPolyTime_contractionInput k)).space φ ≤ + cp' * Y ^ b := (hsp φ).trans (Nat.mul_le_mul_left _ (hpow (by omega))) + have hsf' : (NativeCertificate.ofPolyTime computableInPolyTime_fallback).space φ ≤ + cf' * Y ^ b := (hsf φ).trans (Nat.mul_le_mul_left _ (hpow (by omega))) + have hsc : guard k φ = true → + fastContractionAlgorithm.certificate.space (contractionInput k φ) ≤ + K * (p + 1) ^ K * Y ^ b := by + intro 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 + have hb := (hK (3 * φ.vars.length) (3 * φ.vars.length) (clauseNetwork k φ) (by omega) + (by omega) (by omega) (explicitAdmissible_clauseNetwork hgφ)).2 + refine hb.trans ?_ + calc K * _ ≤ K * ((p + 1) ^ K * Y ^ (q * K)) := Nat.mul_le_mul_left _ hn'K + _ ≤ K * (p + 1) ^ K * Y ^ b := by + rw [← Nat.mul_assoc] + exact Nat.mul_le_mul_left _ (hpow (by omega)) + rw [certificate_space] + generalize hKP : K * (p + 1) ^ K = KP at hsc + have hC : ∀ c, c ≤ cg + cp + cf + KP + cg' + cp' + cf' + 1 → + c * Y ^ b ≤ (cg + cp + cf + KP + cg' + cp' + cf' + 1) * (Y ^ b + 1) := fun c hc => + (Nat.mul_le_mul_right _ hc).trans (Nat.mul_le_mul_left _ (Nat.le_succ _)) + split + · next hgφ => + calc _ ≤ cg' * Y ^ b + (cp' * Y ^ b + KP * Y ^ b) := + Nat.add_le_add hsg' (Nat.add_le_add hsp' (hsc hgφ)) + _ = (cg' + cp' + KP) * Y ^ b := by ring + _ ≤ _ := hC _ (by omega) + · calc _ ≤ cg' * Y ^ b + cf' * Y ^ b := Nat.add_le_add hsg' hsf' + _ = (cg' + cf') * Y ^ b := by ring + _ ≤ _ := hC _ (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 +`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_fixedDensity (k : ℕ) : + ∃ (count : CNF ℕ → ℕ) (T S : CNF ℕ → ℕ) (e b : ℕ), + (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) → count φ = φ.modelCount) ∧ + ComputableInO count encCNF encNat T S ∧ + (∀ φ, S φ = ((encCNF φ).length + 1) ^ b) ∧ + ∀ D : ℕ, ∃ A : ℕ, ∀ φ : CNF ℕ, φ.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 k + 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) (Nat.div_le_div_right ?_)) + have : φ.length + 1 ≤ (D + 1) * (φ.numVars + 1) := by nlinarith + calc A * (φ.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/ComplexityTests/ContractionCounting.lean b/ComplexityTests/ContractionCounting.lean new file mode 100644 index 0000000000..177d4f5876 --- /dev/null +++ b/ComplexityTests/ContractionCounting.lean @@ -0,0 +1,65 @@ +/- +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.ContractionCounting + +/-! # Model counting by tensor contraction: checked instances + +The clause network of a small formula with a repeated variable, its bipartition, admissibility +and contraction, and the fixed-density counter of Theorem 1.1. -/ + +namespace ComplexityTests.ContractionCounting + +open Cslib.Logic.PL Cslib.Circuits.Frontier Cslib.Circuits.Frontier.ClauseNetwork + Cslib.Complexity Cslib.Complexity.ContractionCounting Cslib.Complexity.CountingSimulation + +/-- `(x₀ ∨ ¬x₁) ∧ (x₁ ∨ x₀ ∨ x₁) ∧ ¬x₂`: three clauses, six occurrences, three variables. -/ +def φ₀ : CNF ℕ := [[(0, true), (1, false)], [(1, true), (0, true), (1, true)], [(2, false)]] + +-- The chains: the previous occurrence of each occurrence of `x₀, x₁, x₁, x₀, x₁, x₂`. +example : (List.range 6).map (prev (occurrences φ₀)) = [0, 1, 1, 0, 2, 5] := by decide + +example : clausePorts (occurrences φ₀) 1 = [6, 9, 12] := by decide + +example : qPorts (occurrences φ₀) 1 = [3, 4, 5, 8] := by decide + +example : (clauseNetwork 3 φ₀).2.numEdges = 18 ∧ (clauseNetwork 3 φ₀).1 = 9 ∧ + (clauseNetwork 3 φ₀).2.vertices.length = 15 := by decide + +example : (clauseNetwork 3 φ₀).2.IsRowsFirstBipartite (clauseNetwork 3 φ₀).1 := + isRowsFirstBipartite_clauseNetwork 3 φ₀ + +example : (clauseNetwork 3 φ₀).2.maxDegree = 4 := by decide + +-- The guard accepts `φ₀`, so its network is admissible at its number of edges. +example : ExplicitAdmissible (3 + 4) 18 (clauseNetwork 3 φ₀) := + explicitAdmissible_clauseNetwork (φ := φ₀) (by decide) + +example : (clauseNetwork 3 φ₀).2.contraction = φ₀.modelCount := + contraction_clauseNetwork (by decide) + +-- The guard rejects the empty formula, a formula with an empty clause and a clause too wide. +example : guard 3 [] = false ∧ guard 3 [[(0, true)], []] = false ∧ + guard 1 [[(0, true), (1, true)]] = false := by decide + +example : count 3 ([] : CNF ℕ) = 1 := count_eq (by simp) + +example : count 3 ([[(0, true)], []] : CNF ℕ) = 0 := by + rw [count_eq (by decide), ← CNF.modelCountOn_vars, CNF.modelCountOn_eq_zero_of_nil_mem (by simp)] + +-- The counter for width three, and its fixed-density form. +example : ∃ (count : CNF ℕ → ℕ) (A e b : ℕ), + (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ 3) → count φ = φ.modelCount) ∧ + Turing.MultiTapeTM.ComputableInO count encCNF Turing.MultiTapeTM.encNat + (fun φ => 2 ^ (A * (φ.length + 1) / Nat.sqrt (Nat.log 2 (φ.numVars + 2))) * + ((encCNF φ).length + 1) ^ e) + (fun φ => ((encCNF φ).length + 1) ^ b) := + exists_modelCounter 3 + +-- `φ₀` meets the density bound `m ≤ 1 · n` of the fixed-density statement. +example : φ₀.length ≤ 1 * φ₀.numVars := by decide + +end ComplexityTests.ContractionCounting From b2677d818e8e46d27acb7bd1ac5c1e8047edf3af Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 08:46:35 -0400 Subject: [PATCH 2/4] feat(FineGrained): one #k-SAT counter with both bounds of Theorem 1.1 (p. 57) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `DensityBranchCounting.exists_modelCounter k`: one machine computes the model count of every width-k formula in polynomial space, with a single time function bounded by 2^O(ρ(n)) · poly on every formula, by 2^O(n⌈log₂⌈log₂ n⌉⌉/√log n) · poly when m ≤ n⌈log₂⌈log₂ n⌉⌉, and by 2^O_D(n/√log n) · poly when m ≤ Dn. It is the single algorithm at the end of Appendix D.3: the tensor-contraction counter below the threshold and the Section 6.4 counter above it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../FineGrained/DensityBranchCounting.lean | 367 ++++++++++++++++++ ComplexityTests/DensityBranchCounting.lean | 63 +++ ROADMAP.md | 6 + 4 files changed, 437 insertions(+) create mode 100644 Complexity/Computability/Complexity/FineGrained/DensityBranchCounting.lean create mode 100644 ComplexityTests/DensityBranchCounting.lean diff --git a/Complexity.lean b/Complexity.lean index fd66ede951..eb657ae5a3 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1395,6 +1395,7 @@ public import Complexity.Computability.Complexity.FineGrained.CountingSparsifica public import Complexity.Computability.Complexity.FineGrained.CountingSparsificationUniform public import Complexity.Computability.Complexity.FineGrained.CountingSparsifyContext public import Complexity.Computability.Complexity.FineGrained.CountingTreeBound +public import Complexity.Computability.Complexity.FineGrained.DensityBranchCounting public import Complexity.Computability.Complexity.FineGrained.ExhaustiveSearch public import Complexity.Computability.Complexity.FineGrained.Exponents public import Complexity.Computability.Complexity.FineGrained.GeneralCNFBranchSchedule diff --git a/Complexity/Computability/Complexity/FineGrained/DensityBranchCounting.lean b/Complexity/Computability/Complexity/FineGrained/DensityBranchCounting.lean new file mode 100644 index 0000000000..edbf39220c --- /dev/null +++ b/Complexity/Computability/Complexity/FineGrained/DensityBranchCounting.lean @@ -0,0 +1,367 @@ +/- +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.CountingScale +public import Complexity.Computability.Complexity.Problems.SAT +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain +public import Complexity.Logics.Propositional.CNF.ModelCount +import Complexity.Computability.Complexity.FineGrained.ContractionCounting +import Complexity.Computability.Complexity.FineGrained.CountingNativeModelCount +import Complexity.Computability.Complexity.FineGrained.SparseBranchAsymptotics +import Complexity.Computability.Complexity.Problems.SAT.PolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Lists +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryLog +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain + +/-! +# One model counter with both bounds of Theorem 1.1 + +For every fixed clause width `k`, one machine computes the number of satisfying assignments +`CNF.modelCount φ` of every formula `φ` whose clauses have at most `k` literals, in polynomial +space, with a single time function `T` that satisfies three bounds at once +(`DensityBranchCounting.exists_modelCounter`). Write `n` for the number of variables, `m` for +the number of clauses, `L` for the encoding length and `ν = ⌈log₂ ⌈log₂ n⌉⌉`. + +* On every formula, `T` is `2 ^ O_k(ρ(n))` times a polynomial in `L`, where `ρ` is the + interpolation scale `n (log log n)² / √log n` of Section 6.4 of [OpenAI2026ETH]. +* On formulas with `m ≤ n ν`, it is `2 ^ O_k(n ν / √log n)` times a polynomial. +* For each density `D`, on formulas with `m ≤ D n` it is `2 ^ O_{k,D}(n / √log n)` times a + polynomial. Only the constant in the exponent depends on `D`; the machine, `T` and the degree + of the polynomial do not. + +The machine is the single algorithm in the last paragraph of Appendix D.3 of [OpenAI2026ETH] +(p. 57): it tests `m ≤ n ν` (`DensityBranchCounting.threshold`), runs the tensor-contraction +counter `ContractionCounting.exists_modelCounter` when the test passes, and otherwise runs a dense +counter. In the paper the dense branch is the parity-query proof of the arbitrary-density bound +(p. 57), with exponent `O_k(n log log n / √log n)`. It evaluates its queries by Lemma D.2 +(pp. 54–56), which applies Theorem D.1 with truncation order `ℓ = n + 1`. That is not formalized, +so the dense branch here is the Section 6.4 counter `CountingNativeEndpoint.exists_modelCounter`, +and the bound on every formula stays at the interpolation scale `ρ(n)`. The arbitrary-density +bound of Theorem 1.1 remains open. + +As in the two counters it combines, `n` is the number of variables occurring in `φ` +(`CNF.numVars`); the paper counts declared variables, with `n ≥ 20`. + +## Main definitions + +* `Cslib.Complexity.DensityBranchCounting.threshold`: the clause-count threshold `n ν`. + +## Main results + +* `Cslib.Complexity.DensityBranchCounting.exists_modelCounter`: the counter and its three bounds. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], Theorem 1.1 (p. 2) and + the last paragraph of Appendix D.3 (p. 57). +-/ + +public section + +namespace Cslib.Complexity.DensityBranchCounting + +open Cslib.Logic.PL Turing.MultiTapeTM SubexponentialSAT + +/-- The clause-count threshold of the single algorithm, `n ⌈log₂ ⌈log₂ n⌉⌉` for `n` variables. +Formulas with at most this many clauses are counted by tensor contraction. -/ +@[expose] def threshold (n : ℕ) : ℕ := n * Nat.clog 2 (Nat.clog 2 n) + +/-- The test of the single algorithm: at most `threshold n` clauses. -/ +private def guard (φ : CNF ℕ) : Bool := decide (φ.length ≤ threshold φ.numVars) + +private theorem computableInPolyTime_guard : ComputableInPolyTime guard encCNF encBool := by + unfold guard threshold + fun_prop + +/-! ### Arithmetic of the exponents -/ + +/-- The divisor `√⌊log₂ (n + 2)⌋` of the contraction exponent is positive. -/ +private theorem one_le_sqrt_log (n : ℕ) : 1 ≤ Nat.sqrt (Nat.log 2 (n + 2)) := + Nat.le_sqrt.mpr (by have := Nat.log_pos (b := 2) (n := n + 2) (by norm_num) (by omega); omega) + +/-- For a positive number of variables, the divisor `√⌊log₂ (n + 2)⌋` is at most `n`. -/ +private theorem sqrt_log_le {n : ℕ} (hn : 1 ≤ n) : Nat.sqrt (Nat.log 2 (n + 2)) ≤ n := by + refine (Nat.sqrt_le_self _).trans (Nat.lt_succ_iff.mp (Nat.log_lt_of_lt_pow (by omega) ?_)) + have := Nat.lt_two_pow_self (n := n) + rw [Nat.pow_succ] + omega + +/-- Below `16384` variables the threshold is at most `65536`. -/ +private theorem threshold_le_of_lt {n : ℕ} (hn : n < 16384) : threshold n ≤ 65536 := by + have h14 : Nat.clog 2 n ≤ 14 := + Nat.clog_le_of_le_pow (by norm_num; omega) + have h4 : Nat.clog 2 (Nat.clog 2 n) ≤ 4 := + Nat.clog_le_of_le_pow (by norm_num; omega) + unfold threshold + nlinarith + +/-- Above `2 ^ 2 ^ D` variables the threshold is at least `D n`. -/ +private theorem mul_le_threshold {D n : ℕ} (hn : 2 ^ 2 ^ D ≤ n) : D * n ≤ threshold n := by + have h1 : 2 ^ D ≤ Nat.clog 2 n := by + simpa only [Nat.clog_pow 2 _ one_lt_two] using Nat.clog_mono_right 2 hn + have h2 : D ≤ Nat.clog 2 (Nat.clog 2 n) := by + simpa only [Nat.clog_pow 2 _ one_lt_two] using Nat.clog_mono_right 2 h1 + unfold threshold + rw [Nat.mul_comm D n] + exact Nat.mul_le_mul_left n h2 + +/-- **The contraction exponent at the threshold is at most the interpolation scale**, up to the +factor `32`, from `16384` variables on: `n ν / √⌊log₂ (n + 2)⌋ ≤ 32 ρ(n)`. -/ +private theorem threshold_div_le_interpolationScale {n : ℕ} (hn : 16384 ≤ n) : + (threshold n : ℝ) / Nat.sqrt (Nat.log 2 (n + 2)) ≤ 32 * interpolationScale n := by + have hmain := ReplacementParams.mul_iter_clog_sq_div_sqrt_clog_le_interpolationScale hn + set lam := Nat.clog 2 n + set nu := Nat.clog 2 lam + set q := Nat.sqrt (Nat.log 2 (n + 2)) + have hlam : 14 ≤ lam := by + simpa only [show (16384 : ℕ) = 2 ^ 14 by norm_num, Nat.clog_pow 2 _ one_lt_two] using + Nat.clog_mono_right 2 hn + have hnu : 1 ≤ nu := by + simpa only [Nat.clog_pow 2 1 one_lt_two] using Nat.clog_mono_right 2 (by omega : 2 ^ 1 ≤ lam) + have hq : 1 ≤ q := one_le_sqrt_log n + -- `λ ≤ ⌊log₂ (n + 2)⌋ + 1 < (q + 1) ^ 2 + 1 ≤ (2 q) ^ 2 + 1` + have hlamq : lam ≤ (2 * q) ^ 2 := by + have h1 : lam ≤ Nat.log 2 (n + 2) + 1 := Nat.clog_le_of_le_pow + (by have := Nat.lt_pow_succ_log_self (b := 2) one_lt_two (n + 2); omega) + have h2 := Nat.lt_succ_sqrt' (Nat.log 2 (n + 2)) + change Nat.log 2 (n + 2) < (q + 1) ^ 2 at h2 + nlinarith + have hqR : (0 : ℝ) < q := Nat.cast_pos.mpr hq + have hlamR : (0 : ℝ) < Real.sqrt lam := + Real.sqrt_pos.mpr (Nat.cast_pos.mpr (by omega)) + have hsqrt : Real.sqrt lam ≤ 2 * q := by + rw [Real.sqrt_le_iff] + exact ⟨by positivity, by exact_mod_cast hlamq⟩ + have hnuR : (nu : ℝ) ≤ (nu : ℝ) ^ 2 := by + have : (1 : ℝ) ≤ nu := Nat.one_le_cast.mpr hnu + nlinarith + have hstep : (threshold n : ℝ) / q ≤ 2 * ((n : ℝ) * (nu : ℝ) ^ 2 / Real.sqrt lam) := by + rw [div_le_iff₀ hqR, show 2 * ((n : ℝ) * (nu : ℝ) ^ 2 / Real.sqrt lam) * q = + (n : ℝ) * (nu : ℝ) ^ 2 * (2 * q) / Real.sqrt lam by ring, le_div_iff₀ hlamR] + have hn0 : (0 : ℝ) ≤ n := Nat.cast_nonneg n + have hnu0 : (0 : ℝ) ≤ nu := Nat.cast_nonneg nu + calc (threshold n : ℝ) * Real.sqrt lam = (n : ℝ) * nu * Real.sqrt lam := by + simp only [threshold, Nat.cast_mul, nu, lam] + _ ≤ (n : ℝ) * nu * (2 * q) := mul_le_mul_of_nonneg_left hsqrt (by positivity) + _ ≤ (n : ℝ) * (nu : ℝ) ^ 2 * (2 * q) := + mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hnuR hn0) (by positivity) + linarith + +/-- The length of a formula's encoding is at least its number of clauses. -/ +private theorem length_le_length_encCNF (φ : CNF ℕ) : φ.length ≤ (encCNF φ).length := + length_le_length_encList _ φ + +/-- `2 ^ (A m / √⌊log₂ (n + 2)⌋)` on formulas with at most `threshold n` clauses is at most +`2 ^ O(ρ(n))` times a polynomial in the encoding length: the contraction branch obeys the +interpolation-scale bound. -/ +private theorem two_pow_le_of_le_threshold (A₁ : ℕ) {φ : CNF ℕ} + (hφ : φ.length ≤ threshold φ.numVars) : + 2 ^ (A₁ * φ.length / Nat.sqrt (Nat.log 2 (φ.numVars + 2))) ≤ + ⌈(2 : ℝ) ^ (((32 * A₁ : ℕ) : ℝ) * interpolationScale φ.numVars)⌉₊ * + ((encCNF φ).length + 1) ^ (65536 * A₁) := by + set E := A₁ * φ.length / Nat.sqrt (Nat.log 2 (φ.numVars + 2)) + set X := (2 : ℝ) ^ (((32 * A₁ : ℕ) : ℝ) * interpolationScale φ.numVars) + set Y := (encCNF φ).length + 1 + have hX : 1 ≤ ⌈X⌉₊ := Nat.one_le_ceil_iff.mpr (Real.rpow_pos_of_pos (by norm_num) _) + have hY : 1 ≤ Y := Nat.le_add_left 1 _ + rcases Nat.lt_or_ge φ.numVars 16384 with hn | hn + · -- few variables: the exponent is bounded, and charged to the encoding length + have hE : E ≤ 65536 * A₁ := + (Nat.div_le_self _ _).trans (by have := threshold_le_of_lt hn; nlinarith) + have h2Y : 2 ^ E ≤ Y ^ E := by + rcases Nat.eq_zero_or_pos φ.length with h0 | h0 + · simp only [E, h0, Nat.mul_zero, Nat.zero_div, pow_zero, le_refl] + · exact Nat.pow_le_pow_left (by have := length_le_length_encCNF φ; omega) E + calc 2 ^ E ≤ Y ^ E := h2Y + _ ≤ Y ^ (65536 * A₁) := Nat.pow_le_pow_right hY hE + _ ≤ ⌈X⌉₊ * Y ^ (65536 * A₁) := Nat.le_mul_of_pos_left _ hX + · -- many variables: the exponent is at most `32 ρ(n)` + have hscale := threshold_div_le_interpolationScale hn + have hER : (E : ℝ) ≤ ((32 * A₁ : ℕ) : ℝ) * interpolationScale φ.numVars := by + refine Nat.cast_div_le.trans ?_ + have hq : (0 : ℝ) < Nat.sqrt (Nat.log 2 (φ.numVars + 2)) := + Nat.cast_pos.mpr (one_le_sqrt_log _) + have hm : (φ.length : ℝ) ≤ threshold φ.numVars := by exact_mod_cast hφ + calc ((A₁ * φ.length : ℕ) : ℝ) / Nat.sqrt (Nat.log 2 (φ.numVars + 2)) + ≤ A₁ * ((threshold φ.numVars : ℝ) / Nat.sqrt (Nat.log 2 (φ.numVars + 2))) := by + rw [Nat.cast_mul, mul_div_assoc] + exact mul_le_mul_of_nonneg_left (div_le_div_of_nonneg_right hm hq.le) + (Nat.cast_nonneg _) + _ ≤ A₁ * (32 * interpolationScale φ.numVars) := + mul_le_mul_of_nonneg_left hscale (Nat.cast_nonneg _) + _ = ((32 * A₁ : ℕ) : ℝ) * interpolationScale φ.numVars := by push_cast; ring + have h2E : ((2 ^ E : ℕ) : ℝ) ≤ ⌈X⌉₊ := by + calc ((2 ^ E : ℕ) : ℝ) = (2 : ℝ) ^ (E : ℝ) := by + rw [Real.rpow_natCast]; push_cast; rfl + _ ≤ X := Real.rpow_le_rpow_of_exponent_le (by norm_num) hER + _ ≤ ⌈X⌉₊ := Nat.le_ceil X + calc 2 ^ E ≤ ⌈X⌉₊ := by exact_mod_cast h2E + _ ≤ ⌈X⌉₊ * Y ^ (65536 * A₁) := Nat.le_mul_of_pos_right _ (Nat.one_le_pow _ _ hY) + +/-! ### The counter -/ + +/-- The contraction counter of `ContractionCounting.exists_modelCounter`, with the exponent +`A m / √⌊log₂ (n + 2)⌋` in place of `A (m + 1) / √⌊log₂ (n + 2)⌋`. -/ +private theorem exists_contractionCounter (k : ℕ) : + ∃ (count : CNF ℕ → ℕ) (A e b : ℕ), + (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) → count φ = φ.modelCount) ∧ + ComputableInO count encCNF encNat + (fun φ => 2 ^ (A * φ.length / Nat.sqrt (Nat.log 2 (φ.numVars + 2))) * + ((encCNF φ).length + 1) ^ e) + (fun φ => ((encCNF φ).length + 1) ^ b) := by + obtain ⟨count, A, e, b, hcount, hc⟩ := ContractionCounting.exists_modelCounter k + refine ⟨count, A, e, b, hcount, hc.mono (2 ^ A) (fun φ => ?_) (fun φ => ?_)⟩ + · set s := Nat.sqrt (Nat.log 2 (φ.numVars + 2)) + have hs : 0 < s := one_le_sqrt_log _ + have hdiv : A * (φ.length + 1) / s ≤ A * φ.length / s + A := by + calc A * (φ.length + 1) / s ≤ (A * φ.length + s * A) / s := + Nat.div_le_div_right (by rw [Nat.mul_succ]; nlinarith) + _ = A * φ.length / s + A := Nat.add_mul_div_left _ _ hs + calc 2 ^ (A * (φ.length + 1) / s) * ((encCNF φ).length + 1) ^ e + ≤ 2 ^ (A * φ.length / s + A) * ((encCNF φ).length + 1) ^ e := + Nat.mul_le_mul_right _ (Nat.pow_le_pow_right (by norm_num) hdiv) + _ = 2 ^ A * (2 ^ (A * φ.length / s) * ((encCNF φ).length + 1) ^ e) := by ring + _ ≤ _ := Nat.mul_le_mul_left _ (Nat.le_succ _) + · exact (Nat.le_mul_of_pos_left _ (Nat.two_pow_pos A)).trans + (Nat.mul_le_mul_left _ (Nat.le_succ _)) + +/-- **One model counter with both bounds 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 its time function `T` satisfies, for `n` variables, `m` clauses and +encoding length `L`: + +* on every formula, `T φ ≤ ⌈2 ^ (A ρ(n))⌉ (L + 1) ^ e`, where `ρ = interpolationScale`; +* when `m ≤ threshold n = n ⌈log₂ ⌈log₂ n⌉⌉`, + `T φ ≤ 2 ^ (A · threshold n / √⌊log₂ (n + 2)⌋) (L + 1) ^ e`; +* for each density bound `D`, when `m ≤ D n`, `T φ ≤ 2 ^ (A' n / √⌊log₂ (n + 2)⌋) (L + 1) ^ e` + for a constant `A'` depending on `D`. + +The machine, `T`, `S` and the constants `A`, `e`, `b` are fixed before `D`; only `A'` depends on +`D`. -/ +theorem exists_modelCounter (k : ℕ) : + ∃ (count : CNF ℕ → ℕ) (T S : CNF ℕ → ℕ) (A e b : ℕ), + (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) → count φ = φ.modelCount) ∧ + ComputableInO count encCNF encNat T S ∧ + (∀ φ, S φ = ((encCNF φ).length + 1) ^ b) ∧ + (∀ φ, T φ ≤ ⌈(2 : ℝ) ^ ((A : ℝ) * interpolationScale φ.numVars)⌉₊ * + ((encCNF φ).length + 1) ^ e) ∧ + (∀ φ : CNF ℕ, φ.length ≤ threshold φ.numVars → + T φ ≤ 2 ^ (A * threshold φ.numVars / Nat.sqrt (Nat.log 2 (φ.numVars + 2))) * + ((encCNF φ).length + 1) ^ e) ∧ + ∀ D : ℕ, ∃ A' : ℕ, ∀ φ : CNF ℕ, φ.length ≤ D * φ.numVars → + T φ ≤ 2 ^ (A' * φ.numVars / Nat.sqrt (Nat.log 2 (φ.numVars + 2))) * + ((encCNF φ).length + 1) ^ e := by + obtain ⟨count₁, A₁, e₁, b₁, hcount₁, hc₁⟩ := exists_contractionCounter k + obtain ⟨count₂, A₂, e₂, b₂, hcount₂, hc₂⟩ := CountingNativeEndpoint.exists_modelCounter k + obtain ⟨d, _, hd⟩ := computableInPolyTime_guard.exists_degree + -- `e₀` is the polynomial degree of `T`; `e` absorbs the contraction branch on few variables + set e₀ := d + e₁ + e₂ with he₀ + set A := 32 * A₁ + A₂ with hA + set e := e₀ + 65536 * A₁ with he + set b := d + b₁ + b₂ with hb + set q : CNF ℕ → ℕ := fun φ => Nat.sqrt (Nat.log 2 (φ.numVars + 2)) with hq + set Y : CNF ℕ → ℕ := fun φ => (encCNF φ).length + 1 with hY + set T : CNF ℕ → ℕ := fun φ => if guard φ then 2 ^ (A₁ * φ.length / q φ) * Y φ ^ e₀ + else ⌈(2 : ℝ) ^ ((A₂ : ℝ) * interpolationScale φ.numVars)⌉₊ * Y φ ^ e₀ with hT + have hY1 (φ : CNF ℕ) : 1 ≤ Y φ := Nat.le_add_left 1 _ + have hYe (φ : CNF ℕ) : Y φ ^ e₀ ≤ Y φ ^ e := Nat.pow_le_pow_right (hY1 φ) (by omega) + have hT1 (φ : CNF ℕ) : Y φ ^ e₀ ≤ T φ := by + simp only [T] + split + · exact Nat.le_mul_of_pos_left _ (Nat.two_pow_pos _) + · exact Nat.le_mul_of_pos_left _ + (Nat.one_le_ceil_iff.mpr (Real.rpow_pos_of_pos (by norm_num) _)) + refine ⟨fun φ => if guard φ then count₁ φ else count₂ φ, T, fun φ => Y φ ^ b, A, e, b, + fun φ hφ => ?_, (hd.inO.ite hc₁ hc₂).mono 2 (fun φ => ?_) (fun φ => ?_), fun _ => rfl, + fun φ => ?_, fun φ hφ => ?_, fun D => ?_⟩ + · -- correctness: both branches count models + dsimp only + split + · exact hcount₁ φ hφ + · exact hcount₂ φ hφ + · -- time: the test and either branch are within `T` + have hd' : Y φ ^ d ≤ T φ := (Nat.pow_le_pow_right (hY1 φ) (by omega)).trans (hT1 φ) + have hbr : (if guard φ then 2 ^ (A₁ * φ.length / q φ) * Y φ ^ e₁ + else ⌈(2 : ℝ) ^ ((A₂ : ℝ) * interpolationScale φ.numVars)⌉₊ * Y φ ^ e₂) ≤ T φ := by + simp only [T] + split + · exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (hY1 φ) (by omega)) + · exact Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (hY1 φ) (by omega)) + change Y φ ^ d + (if guard φ then 2 ^ (A₁ * φ.length / q φ) * Y φ ^ e₁ + else ⌈(2 : ℝ) ^ ((A₂ : ℝ) * interpolationScale φ.numVars)⌉₊ * Y φ ^ e₂) ≤ 2 * (T φ + 1) + omega + · -- space: the test and either branch are within `Y ^ b` + have hd' : Y φ ^ d ≤ Y φ ^ b := Nat.pow_le_pow_right (hY1 φ) (by omega) + have hbr : (if guard φ then Y φ ^ b₁ else Y φ ^ b₂) ≤ Y φ ^ b := by + split + · exact Nat.pow_le_pow_right (hY1 φ) (by omega) + · exact Nat.pow_le_pow_right (hY1 φ) (by omega) + change Y φ ^ d + (if guard φ then Y φ ^ b₁ else Y φ ^ b₂) ≤ 2 * (Y φ ^ b + 1) + omega + · -- every formula: the interpolation scale + simp only [T] + split + · next hg => + have hφ : φ.length ≤ threshold φ.numVars := of_decide_eq_true hg + have h := two_pow_le_of_le_threshold A₁ hφ + have hceil : ⌈(2 : ℝ) ^ (((32 * A₁ : ℕ) : ℝ) * interpolationScale φ.numVars)⌉₊ ≤ + ⌈(2 : ℝ) ^ ((A : ℝ) * interpolationScale φ.numVars)⌉₊ := + Nat.ceil_le_ceil (Real.rpow_le_rpow_of_exponent_le (by norm_num) + (mul_le_mul_of_nonneg_right (by exact_mod_cast (by omega : 32 * A₁ ≤ A)) + (interpolationScale_nonneg _))) + calc 2 ^ (A₁ * φ.length / q φ) * Y φ ^ e₀ + ≤ ⌈(2 : ℝ) ^ ((A : ℝ) * interpolationScale φ.numVars)⌉₊ * Y φ ^ (65536 * A₁) * + Y φ ^ e₀ := Nat.mul_le_mul_right _ (h.trans (Nat.mul_le_mul_right _ hceil)) + _ = ⌈(2 : ℝ) ^ ((A : ℝ) * interpolationScale φ.numVars)⌉₊ * Y φ ^ e := by + rw [he, pow_add]; ring + · refine Nat.mul_le_mul (Nat.ceil_le_ceil (Real.rpow_le_rpow_of_exponent_le (by norm_num) + (mul_le_mul_of_nonneg_right (by exact_mod_cast (by omega : A₂ ≤ A)) + (interpolationScale_nonneg _)))) (hYe φ) + · -- at most `threshold n` clauses: the contraction branch + have hg : guard φ = true := decide_eq_true hφ + simp only [T, hg, ↓reduceIte] + refine Nat.mul_le_mul (Nat.pow_le_pow_right (by norm_num) (Nat.div_le_div_right ?_)) (hYe φ) + exact Nat.mul_le_mul (by omega) hφ + · -- fixed density: few variables fall back on a constant + set K := (Finset.range (2 ^ 2 ^ D)).sup + fun n => ⌈(2 : ℝ) ^ ((A₂ : ℝ) * interpolationScale n)⌉₊ with hK + refine ⟨A₁ * D + K, fun φ hφ => ?_⟩ + simp only [T] + split + · refine Nat.mul_le_mul (Nat.pow_le_pow_right (by norm_num) (Nat.div_le_div_right ?_)) + (hYe φ) + calc A₁ * φ.length ≤ A₁ * (D * φ.numVars) := Nat.mul_le_mul_left _ hφ + _ ≤ (A₁ * D + K) * φ.numVars := by nlinarith + · next hg => + have hgt : threshold φ.numVars < φ.length := by + simpa only [guard, decide_eq_true_eq, not_le] using hg + have hsmall : φ.numVars < 2 ^ 2 ^ D := by + by_contra hbig + have := mul_le_threshold (not_lt.mp hbig) + omega + have hn : 1 ≤ φ.numVars := by + rcases Nat.eq_zero_or_pos φ.numVars with h0 | h0 + · rw [h0] at hφ hgt; omega + · exact h0 + have hK' : ⌈(2 : ℝ) ^ ((A₂ : ℝ) * interpolationScale φ.numVars)⌉₊ ≤ K := + Finset.le_sup (f := fun n => ⌈(2 : ℝ) ^ ((A₂ : ℝ) * interpolationScale n)⌉₊) + (Finset.mem_range.mpr hsmall) + have hexp : K ≤ (A₁ * D + K) * φ.numVars / q φ := by + calc K ≤ A₁ * D + K := Nat.le_add_left _ _ + _ = (A₁ * D + K) * φ.numVars / φ.numVars := (Nat.mul_div_cancel _ hn).symm + _ ≤ (A₁ * D + K) * φ.numVars / q φ := + Nat.div_le_div_left (sqrt_log_le hn) (one_le_sqrt_log _) + calc ⌈(2 : ℝ) ^ ((A₂ : ℝ) * interpolationScale φ.numVars)⌉₊ * Y φ ^ e₀ + ≤ 2 ^ ((A₁ * D + K) * φ.numVars / q φ) * Y φ ^ e := + Nat.mul_le_mul (hK'.trans ((Nat.lt_two_pow_self).le.trans + (Nat.pow_le_pow_right (by norm_num) hexp))) (hYe φ) + +end Cslib.Complexity.DensityBranchCounting diff --git a/ComplexityTests/DensityBranchCounting.lean b/ComplexityTests/DensityBranchCounting.lean new file mode 100644 index 0000000000..a7fec19df1 --- /dev/null +++ b/ComplexityTests/DensityBranchCounting.lean @@ -0,0 +1,63 @@ +/- +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.DensityBranchCounting +import Complexity.Computability.Complexity.FineGrained.CountingNativeModelCount + +/-! # One model counter with both bounds of Theorem 1.1: checked instances + +The threshold `n ⌈log₂ ⌈log₂ n⌉⌉` at small sizes, formulas on either side of it, and the two +earlier counters recovered from the single one: its bound on every formula gives the +interpolation-scale counter, and its fixed-density bound gives the shape of the +tensor-contraction counter. -/ + +namespace ComplexityTests.DensityBranchCounting + +open Cslib.Logic.PL Cslib.Complexity Cslib.Complexity.DensityBranchCounting + Cslib.Complexity.SubexponentialSAT Turing.MultiTapeTM + +-- `λ = ⌈log₂ n⌉` and `ν = ⌈log₂ λ⌉`: `ν = 0` below three variables, then `1, 2, 3, …`. +example : threshold 2 = 0 ∧ threshold 3 = 3 ∧ threshold 4 = 4 ∧ threshold 16 = 32 ∧ + threshold 20 = 60 ∧ threshold 256 = 768 ∧ threshold 257 = 1028 := by decide + +/-- Four clauses on four variables: at the threshold, so the contraction branch. -/ +def sparse : CNF ℕ := [[(0, true), (1, true)], [(1, false), (2, true)], [(2, false), (3, true)], + [(3, false), (0, false)]] + +example : sparse.length ≤ threshold sparse.numVars := by decide + +/-- Three clauses on two variables: above the threshold `0`, so the dense branch. -/ +def dense : CNF ℕ := [[(0, true), (1, true)], [(0, false), (1, true)], [(0, true), (1, false)]] + +example : threshold dense.numVars < dense.length := by decide + +-- The single counter has the interpolation-scale bound of the Section 6.4 counter. +example (k : ℕ) : ∃ (count : CNF ℕ → ℕ) (A e b : ℕ), + (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) → count φ = φ.modelCount) ∧ + ComputableInO count encCNF encNat + (fun φ => ⌈(2 : ℝ) ^ ((A : ℝ) * interpolationScale φ.numVars)⌉₊ * + ((encCNF φ).length + 1) ^ e) + (fun φ => ((encCNF φ).length + 1) ^ b) := by + obtain ⟨count, T, S, A, e, b, hcount, hc, hS, hT, -, -⟩ := exists_modelCounter k + exact ⟨count, A, e, b, hcount, hc.mono_le hT fun φ => (hS φ).le⟩ + +-- The same counter, at each density, has the exponent `A (n + 1) / √⌊log₂ (n + 2)⌋` of the +-- fixed-density tensor-contraction counter. +example (k : ℕ) : ∃ (count : CNF ℕ → ℕ) (T S : CNF ℕ → ℕ) (e b : ℕ), + (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) → count φ = φ.modelCount) ∧ + ComputableInO count encCNF encNat T S ∧ + (∀ φ, S φ = ((encCNF φ).length + 1) ^ b) ∧ + ∀ D : ℕ, ∃ A : ℕ, ∀ φ : CNF ℕ, φ.length ≤ D * φ.numVars → + T φ ≤ 2 ^ (A * (φ.numVars + 1) / Nat.sqrt (Nat.log 2 (φ.numVars + 2))) * + ((encCNF φ).length + 1) ^ e := by + obtain ⟨count, T, S, A, e, b, hcount, hc, hS, -, -, hD⟩ := exists_modelCounter k + refine ⟨count, T, S, e, b, hcount, hc, hS, fun D => ?_⟩ + obtain ⟨A', hA'⟩ := hD D + exact ⟨A', fun φ hφ => (hA' φ hφ).trans (Nat.mul_le_mul_right _ + (Nat.pow_le_pow_right (by norm_num) (Nat.div_le_div_right (Nat.mul_le_mul_left _ + (Nat.le_succ _)))))⟩ + +end ComplexityTests.DensityBranchCounting diff --git a/ROADMAP.md b/ROADMAP.md index 0c5c4eba03..ee6ef2cea7 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -795,6 +795,12 @@ and credited. subexponential-time `k`-SAT, zero SAT exponents, `¬ETH`, and `¬SETH`. This is the Sections 3–6 and Appendices A–B interpolation-scale bound, not the sharper Appendix D runtime. Integration, validation, and the curated formal abstract are tracked in #1226. +- **The sharper Theorem 1.1 bound** ([#1538](https://github.com/cslib-community/complexitylib/issues/1538)): + `ContractionCounting.exists_modelCounter_fixedDensity` proves the fixed-density bound + `2^{O_{k,D}(n / √log n)}` by tensor contraction (Theorem D.1 with `ℓ = 1`), and + `DensityBranchCounting.exists_modelCounter` combines it with the interpolation-scale counter in + one machine. The arbitrary-density bound `2^{O_k(n log log n / √log n)}` still needs Theorem D.1 + with truncation order `ℓ = n + 1` and Lemma D.2. ## Documentation and repository From 0062da138a321e6a6767b05eaf518686cebca89d Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 08:52:02 -0400 Subject: [PATCH 3/4] style(TensorNetwork/ClauseNetwork): replace a non-terminal bare simp with simp only Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Circuit/Frontier/TensorNetwork/ClauseNetwork.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetwork.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetwork.lean index 61008dd754..03816a3c82 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetwork.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetwork.lean @@ -388,7 +388,7 @@ theorem vertices_network (B m : ℕ) : (network os B m).2.vertices = @[simp] theorem length_vertices_network (B m : ℕ) : (network os B m).2.vertices.length = m + 2 * os.length := by - simp [vertices_network] + simp only [vertices_network, List.length_append, List.length_map, List.length_range] omega private theorem sum_range_ite (m a : ℕ) (c : Prop) [Decidable c] : From e35c32299f9dc7a3780352fd6c4c195a93d67ed1 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 09:42:01 -0400 Subject: [PATCH 4/4] refactor(FineGrained): reuse the model-count bound and name occurrence components Address review of #2029: - `ClauseNetwork.var` and `ClauseNetwork.pol` destructure the occurrence by name instead of projecting `.2.2.1`/`.2.2.2`; both stay definitionally equal. - Move the general `modelCount_le_two_pow_numVars` from `FineGrained/CountingSparsification` to `CNF/ModelCount` as `CNF.modelCount_le_two_pow_numVars`, update its clients there and in `ThreeOccurrenceReduction`, and drop the duplicate `ContractionCounting.modelCount_le_two_pow`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Frontier/TensorNetwork/ClauseNetwork.lean | 8 ++++---- .../Complexity/FineGrained/ContractionCounting.lean | 8 +------- .../FineGrained/CountingSparsification.lean | 12 ++---------- .../FineGrained/ThreeOccurrenceReduction.lean | 2 +- Complexity/Logics/Propositional/CNF/ModelCount.lean | 9 +++++++++ 5 files changed, 17 insertions(+), 22 deletions(-) diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetwork.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetwork.lean index 03816a3c82..4b8ceb8446 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetwork.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/ClauseNetwork.lean @@ -115,10 +115,10 @@ end. -/ @[expose] def occ (u : ℕ) : Occurrence ℕ := os.getD u (0, 0, (0, false)) /-- The variable of occurrence `u`. -/ -@[expose] def var (u : ℕ) : ℕ := (occ os u).2.2.1 +@[expose] def var (u : ℕ) : ℕ := let (_, _, (v, _)) := occ os u; v /-- The polarity of occurrence `u`. -/ -@[expose] def pol (u : ℕ) : Bool := (occ os u).2.2.2 +@[expose] def pol (u : ℕ) : Bool := let (_, _, (_, b)) := occ os u; b /-- The clause of occurrence `u`. -/ @[expose] def clauseOf (u : ℕ) : ℕ := (occ os u).1 @@ -742,8 +742,8 @@ private theorem good_iff have h3u : 3 * u ∈ clausePorts os i := mem_clausePorts.mpr ⟨u, hu, hci, rfl⟩ have := hall _ h3u rw [hX _ (by omega), show 3 * u / 3 = u by omega] at this - have hv : var os u = l.1 := by rw [var, hocc] - have hp : pol os u = l.2 := by rw [pol, hocc] + have hv : var os u = l.1 := congrArg Prod.fst hocc + have hp : pol os u = l.2 := congrArg Prod.snd hocc rw [hv, hp, hsl] at this cases l.2 <;> simp at this · rw [hX _ (by omega), hX _ (by omega), show (3 * u + 1) / 3 = u by omega, diff --git a/Complexity/Computability/Complexity/FineGrained/ContractionCounting.lean b/Complexity/Computability/Complexity/FineGrained/ContractionCounting.lean index b4b4b80b78..abfbca7ba2 100644 --- a/Complexity/Computability/Complexity/FineGrained/ContractionCounting.lean +++ b/Complexity/Computability/Complexity/FineGrained/ContractionCounting.lean @@ -126,12 +126,6 @@ theorem guard_eq_true_iff {k : ℕ} {φ : CNF ℕ} : guard k φ = true ↔ φ ≠ [] ∧ ∀ c ∈ φ, 1 ≤ c.length ∧ c.length ≤ k := by simp [guard] -/-- A formula has at most `2 ^ n` satisfying assignments of its `n` variables. -/ -theorem modelCount_le_two_pow (φ : CNF ℕ) : φ.modelCount ≤ 2 ^ φ.numVars := by - unfold CNF.modelCount CNF.numVars - refine (Finset.card_filter_le _ _).trans ?_ - simp only [Finset.card_univ, Fintype.card_fun, Fintype.card_bool, Fintype.card_coe, le_refl] - /-- A formula whose clauses are nonempty has at least as many literals as clauses. -/ theorem length_le_length_vars {φ : CNF ℕ} (h : ∀ c ∈ φ, 1 ≤ c.length) : φ.length ≤ φ.vars.length := by @@ -152,7 +146,7 @@ theorem count_eq {k : ℕ} {φ : CNF ℕ} (hk : ∀ c ∈ φ, c.length ≤ k) : · next hg => obtain ⟨hne, hcl⟩ := guard_eq_true_iff.mp hg rw [contraction_clauseNetwork hk] - refine Nat.mod_eq_of_lt ((modelCount_le_two_pow φ).trans_lt ?_) + refine Nat.mod_eq_of_lt (φ.modelCount_le_two_pow_numVars.trans_lt ?_) have h1 : 1 ≤ φ.length := List.length_pos_iff.mpr hne have h2 := length_le_length_vars fun c hc => (hcl c hc).1 have h3 := CNF.numVars_le_length_vars φ diff --git a/Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean b/Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean index 374789ba31..ae0d44c7c0 100644 --- a/Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean +++ b/Complexity/Computability/Complexity/FineGrained/CountingSparsification.lean @@ -121,15 +121,7 @@ namespace CountingSparsify open ClauseSet.Sparsification (CountingBranchingRule) -/-! ### Auxiliary model-count and binary-encoding bounds -/ - -/-- The number of satisfying assignments of `ψ` on its occurring variables is at most -`2 ^ ψ.numVars`. -/ -theorem modelCount_le_two_pow_numVars {V : Type*} [DecidableEq V] (ψ : CNF V) : - ψ.modelCount ≤ 2 ^ ψ.numVars := by - rw [CNF.modelCount, CNF.numVars] - refine (Finset.card_filter_le _ _).trans ?_ - simp only [Finset.card_univ, Fintype.card_fun, Fintype.card_bool, Fintype.card_coe, le_rfl] +/-! ### Auxiliary binary-encoding bound -/ theorem length_encNat_le_of_le_two_pow {acc n : ℕ} (h : acc ≤ 2 ^ n) : (encNat acc).length ≤ n + 1 := by @@ -473,7 +465,7 @@ theorem search_eq_ite_modelCount_of_normalized (hM2 : 2 ≤ M) {k B L_coeff : unfold root split_ifs with hφ · rw [modelCountOn_countingNormalize, CNF.modelCountOn_vars] - exact Nat.min_eq_right (modelCount_le_two_pow_numVars φ) + exact Nat.min_eq_right φ.modelCount_le_two_pow_numVars · rw [CNF.modelCountOn_eq_zero_of_nil_mem (List.mem_singleton_self [])] exact Nat.min_eq_right (Nat.zero_le _) diff --git a/Complexity/Computability/Complexity/FineGrained/ThreeOccurrenceReduction.lean b/Complexity/Computability/Complexity/FineGrained/ThreeOccurrenceReduction.lean index af6e75089e..3f27a0deb2 100644 --- a/Complexity/Computability/Complexity/FineGrained/ThreeOccurrenceReduction.lean +++ b/Complexity/Computability/Complexity/FineGrained/ThreeOccurrenceReduction.lean @@ -320,7 +320,7 @@ theorem guardOccurrenceCounter_le_two_pow_numVars {k : ℕ} (hk : 2 ≤ k) {f : guardOccurrenceCounter k f ψ ≤ 2 ^ ψ.numVars := by rw [guardOccurrenceCounter_eq_ite_modelCount hk hf ψ] split_ifs - · exact CountingSparsify.modelCount_le_two_pow_numVars ψ + · exact ψ.modelCount_le_two_pow_numVars · exact Nat.zero_le _ /-- When `f` counts dense width-`≤ k`, occurrence-`≤ 3` formulas (`2 ≤ k`), diff --git a/Complexity/Logics/Propositional/CNF/ModelCount.lean b/Complexity/Logics/Propositional/CNF/ModelCount.lean index 1594bcc409..36b82c93e8 100644 --- a/Complexity/Logics/Propositional/CNF/ModelCount.lean +++ b/Complexity/Logics/Propositional/CNF/ModelCount.lean @@ -11,6 +11,7 @@ public import Complexity.Foundations.Data.List.SelectDistinct public import Complexity.Logics.Propositional.CNF public import Mathlib.Data.Fintype.Pi public import Mathlib.Data.Nat.Bitwise +import Mathlib.Data.Fintype.BigOperators /-! # Counting satisfying assignments @@ -57,6 +58,8 @@ with a given one on the variables of the formula (`CNF.modelCount_eq_one_iff`). * `Cslib.Logic.PL.exists_lt_two_pow_bitsAssignment_eq`, `Cslib.Logic.PL.CNF.satisfiable_iff_exists_bitsAssignment`: satisfiability is a search over `2 ^ |vs|` numbered assignments. +* `Cslib.Logic.PL.CNF.modelCount_le_two_pow_numVars`: at most `2 ^ φ.numVars` satisfying + assignments. * `Cslib.Logic.PL.CNF.modelCount_eq_card_filter`: counting satisfying assignments through a map. * `Cslib.Logic.PL.CNF.modelCount_pos_iff`, `Cslib.Logic.PL.CNF.modelCount_eq_one_iff`. @@ -199,6 +202,12 @@ in `φ` that satisfy it. -/ def CNF.modelCount (φ : CNF V) : ℕ := (Finset.univ.filter fun τ : φ.vars.toFinset → Bool => φ.eval (φ.extendAssignment τ) = true).card +/-- A formula has at most `2 ^ φ.numVars` satisfying assignments of its occurring variables. -/ +theorem CNF.modelCount_le_two_pow_numVars (φ : CNF V) : φ.modelCount ≤ 2 ^ φ.numVars := by + rw [CNF.modelCount, CNF.numVars] + refine (Finset.card_filter_le _ _).trans ?_ + simp only [Finset.card_univ, Fintype.card_fun, Fintype.card_bool, Fintype.card_coe, le_rfl] + /-- An assignment of all variables satisfies `φ` exactly when its restriction to the variables of `φ`, extended by `false`, does. -/ theorem CNF.eval_extendAssignment_restrict (φ : CNF V) (σ : V → Bool) :