claimroutine
Clause network as bipartite tensor network
Statement (paper)
From a -CNF on declared variables with clauses one can build, in time polynomial in , a bipartite Boolean tensor network with vertices and edges and maximum degree at most , whose local tables are of size bounded in terms of , such that (after discarding tautologies, and when no clause is empty) its contraction equals the number of satisfying assignments of restricted to the variables occurring in ; if has an empty clause, then .
In plain English
A -CNF with variables and clauses can be converted in polynomial time into a bipartite Boolean tensor network with vertices and edges, maximum degree at most , and -bounded local tables, whose contraction equals the number of satisfying assignments over the variables that occur in (after dropping tautologies); an empty clause gives .
Why it's here
This reduces model counting to tensor network contraction, so the paper's contraction theorem can be applied to -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}.