theoremnovelstructure_uncertain

Subexponential deterministic k-CNF model counting

Theorem·thm:main·§1 Introduction

Statement (paper)

For each fixed

k\ge2

, there exists a deterministic algorithm that, given a

k

-CNF

F

n\ge20

declared variables with

m

clauses, computes

\#F

as defined in in

(n+m)^{O_k(1)}2^{O_k(n\log\log n/\sqrt{\log n})}

bit operations and

(n+m)^{O_k(1)}

bits of space. For each fixed

D>0

, its running time on inputs with

m\le Dn

(n+m)^{O_{k,D}(1)}2^{O_{k,D}(n/\sqrt{\log n})}.

In plain English

For each fixed

k\ge2

, a deterministic algorithm counts the satisfying assignments

\#F

of a

k

-CNF on

n\ge20

variables with

m

clauses in

(n+m)^{O_k(1)}2^{O_k(n\log\log n/\sqrt{\log n})}

time and polynomial space. If

m\le Dn

for a fixed

D

, the time improves to

(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

2^{o(n)}

algorithm for

k

-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

2^{o(n)}

algorithm for

k

-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)n}

-type exponential, and no subexponential algorithm was known for even

k

-SAT decision.

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

Selected node

Statement (paper)

In plain English

Why it's here

Inside the proof