<p><a href="http://link.springer.com/chapter/10.1007/11750321_34?LI=true">#3-Regular Bipartite Planar Vertex Cover is #P-Complete</a></p>

<p>As counting vertex covers is exactly the same as counting satisfying assignments of a <em>monotone</em> #2-SAT instance, the above result implies that it is #P-complete to count satisfying assignments of a #2-SAT instance which is <em>monotone</em> and <em>3-regular</em> and <em>bipartite</em> and <em>planar</em>.</p>

<p>This in turn means that, in addition to the two #2-MONOTONE-SAT and #2-BIPARTITE-SAT special cases already cited in the question, the two #2-CUBIC-SAT and #2-PLANAR-SAT special cases are #P-complete as well.</p>

CC BY-SA 3.0
2012-11-29T14:02:48.473Z
2012-11-29T14:02:48.473Z
Giorgio Camerani
<p>Despite being 11 years late I hope I can still claim the bonus points! There is an (IMHO) simple and direct reduction from #SAT to #BIPARTITE-2SAT that does not rely on monotone instances. This appears in <a href="https://arxiv.org/abs/2304.02524" rel="nofollow noreferrer">arXiv:2304.02524</a> by myself, Konstantinos Meichanetzidis, and John van de Wetering.</p>
<p>Given <span class="math-container">$r \in \mathbb{N}$</span> and <span class="math-container">$f : \mathbb{B}^n \to \mathbb{B}$</span> a CNF formula with <span class="math-container">$n$</span> variables and <span class="math-container">$m$</span> clauses, there is a bipartite 2-CNF <span class="math-container">$f'$</span> with <span class="math-container">$O(n + mr)$</span> variables such that
<span class="math-container">$$|\{x \in \mathbb{B}^n \mid f(x) = 1\}| \equiv |\{x \in \mathbb{B}^n \mid f'(x) = 1\}| \pmod{2^r + 1}$$</span>
Now suppose we have an oracle for #BIPARTITE-2SAT. Then since <span class="math-container">$|\{x \in \mathbb{B}^n \mid f(x) = 1\}| &lt; 2^n + 1$</span>, if we set <span class="math-container">$r = n$</span> then we can recover this value exactly from <span class="math-container">$|\{x \in \mathbb{B}^n \mid f'(x) = 1\}|$</span>, which we can compute using the oracle. This gives a reduction from #SAT to #BIPARTITE-2SAT.</p>
<p>We can construct <span class="math-container">$f'$</span> from <span class="math-container">$f$</span> as follows:</p>
<ol>
<li>For each variable <span class="math-container">$x_i$</span> of <span class="math-container">$f$</span>, add a variable <span class="math-container">$x_i'$</span> to <span class="math-container">$f'$</span></li>
<li>For each clause <span class="math-container">$C_j$</span> of <span class="math-container">$f$</span>, add a variable <span class="math-container">$y_j'$</span> to <span class="math-container">$f'$</span></li>
<li>For each <span class="math-container">$y_j'$</span> add variables <span class="math-container">$z'_{j1}, z'_{j2}, \dots, z'_{jr}$</span> and clauses <span class="math-container">$(y_j' \lor \lnot z'_{j1}) \land (y_j' \lor \lnot z'_{j2}) \land \cdots \land (y_j' \lor \lnot z'_{jr})$</span> to <span class="math-container">$f'$</span>,</li>
<li>For every <span class="math-container">$i$</span> and <span class="math-container">$j$</span>:
<ul>
<li>If <span class="math-container">$x_i$</span> occurs in <span class="math-container">$C_j$</span>, add <span class="math-container">$\lnot x'_i \lor \lnot y'_j$</span> to <span class="math-container">$f'$</span></li>
<li>If <span class="math-container">$\lnot x_i$</span> occurs in <span class="math-container">$C_j$</span> add <span class="math-container">$x'_i \lor \lnot y'_j$</span> to <span class="math-container">$f'$</span></li>
</ul>
</li>
</ol>
<p>Clearly <span class="math-container">$f'$</span> is bipartite because it can be partitioned as <span class="math-container">$\{x'_i\} \cup \{z'_{jl}\}$</span> and <span class="math-container">$\{y'_j\}$</span>.</p>
<p>This generalizes the reduction given by Giorgio Camerani in <a href="https://cstheory.stackexchange.com/questions/39598/%e2%8a%95p-completeness-of-%e2%8a%952sat/48282#48282">this answer</a> about <span class="math-container">$\oplus$</span>2SAT (they are the same when <span class="math-container">$r = 0$</span>).</p>
<p>As to why this works.. in the paper (see Lemma 3 for details), we show this using the ZH calculus, which is a formal system of diagrammatic reasoning about tensor networks. In this framework, the derivation of this construction is:
<a href="https://i.sstatic.net/xObs9.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/xObs9.png" alt="graphical proof for the construction of f'" /></a>
Here, the yellow boxes with zeros are negated clauses, white dots are variables, and grey dots are negations. I'd encourage anyone interested to have a look at the ZH calculus! (of course, the OP was an author of the predecessor to this paper, so knows all about this..)</p>
<p>I prefer the graphical presentation, but it is also possible to given an explanation in words: the intuition for why this works is that the subformula <span class="math-container">$f''$</span> of <span class="math-container">$f'$</span> generated by only the <span class="math-container">$x'_i$</span>s and <span class="math-container">$y'_j$</span>s is essentially a weighted CNF - for every satisfying assignment of <span class="math-container">$f''$</span>, if any <span class="math-container">$y'_j$</span> is assigned true then there are <span class="math-container">$2^r$</span> ways to assign the <span class="math-container">$z'_{jl}$</span>s to make <span class="math-container">$f'$</span> true, and if <span class="math-container">$y'_j$</span> is false then there is only one way to assign the <span class="math-container">$z'_{jl}$</span>s. Thus we can treat <span class="math-container">$f''$</span> as a weighted CNF where the <span class="math-container">$y'_j$</span>s are given weight <span class="math-container">$2^r$</span>. However, <span class="math-container">$2^r \equiv -1 \mod 2^r + 1$</span>, so we can think of these as having weight <span class="math-container">$-1$</span>.</p>
<p>If <span class="math-container">$y'_j$</span> is false, then no further restrictions are imposed on the <span class="math-container">$x'_i$</span>s. This is as if <span class="math-container">$C_j$</span> did not exist. If <span class="math-container">$y'_j$</span> is true then we assert that the <span class="math-container">$x'_i$</span>s must appear with opposite polarity than they do in <span class="math-container">$C_j$</span>. But this is exactly the condition for <span class="math-container">$C_j$</span> to be unsatisfied! Since <span class="math-container">$y'_j$</span> has weight <span class="math-container">$-1$</span>, the total number of solutions of <span class="math-container">$f''$</span> is the number of solutions where <span class="math-container">$y'_j$</span> is false (and <span class="math-container">$C_j$</span> does not exist), minus the number of solutions <span class="math-container">$y'_j$</span> is true (and <span class="math-container">$C_j$</span> is unsatisfied). Therefore it is exactly the number of solutions where <span class="math-container">$C_j$</span> is satisfied! This applies to every <span class="math-container">$j$</span>, so that the total number of solutions of <span class="math-container">$f'$</span> (mod <span class="math-container">$2^r + 1$</span>) is the same as <span class="math-container">$f$</span>.</p>
<p>I suppose the moral of the story here is that counting is probably hard when the structure of the formulae is not sufficiently constrained to prevent you from putting weights on variables. If you can do that, then you can maybe reconstruct other structure, including arbitrarily large clauses. It seems that the bipartite structure in this case is not intrinsic to the argument but instead an artifact of the fact that the incidence graph of a #SAT instance is naturally bipartite.</p>
<p>For example, in the paper, we also used this weight-and-modulo trick to reduce from #SAT to #MONOTONE-2SAT (modulus <span class="math-container">$2^r$</span>), #2SAT with degree at most three (Fibonacci number modulus), #PERFECT-MATCHINGS (modulus <span class="math-container">$2^r + 1$</span>). And even if you can't show that counting for a particular structure of formula is #P-hard in this way, it might be sufficient to show modulo an integer to obtain at least NP-hardness. For example, if you set <span class="math-container">$r = 0$</span> in the reduction above, you get a reduction from <span class="math-container">$\oplus$</span>SAT to <span class="math-container">$\oplus$</span>2SAT, showing that #2SAT is at least NP-hard (under randomized reductions) by the Valiant-Vazirani theorem.</p>

CC BY-SA 4.0
2023-04-14T15:57:33.853Z
Your item 4 in the construction of $f'$ is weird, it will always propagate the fact that $y'_j = 0$. Did you mean $\vee$ instead of $\wedge$?
holf
CC BY-SA 4.0
2023-04-14T18:23:59.763Z
@holf ah yes I did, fixed. Thanks!
Tuomas Laakkonen
CC BY-SA 4.0
2023-04-17T19:25:01.480Z
how does this not solve SAT? You get O(n+mn) 2-SAT with 0 solutions iff SAT has 0 solutions
Noone AtAll
CC BY-SA 4.0
2023-04-18T05:07:55.020Z
No, $f$ may be unsat and $f'$ has $k(2^r+1)$ solutions for some $k$ hence $\#f = 0 = k(2^r+1) \mathsf{~mod~} (2^r+1) = \#f'$. This is actually a very elegant reduction!
holf
CC BY-SA 4.0
2023-05-27T08:56:59.083Z
@TuomasLaakkonen If I take your $f'$ construction and ignore Step 3, what I get is exactly the same as mentioned in the first half of my answer https://cstheory.stackexchange.com/a/48282/947, which is precisely what I was referring to in my above comment to this question.
Giorgio Camerani
CC BY-SA 4.0
2023-05-27T15:17:04.743Z
@GiorgioCamerani Ah indeed, I missed that answer before! I've added a line explaining the connection
Tuomas Laakkonen
CC BY-SA 4.0
2023-05-27T17:36:45.163Z
@TuomasLaakkonen Thanks, and congratulations for your weight-and-modulo trick, I've found it truly clever. Indeed, it blows every unsatisfying assignment $u$ of $f$ into $(2^n+1)^\mu$ satisfying assignments of $f'$, where $\mu$ is the number of clauses of $f$ that are not satisfied by $u$. Such blown-up satisfying assignments of $f'$ are then sheared off by the modulo, leaving all and only the satisfying assignments of $f'$ that truly correspond to satisfying assignments of $f$.
Giorgio Camerani
CC BY-SA 4.0
2023-07-04T14:52:50.587Z
If you eliminate the $y'_j$ variables and directly add $\pm x'_i\lor\neg z'_{jk}$, $k=1,\dots,r$ in step 4 instead of $\pm x'_i\lor\neg y'_j$ and $y'_j\lor\neg z'_{jk}$, the number of satisfying assignments of the new formula will be congruent to the original one modulo $2^r$ rather than modulo $2^r+1$. I find that more convenient.
Emil Jeřábek
CC BY-SA 4.0
2023-07-04T16:36:36.470Z
@EmilJeřábek Indeed, that works too (e.g it's used as proof of Lemma 5 in the paper), personally I like the construction above because I think it generalizes nicely to the case where we want to compute the number of solutions mod M for arbitrary M.
Tuomas Laakkonen
CC BY-SA 4.0
2023-04-14T10:00:55.847Z
2023-05-27T15:16:24.170Z
2023-05-27T15:16:24.170Z
Tuomas Laakkonen
<p><strong>Short version.</strong></p>

<p>The original proof that #2-SAT is <strong>#P</strong>-complete shows, in fact, that those instances of #2-SAT which are both <em>monotone</em> (not involving the negations of any variables) and <em>bipartite</em> (the graph formed by the clauses over the variables is a bipartite graph) are <strong>#P</strong>-hard. Thus, the two special cases #2-MONOTONE-SAT and #2-BIPARTITE-SAT are <strong>#P</strong>-hard. Are there other special cases which can be characterized in terms of 'natural' properties of the formula, which are also <strong>#P</strong>-hard?</p>

<p><strong>Long version.</strong></p>

<p>The problem #2-SAT is the task of computing &mdash; for a boolean formula $\phi$ consisting of the conjunction of several clauses, where each clause is a disjunction of two literals $x_j$ or $\bar x_j$ &mdash; the number of boolean strings $x \in \{0,1\}^n$ such that $\phi(x) = 1$. Finding out whether or not there <em>exists</em> such an $x$ is easy; but counting the number of solutions in general is <strong>#P</strong>-complete, as shown by Valiant in <a href="http://epubs.siam.org/doi/abs/10.1137/0208032">The Complexity of Enumeration and Reliability Problems, SIAM J. Comput., <strong>8</strong>, pp.&nbsp;410–421</a>.</p>

<p>For the case of #2-SAT in particular, what Valiant actually shows is a reduction to #2-SAT from counting matchings (including imperfect ones) in bipartite graphs, which gives rise to instances of #2-SAT with a very particular structure, as follows.</p>

<ol>
<li><p>First, note that the monotone problem is equivalent, by substitution, to the problem in which for each variable $x_j$, either $x_j$ occurs in the formula $\phi$ or $\bar x_j$ does but not both. In particular, the "monotone decreasing" problem in which <em>only</em> the negations $\bar x_j$ occur for every variable is exactly as hard as the monotone case.</p></li>
<li><p>For any graph $G = (V,E)$ with $m$ edges, we can construct a monotone-decreasing 2-SAT formula corresponding to matchings &mdash; collections of edges which do not share any vertices &mdash; by assigning a variable $x_e$ to each edge, representing whether it is included in an edge-set; the property of a set $M \subseteq E$ being a matching is equivalent to the incidence vector $\mathbf x = \chi_M$ satisfying the CNF formula $\phi$ whose clauses are given by $(\bar x_e \vee \bar x_f)$ for every pair of edges $e, f \in E$ which share a vertex.
By construction, $\phi$ has as many satisfying solutions $\mathbf x \in \{0,1\}^m$ as there are (possibly imperfect) matchings in the graph $G$.</p></li>
<li><p>If the graph $G$ for which we want to count the matchings is bipartite, then it contains no odd cycles &mdash; which we can describe as a sequence of <em>edges</em> in the graph which starts and ends with the same edge (without counting that final edge twice). Then there are no sequence of variables $x_e, x_f, x_g, \ldots, x_e$ of odd length in $\phi$, in which adjacent variables are involved in a common clause. Then the formula $\phi$ would be bipartite in the manner described earlier.</p></li>
<li><p>Counting the number of matchings in arbitrary bipartite graphs, in particular, can be used to count the number of perfect matchings in a bipartite graph: given an input bitrarite graph $G = (A \cup B, E)$ with two bipartitions $A, B$ of the same size $n$, one can create graphs $G_k$ by augmenting $A$ with anywhere $0 \leqslant k \leqslant n$ extra vertices connected to all of the vertices of $B$. Because all matchings in $G$ of a given size contribute differently to the number of matchings in $G_k$, by counting these one can determine the number of matchings in $G$ of size $n$ (that is, which are perfect matchings); and note that counting the number of perfect matchings in bipartite graphs is equivalent to computing permanents of $\{0,1\}$-matrices by a simple correspondance.</p></li>
</ol>

<p>The class of instances of #2-SAT which are shown to be <strong>#P</strong>-hard are then the monotone bipartite instances.</p>

<p><strong>Question:</strong> What are the other special cases of #2-SAT which are <strong>#P</strong>-complete, as a result of this or some other reduction?</p>

<p>It would be interesting if, in addition to showing/citing a reduction, people could also describe an intuitive reason for how the special case might provide obstacles to natural approaches to counting the satsifying assignments. For instance, although MONOTONE-2-SAT is trivially solvable ($\mathbf x = 1^n$ is always a solution), monotone instances are the ones in which assigning some variable to a fixed value will routinely fail to impose many constraints on the remaining variables. Fixing any variable $x_j = 0$ only restricts the values of the variables immediately related to it by some clause; and setting $x_j = 1$ doesn't restrict the possible values of any other variables at all. (It's not clear that the comparable restriction to bipartite graphs is significant in the same way, however; the bipartite restriction seems to add structure rather than removing it, but it fails to add structure enough to count efficiently.)</p>

<p><strong>Edited to add.</strong> Bonus points will be awarded for any such class which <em>doesn't</em> ultimately rely on the existence of monotone instances (as #2-BIPARTITE-SAT does above, whose hardness is <em>apparently</em> due to the inclusion of the <strong>#P</strong>-hard special case #2-MONOTONE-BIPARTITE-SAT). For instance, an argument for the hardness of #2-BIPARTITE-SAT which doesn't rely on monotonic instances (but might rely on some other sub-family) would be interesting. </p>

CC BY-SA 3.0
2016-02-05T21:45:00.513Z
Not exactly what you asked for at the end of your question, but there is a reduction that, given an arbitrary CNF formula $\Phi$, returns a 2-SAT formula $\Psi$ which is not monotone and which has the following property: the number of solutions of $\Psi$ having an odd number of variables set to true minus the number of solutions of $\Psi$ having an even number of variables set to true is equal to the number of solutions of $\Phi$.
Giorgio Camerani
CC BY-SA 3.0
2016-02-13T08:21:40.233Z
I forgot to say that $\Psi$ is also bipartite.
Giorgio Camerani
<cc.complexity-theory><sat><counting-complexity>
What are the #P-complete subfamilies of #2-SAT?
Niel de Beaudrap
# What are the #P-complete subfamilies of #2-SAT?

(Asked by: username_0 on 2012-11-29)

**Short version.**

The original proof that #2-SAT is **#P**-complete shows, in fact, that those instances of #2-SAT which are both *monotone* (not involving the negations of any variables) and *bipartite* (the graph formed by the clauses over the variables is a bipartite graph) are **#P**-hard. Thus, the two special cases #2-MONOTONE-SAT and #2-BIPARTITE-SAT are **#P**-hard. Are there other special cases which can be characterized in terms of 'natural' properties of the formula, which are also **#P**-hard?

**Long version.**

The problem #2-SAT is the task of computing — for a boolean formula $\phi$ consisting of the conjunction of several clauses, where each clause is a disjunction of two literals $x\_j$ or $\bar x\_j$ — the number of boolean strings $x \in \{0,1\}^n$ such that $\phi(x) = 1$. Finding out whether or not there *exists* such an $x$ is easy; but counting the number of solutions in general is **#P**-complete, as shown by Valiant in [The Complexity of Enumeration and Reliability Problems, SIAM J. Comput., **8**, pp. 410–421](http://epubs.siam.org/doi/abs/10.1137/0208032).

For the case of #2-SAT in particular, what Valiant actually shows is a reduction to #2-SAT from counting matchings (including imperfect ones) in bipartite graphs, which gives rise to instances of #2-SAT with a very particular structure, as follows.

1. First, note that the monotone problem is equivalent, by substitution, to the problem in which for each variable $x\_j$, either $x\_j$ occurs in the formula $\phi$ or $\bar x\_j$ does but not both. In particular, the "monotone decreasing" problem in which *only* the negations $\bar x\_j$ occur for every variable is exactly as hard as the monotone case.
2. For any graph $G = (V,E)$ with $m$ edges, we can construct a monotone-decreasing 2-SAT formula corresponding to matchings — collections of edges which do not share any vertices — by assigning a variable $x\_e$ to each edge, representing whether it is included in an edge-set; the property of a set $M \subseteq E$ being a matching is equivalent to the incidence vector $\mathbf x = \chi\_M$ satisfying the CNF formula $\phi$ whose clauses are given by $(\bar x\_e \vee \bar x\_f)$ for every pair of edges $e, f \in E$ which share a vertex.
   By construction, $\phi$ has as many satisfying solutions $\mathbf x \in \{0,1\}^m$ as there are (possibly imperfect) matchings in the graph $G$.
3. If the graph $G$ for which we want to count the matchings is bipartite, then it contains no odd cycles — which we can describe as a sequence of *edges* in the graph which starts and ends with the same edge (without counting that final edge twice). Then there are no sequence of variables $x\_e, x\_f, x\_g, \ldots, x\_e$ of odd length in $\phi$, in which adjacent variables are involved in a common clause. Then the formula $\phi$ would be bipartite in the manner described earlier.
4. Counting the number of matchings in arbitrary bipartite graphs, in particular, can be used to count the number of perfect matchings in a bipartite graph: given an input bitrarite graph $G = (A \cup B, E)$ with two bipartitions $A, B$ of the same size $n$, one can create graphs $G\_k$ by augmenting $A$ with anywhere $0 \leqslant k \leqslant n$ extra vertices connected to all of the vertices of $B$. Because all matchings in $G$ of a given size contribute differently to the number of matchings in $G\_k$, by counting these one can determine the number of matchings in $G$ of size $n$ (that is, which are perfect matchings); and note that counting the number of perfect matchings in bipartite graphs is equivalent to computing permanents of $\{0,1\}$-matrices by a simple correspondance.

The class of instances of #2-SAT which are shown to be **#P**-hard are then the monotone bipartite instances.

**Question:** What are the other special cases of #2-SAT which are **#P**-complete, as a result of this or some other reduction?

It would be interesting if, in addition to showing/citing a reduction, people could also describe an intuitive reason for how the special case might provide obstacles to natural approaches to counting the satsifying assignments. For instance, although MONOTONE-2-SAT is trivially solvable ($\mathbf x = 1^n$ is always a solution), monotone instances are the ones in which assigning some variable to a fixed value will routinely fail to impose many constraints on the remaining variables. Fixing any variable $x\_j = 0$ only restricts the values of the variables immediately related to it by some clause; and setting $x\_j = 1$ doesn't restrict the possible values of any other variables at all. (It's not clear that the comparable restriction to bipartite graphs is significant in the same way, however; the bipartite restriction seems to add structure rather than removing it, but it fails to add structure enough to count efficiently.)

**Edited to add.** Bonus points will be awarded for any such class which *doesn't* ultimately rely on the existence of monotone instances (as #2-BIPARTITE-SAT does above, whose hardness is *apparently* due to the inclusion of the **#P**-hard special case #2-MONOTONE-BIPARTITE-SAT). For instance, an argument for the hardness of #2-BIPARTITE-SAT which doesn't rely on monotonic instances (but might rely on some other sub-family) would be interesting.

**Tags:** cc.complexity-theory, sat, counting-complexity
> **Comments:**
> **username_1**: Not exactly what you asked for at the end of your question, but there is a reduction that, given an arbitrary CNF formula $\Phi$, returns a 2-SAT formula $\Psi$ which is not monotone and which has the following property: the number of solutions of $\Psi$ having an odd number of variables set to true minus the number of solutions of $\Psi$ having an even number of variables set to true is equal to the number of solutions of $\Phi$.  
> **username_1**: I forgot to say that $\Psi$ is also bipartite.  

---

## 2 answers

### Answer by username_1 on 2012-11-29. Score: 16

[#3-Regular Bipartite Planar Vertex Cover is #P-Complete](http://link.springer.com/chapter/10.1007/11750321_34?LI=true)

As counting vertex covers is exactly the same as counting satisfying assignments of a *monotone* #2-SAT instance, the above result implies that it is #P-complete to count satisfying assignments of a #2-SAT instance which is *monotone* and *3-regular* and *bipartite* and *planar*.

This in turn means that, in addition to the two #2-MONOTONE-SAT and #2-BIPARTITE-SAT special cases already cited in the question, the two #2-CUBIC-SAT and #2-PLANAR-SAT special cases are #P-complete as well.


---

### Answer by username_2 on 2023-04-14. Score: 8

Despite being 11 years late I hope I can still claim the bonus points! There is an (IMHO) simple and direct reduction from #SAT to #BIPARTITE-2SAT that does not rely on monotone instances. This appears in [arXiv:2304.02524](https://arxiv.org/abs/2304.02524) by myself, Konstantinos Meichanetzidis, and John van de Wetering.

Given $r \in \mathbb{N}$ and $f : \mathbb{B}^n \to \mathbb{B}$ a CNF formula with $n$ variables and $m$ clauses, there is a bipartite 2-CNF $f'$ with $O(n + mr)$ variables such that
$$|\{x \in \mathbb{B}^n \mid f(x) = 1\}| \equiv |\{x \in \mathbb{B}^n \mid f'(x) = 1\}| \pmod{2^r + 1}$$
Now suppose we have an oracle for #BIPARTITE-2SAT. Then since $|\{x \in \mathbb{B}^n \mid f(x) = 1\}| < 2^n + 1$, if we set $r = n$ then we can recover this value exactly from $|\{x \in \mathbb{B}^n \mid f'(x) = 1\}|$, which we can compute using the oracle. This gives a reduction from #SAT to #BIPARTITE-2SAT.

We can construct $f'$ from $f$ as follows:

1. For each variable $x\_i$ of $f$, add a variable $x\_i'$ to $f'$
2. For each clause $C\_j$ of $f$, add a variable $y\_j'$ to $f'$
3. For each $y\_j'$ add variables $z'\_{j1}, z'\_{j2}, \dots, z'\_{jr}$ and clauses $(y\_j' \lor \lnot z'\_{j1}) \land (y\_j' \lor \lnot z'\_{j2}) \land \cdots \land (y\_j' \lor \lnot z'\_{jr})$ to $f'$,
4. For every $i$ and $j$:
   * If $x\_i$ occurs in $C\_j$, add $\lnot x'\_i \lor \lnot y'\_j$ to $f'$
   * If $\lnot x\_i$ occurs in $C\_j$ add $x'\_i \lor \lnot y'\_j$ to $f'$

Clearly $f'$ is bipartite because it can be partitioned as $\{x'\_i\} \cup \{z'\_{jl}\}$ and $\{y'\_j\}$.

This generalizes the reduction given by Giorgio Camerani in [this answer](https://cstheory.stackexchange.com/questions/39598/%e2%8a%95p-completeness-of-%e2%8a%952sat/48282#48282) about $\oplus$2SAT (they are the same when $r = 0$).

As to why this works.. in the paper (see Lemma 3 for details), we show this using the ZH calculus, which is a formal system of diagrammatic reasoning about tensor networks. In this framework, the derivation of this construction is:
[![graphical proof for the construction of f'](https://i.sstatic.net/xObs9.png)](https://i.sstatic.net/xObs9.png)
Here, the yellow boxes with zeros are negated clauses, white dots are variables, and grey dots are negations. I'd encourage anyone interested to have a look at the ZH calculus! (of course, the OP was an author of the predecessor to this paper, so knows all about this..)

I prefer the graphical presentation, but it is also possible to given an explanation in words: the intuition for why this works is that the subformula $f''$ of $f'$ generated by only the $x'\_i$s and $y'\_j$s is essentially a weighted CNF - for every satisfying assignment of $f''$, if any $y'\_j$ is assigned true then there are $2^r$ ways to assign the $z'\_{jl}$s to make $f'$ true, and if $y'\_j$ is false then there is only one way to assign the $z'\_{jl}$s. Thus we can treat $f''$ as a weighted CNF where the $y'\_j$s are given weight $2^r$. However, $2^r \equiv -1 \mod 2^r + 1$, so we can think of these as having weight $-1$.

If $y'\_j$ is false, then no further restrictions are imposed on the $x'\_i$s. This is as if $C\_j$ did not exist. If $y'\_j$ is true then we assert that the $x'\_i$s must appear with opposite polarity than they do in $C\_j$. But this is exactly the condition for $C\_j$ to be unsatisfied! Since $y'\_j$ has weight $-1$, the total number of solutions of $f''$ is the number of solutions where $y'\_j$ is false (and $C\_j$ does not exist), minus the number of solutions $y'\_j$ is true (and $C\_j$ is unsatisfied). Therefore it is exactly the number of solutions where $C\_j$ is satisfied! This applies to every $j$, so that the total number of solutions of $f'$ (mod $2^r + 1$) is the same as $f$.

I suppose the moral of the story here is that counting is probably hard when the structure of the formulae is not sufficiently constrained to prevent you from putting weights on variables. If you can do that, then you can maybe reconstruct other structure, including arbitrarily large clauses. It seems that the bipartite structure in this case is not intrinsic to the argument but instead an artifact of the fact that the incidence graph of a #SAT instance is naturally bipartite.

For example, in the paper, we also used this weight-and-modulo trick to reduce from #SAT to #MONOTONE-2SAT (modulus $2^r$), #2SAT with degree at most three (Fibonacci number modulus), #PERFECT-MATCHINGS (modulus $2^r + 1$). And even if you can't show that counting for a particular structure of formula is #P-hard in this way, it might be sufficient to show modulo an integer to obtain at least NP-hardness. For example, if you set $r = 0$ in the reduction above, you get a reduction from $\oplus$SAT to $\oplus$2SAT, showing that #2SAT is at least NP-hard (under randomized reductions) by the Valiant-Vazirani theorem.

> **Comments:**
> **username_3**: Your item 4 in the construction of $f'$ is weird, it will always propagate the fact that $y'_j = 0$. Did you mean $\vee$ instead of $\wedge$?  
> **username_2**: @holf ah yes I did, fixed. Thanks!  
> **username_4**: how does this not solve SAT? You get O(n+mn) 2-SAT with 0 solutions iff SAT has 0 solutions  
> **username_3**: No, $f$ may be unsat and $f'$ has $k(2^r+1)$ solutions for some $k$ hence $\#f = 0 = k(2^r+1) \mathsf{~mod~} (2^r+1) = \#f'$. This is actually a very elegant reduction!  
> **username_1**: @TuomasLaakkonen If I take your $f'$ construction and ignore Step 3, what I get is exactly the same as mentioned in the first half of my answer https://cstheory.stackexchange.com/a/48282/947, which is precisely what I was referring to in my above comment to this question.  
> **username_2**: @GiorgioCamerani Ah indeed, I missed that answer before! I've added a line explaining the connection  
> **username_1**: @TuomasLaakkonen Thanks, and congratulations for your weight-and-modulo trick, I've found it truly clever. Indeed, it blows every unsatisfying assignment $u$ of $f$ into $(2^n+1)^\mu$ satisfying assignments of $f'$, where $\mu$ is the number of clauses of $f$ that are not satisfied by $u$. Such blown-up satisfying assignments of $f'$ are then sheared off by the modulo, leaving all and only the satisfying assignments of $f'$ that truly correspond to satisfying assignments of $f$.  
> **username_5**: If you eliminate the $y'_j$ variables and directly add $\pm x'_i\lor\neg z'_{jk}$, $k=1,\dots,r$ in step 4 instead of $\pm x'_i\lor\neg y'_j$ and $y'_j\lor\neg z'_{jk}$, the number of satisfying assignments of the new formula will be congruent to the original one modulo $2^r$ rather than modulo $2^r+1$. I find that more convenient.  
> **username_2**: @EmilJeřábek Indeed, that works too (e.g it's used as proof of Lemma 5 in the paper), personally I like the construction above because I think it generalizes nicely to the case where we want to compute the number of solutions mod M for arbitrary M.  

---

