claimroutine

Clause network as bipartite tensor network

Claim·§D.2 Fixed clause density·inside thmSubexponential deterministic k-CNF model counting

Statement (paper)

From a

k

-CNF

F

n

declared variables with

m

clauses one can build, in time polynomial in

n+m

, a bipartite Boolean tensor network with

O_k(n+m)

vertices and edges and maximum degree at most

\max\{k,3\}

, whose local tables are of size bounded in terms of

k

, such that (after discarding tautologies, and when no clause is empty) its contraction equals the number of satisfying assignments of

F

restricted to the variables occurring in

F

; if

F

has an empty clause, then

\#F=0

In plain English

k

-CNF with

n

variables and

m

clauses can be converted in polynomial time into a bipartite Boolean tensor network with

O_k(n+m)

vertices and edges, maximum degree at most

\max\{k,3\}

, and

k

-bounded local tables, whose contraction equals the number of satisfying assignments over the variables that occur in

F

(after dropping tautologies); an empty clause gives

\#F=0

Why it's here

This reduces model counting to tensor network contraction, so the paper's contraction theorem can be applied to

k

-CNFs. Variables and clauses become the two sides of the bipartite graph, and the degree and table-size bounds are what that theorem needs in order to give the fixed-density running time in the next claim.

Classified routine:

This is the standard encoding of a CNF as a tensor network or factor graph, with clause tables and variable copy/equality tensors. Degree reduction by splitting high-occurrence variables into chains of equality tensors, as in counting CSPs via tensor network contraction (e.g. Markov–Shi 2008), keeps the maximum degree at most max{k,3}.

Uses

Nothing else in the paper

Used by

claimFixed-density counting via tensor contraction

Sources

PaperOpen

Section: §D.2 Fixed clause density
Page: —
Label: —
Line: quantitative-reduction.tex:68

Leannot aligned

Phase 2 aligns this node to a Lean declaration.