Subexponential model counting for bounded-width CNF formulas

For every fixed clause width k, one native machine computes the number of satisfying assignments CNF.modelCount φ of every formula φ with clauses of at most k literals. It runs in time 2 ^ (A * interpolationScale n) times a polynomial in the encoding length, where n = φ.numVars, and in space polynomial in the encoding length.

This restates CountingNativeEndpoint.exists_declaredCounter on the plain formula: the machine relabels the variables densely, declares their number, and runs the declared counter. The resource bounds are folded into ComputableInO.

More generally:

• CountingNativeEndpoint.exists_counter_of_polyTime_toDeclared composes CountingNativeEndpoint.exists_declaredCounter with any polynomial-time reduction g : α → ℕ × CNF ℕ and polynomial-time validity guard valid : α → Bool.
• CountingNativeEndpoint.exists_shiftedCounter_of_polyTime_toCNF composes CountingNativeEndpoint.exists_modelCounter with any polynomial-time CNF compilation φ : α → CNF ℕ, unary binary-power shift shift : α → ℕ, validity guard valid : α → Bool, and linear variable-count bound (φ x).numVars ≤ C * μ x + D, multiplying (φ x).modelCount by 2 ^ shift x in binary while rescaling the subexponential rate to μ x.

Main results

• CountingNativeEndpoint.exists_counter_of_polyTime_toDeclared: compose the declared k-CNF counter with any polynomial-time reduction and validity guard.
• CountingNativeEndpoint.exists_modelCounter: the bounded-width model counter.
• CountingNativeEndpoint.exists_shiftedCounter_of_polyTime_toCNF: compose the bounded-width model counter with a 2 ^ shift factor and a linear numVars ≤ C * μ + D rescaling.

References

• OpenAI, The Exponential Time Hypothesis is False, Proposition 6.4.

theorem Cslib.Complexity.CountingNativeEndpoint.exists_counter_of_polyTime_toDeclared {α : Type} {encA : α ↪ List Bool} (k : ℕ) {g : α → ℕ × Logic.PL.CNF ℕ} (hg : Turing.MultiTapeTM.ComputableInPolyTime g encA (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encCNF)) {valid : α → Bool} (hvalid : Turing.MultiTapeTM.ComputableInPolyTime valid encA Turing.MultiTapeTM.encBool) (hvalid_imp : ∀ (x : α), valid x = true → Logic.PL.CNF.validDeclaredInput k (g x).1 (g x).2 = true) : ∃ (count : α → ℕ) (T : α → ℕ) (S : α → ℕ) (A : ℕ) (c : ℕ) (e : ℕ) (a : ℕ) (b : ℕ), Turing.MultiTapeTM.ComputableInO count encA Turing.MultiTapeTM.encNat T S ∧ (∀ (x : α), count x = if valid x = true then (g x).2.modelCountOn (Finset.range (g x).1) else 0) ∧ (∀ (x : α), ↑(T x) ≤ ↑c * (2 ^ (↑A * SubexponentialSAT.interpolationScale (g x).1) * (↑(encA x).length + 1) ^ e) + ↑c) ∧ ∀ (x : α), S x ≤ a * ((encA x).length + 1) ^ b

General composition of CountingNativeEndpoint.exists_declaredCounter with any polynomial-time reduction g : α → ℕ × CNF ℕ and polynomial-time validity guard valid : α → Bool.

theorem Cslib.Complexity.CountingNativeEndpoint.exists_modelCounter (k : ℕ) : ∃ (count : Logic.PL.CNF ℕ → ℕ) (A : ℕ) (e : ℕ) (b : ℕ), (∀ (φ : Logic.PL.CNF ℕ), (∀ c ∈ φ, List.length c ≤ k) → count φ = φ.modelCount) ∧ Turing.MultiTapeTM.ComputableInO count encCNF Turing.MultiTapeTM.encNat (fun (φ : Logic.PL.CNF ℕ) => ⌈2 ^ (↑A * SubexponentialSAT.interpolationScale φ.numVars)⌉₊ * ((encCNF φ).length + 1) ^ e) fun (φ : Logic.PL.CNF ℕ) => ((encCNF φ).length + 1) ^ b

Subexponential bounded-width model counting. For each width k, one machine computes φ.modelCount on every formula φ whose clauses have at most k literals, in time 2 ^ (A * interpolationScale φ.numVars) times a polynomial in the encoding length, and in polynomial space.

theorem Cslib.Complexity.CountingNativeEndpoint.exists_shiftedCounter_of_polyTime_toCNF {α : Type} {encA : α ↪ List Bool} (k : ℕ) {φ : α → Logic.PL.CNF ℕ} (hφ : Turing.MultiTapeTM.ComputableInPolyTime φ encA encCNF) {shift : α → ℕ} (hshift : Turing.MultiTapeTM.ComputableInPolyTime shift encA Turing.MultiTapeTM.encUnary) {valid : α → Bool} (hvalid : Turing.MultiTapeTM.ComputableInPolyTime valid encA Turing.MultiTapeTM.encBool) (μ : α → ℕ) (C D : ℕ) (hvalid_imp : ∀ (x : α), valid x = true → (∀ cl ∈ φ x, List.length cl ≤ k) ∧ (φ x).numVars ≤ C * μ x + D) : ∃ (count : α → ℕ) (A : ℕ) (e : ℕ) (b : ℕ), (∀ (x : α), count x = if valid x = true then 2 ^ shift x * (φ x).modelCount else 0) ∧ Turing.MultiTapeTM.ComputableInO count encA Turing.MultiTapeTM.encNat (fun (x : α) => ⌈2 ^ (↑A * SubexponentialSAT.interpolationScale (μ x))⌉₊ * ((encA x).length + 1) ^ e) fun (x : α) => ((encA x).length + 1) ^ b

Compose CountingNativeEndpoint.exists_modelCounter with a polynomial-time CNF compilation φ : α → CNF ℕ, a polynomial-time unary binary-exponent shift shift : α → ℕ, a polynomial-time validity guard valid : α → Bool, and a linear variable-count bound (φ x).numVars ≤ C * μ x + D under valid x = true, multiplying (φ x).modelCount in binary by 2 ^ shift x while rescaling the interpolationScale exponent to μ x.