theoremnovelstructure_uncertain

Subexponential deterministic k-CNF model counting

Theorem·thm:main·§1 Introduction

Statement (paper)

For each fixed k⩾2k\ge2, there exists a deterministic algorithm that, given a kk-CNF FF on n⩾20n\ge20 declared variables with mm clauses, computes #F\#F as defined in in (n+m)Ok(1)2Ok(nlog⁡log⁡n/log⁡n) (n+m)^{O_k(1)}2^{O_k(n\log\log n/\sqrt{\log n})} bit operations and (n+m)Ok(1)(n+m)^{O_k(1)} bits of space. For each fixed D>0D>0, its running time on inputs with m⩽Dnm\le Dn is (n+m)Ok,D(1)2Ok,D(n/log⁡n). (n+m)^{O_{k,D}(1)}2^{O_{k,D}(n/\sqrt{\log n})}.

In plain English

For each fixed k⩾2k\ge2, a deterministic algorithm counts the satisfying assignments #F\#F of a kk-CNF on n⩾20n\ge20 variables with mm clauses in (n+m)Ok(1)2Ok(nlog⁡log⁡n/log⁡n)(n+m)^{O_k(1)}2^{O_k(n\log\log n/\sqrt{\log n})} time and polynomial space. If m⩽Dnm\le Dn for a fixed DD, the time improves to (n+m)Ok,D(1)2Ok,D(n/log⁡n)(n+m)^{O_{k,D}(1)}2^{O_{k,D}(n/\sqrt{\log n})}.

Why it's here

This is the paper's main theorem, refuting the Exponential Time Hypothesis by giving a 2o(n)2^{o(n)} algorithm for kk-CNF counting. The fixed-density case follows by encoding the formula as a bipartite tensor network and applying the contraction theorem. The general case sparsifies the formula into bounded-occurrence leaves and counts each leaf via sparse parity checks and sparse-system zero-counting queries, with the costs summed over the tree.
Classified novel:
This is the paper's headline claim: a deterministic 2o(n)2^{o(n)} algorithm for kk-CNF model counting. Nothing prior gives one; the best known algorithms (e.g., PPSZ-type bounds and the Impagliazzo–Paturi–Zane sparsification framework) remain 2(1−c/k)n2^{(1-c/k)n}-type exponential, and no subexponential algorithm was known for even kk-SAT decision.

Uses

thmSubexponential Boolean tensor network contractionlemSparsification into bounded-occurrence k-CNF leaveslemSparse parity checks force large supportslemGreedy appended rows give exact countlemCounting zeros of sparse polynomial systems

Used by

corRandomized approximate Max-k-SAT in subexponential timecorSubexponential counting for graph problemscorSuperlinear circuit lower bound for E^NPcorLinear-size circuit lower bound for E^NPcorFast inversion of local Boolean mapsclaimFast 3-SAT at linear clause density

Inside the proof

claimClause network as bipartite tensor networkclaimFixed-density counting via tensor contractionclaimSparsify with sigma about 1/sqrt(log n)claimLeaf counts via parity rows and queriesclaimArbitrary-density time and space accounting

Sources

PaperOpen
Section
§1 Introduction
Page
—
Label
thm:main
Line
main_full_version.tex:73
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    structure_uncertain
    Skeleton records only the fixed-density proof (quantitative-reduction.tex:67-98); a second proof of the arbitrary-density bound is at quantitative-reduction.tex:317-361, and the combined single algorithm is described at 363-369.
  • info
    structure_uncertain
    claim "Sparsify with sigma about 1/sqrt(log n)" (quantitative-reduction.tex:319-328) lies outside the recorded proof; a second proof or an appendix
  • info
    structure_uncertain
    claim "Leaf counts via parity rows and contraction queries" (quantitative-reduction.tex:330-345) lies outside the recorded proof; a second proof or an appendix
  • info
    structure_uncertain
    claim "Arbitrary-density time and space accounting" (quantitative-reduction.tex:347-360) lies outside the recorded proof; a second proof or an appendix