<p>In <a href="https://arxiv.org/abs/2304.02524" rel="nofollow noreferrer">arXiv:2304.02524</a> Konstantinos Meichanetzidis, John van de Wetering, and I give a direct reduction from #SAT to #MONOTONE-2SAT that doesn't rely on the permanent and can be easily translated to an explicit construction. It works by first translating to #2SAT and then to #MONOTONE-2SAT. For more details on how the first part works, see <a href="https://cstheory.stackexchange.com/a/52726/37271">my other answer</a>. Essentially it encodes an arbitrary CNF into an integer-weighted 2-CNF, then makes all the weights positive by using a back transformation that is modulo a large integer. Positive weights can then be translated into extra variables and clauses. It is hilariously inefficient! For example, it translates
<span class="math-container">$$ f = (x_{1} \lor \lnot x_{2} \lor x_{3}) \land(x_{1} \lor x_{2} \lor x_{3}) $$</span>
first to this #2SAT formula
<span class="math-container">$$f' = (\lnot x_{1} \lor \lnot x_{4}) \land(x_{2} \lor \lnot x_{4}) \land(\lnot x_{3} \lor \lnot x_{4}) \land(x_{4} \lor \lnot x_{5}) \land(x_{4} \lor \lnot x_{6}) \land(x_{4} \lor \lnot x_{7}) \land(\lnot x_{1} \lor \lnot x_{8}) \land(\lnot x_{2} \lor \lnot x_{8}) \land(\lnot x_{3} \lor \lnot x_{8}) \land(x_{8} \lor \lnot x_{9}) \land(x_{8} \lor \lnot x_{10}) \land(x_{8} \lor \lnot x_{11})$$</span>
and then to following #MONOTONE-2SAT formula (with 102 variables and 187 clauses):
<span class="math-container">$$ f'' = (x_{1} \lor x_{4}) \land(x_{2} \lor x_{12}) \land(x_{2} \lor x_{13}) \land(x_{13} \lor x_{12}) \land(x_{2} \lor x_{14}) \land(x_{14} \lor x_{12}) \land(x_{2} \lor x_{15}) \land(x_{15} \lor x_{12}) \land(x_{2} \lor x_{16}) \land(x_{16} \lor x_{12}) \land(x_{2} \lor x_{17}) \land(x_{17} \lor x_{12}) \land(x_{2} \lor x_{18}) \land(x_{18} \lor x_{12}) \land(x_{2} \lor x_{19}) \land(x_{19} \lor x_{12}) \land(x_{2} \lor x_{20}) \land(x_{20} \lor x_{12}) \land(x_{2} \lor x_{21}) \land(x_{21} \lor x_{12}) \land(x_{2} \lor x_{22}) \land(x_{22} \lor x_{12}) \land(x_{2} \lor x_{23}) \land(x_{23} \lor x_{12}) \land(x_{2} \lor x_{24}) \land(x_{24} \lor x_{12}) \land(x_{12} \lor x_{4}) \land(x_{3} \lor x_{4}) \land(x_{4} \lor x_{25}) \land(x_{4} \lor x_{26}) \land(x_{26} \lor x_{25}) \land(x_{4} \lor x_{27}) \land(x_{27} \lor x_{25}) \land(x_{4} \lor x_{28}) \land(x_{28} \lor x_{25}) \land(x_{4} \lor x_{29}) \land(x_{29} \lor x_{25}) \land(x_{4} \lor x_{30}) \land(x_{30} \lor x_{25}) \land(x_{4} \lor x_{31}) \land(x_{31} \lor x_{25}) \land(x_{4} \lor x_{32}) \land(x_{32} \lor x_{25}) \land(x_{4} \lor x_{33}) \land(x_{33} \lor x_{25}) \land(x_{4} \lor x_{34}) \land(x_{34} \lor x_{25}) \land(x_{4} \lor x_{35}) \land(x_{35} \lor x_{25}) \land(x_{4} \lor x_{36}) \land(x_{36} \lor x_{25}) \land(x_{4} \lor x_{37}) \land(x_{37} \lor x_{25}) \land(x_{25} \lor x_{5}) \land(x_{4} \lor x_{38}) \land(x_{4} \lor x_{39}) \land(x_{39} \lor x_{38}) \land(x_{4} \lor x_{40}) \land(x_{40} \lor x_{38}) \land(x_{4} \lor x_{41}) \land(x_{41} \lor x_{38}) \land(x_{4} \lor x_{42}) \land(x_{42} \lor x_{38}) \land(x_{4} \lor x_{43}) \land(x_{43} \lor x_{38}) \land(x_{4} \lor x_{44}) \land(x_{44} \lor x_{38}) \land(x_{4} \lor x_{45}) \land(x_{45} \lor x_{38}) \land(x_{4} \lor x_{46}) \land(x_{46} \lor x_{38}) \land(x_{4} \lor x_{47}) \land(x_{47} \lor x_{38}) \land(x_{4} \lor x_{48}) \land(x_{48} \lor x_{38}) \land(x_{4} \lor x_{49}) \land(x_{49} \lor x_{38}) \land(x_{4} \lor x_{50}) \land(x_{50} \lor x_{38}) \land(x_{38} \lor x_{6}) \land(x_{4} \lor x_{51}) \land(x_{4} \lor x_{52}) \land(x_{52} \lor x_{51}) \land(x_{4} \lor x_{53}) \land(x_{53} \lor x_{51}) \land(x_{4} \lor x_{54}) \land(x_{54} \lor x_{51}) \land(x_{4} \lor x_{55}) \land(x_{55} \lor x_{51}) \land(x_{4} \lor x_{56}) \land(x_{56} \lor x_{51}) \land(x_{4} \lor x_{57}) \land(x_{57} \lor x_{51}) \land(x_{4} \lor x_{58}) \land(x_{58} \lor x_{51}) \land(x_{4} \lor x_{59}) \land(x_{59} \lor x_{51}) \land(x_{4} \lor x_{60}) \land(x_{60} \lor x_{51}) \land(x_{4} \lor x_{61}) \land(x_{61} \lor x_{51}) \land(x_{4} \lor x_{62}) \land(x_{62} \lor x_{51}) \land(x_{4} \lor x_{63}) \land(x_{63} \lor x_{51}) \land(x_{51} \lor x_{7}) \land(x_{1} \lor x_{8}) \land(x_{2} \lor x_{8}) \land(x_{3} \lor x_{8}) \land(x_{8} \lor x_{64}) \land(x_{8} \lor x_{65}) \land(x_{65} \lor x_{64}) \land(x_{8} \lor x_{66}) \land(x_{66} \lor x_{64}) \land(x_{8} \lor x_{67}) \land(x_{67} \lor x_{64}) \land(x_{8} \lor x_{68}) \land(x_{68} \lor x_{64}) \land(x_{8} \lor x_{69}) \land(x_{69} \lor x_{64}) \land(x_{8} \lor x_{70}) \land(x_{70} \lor x_{64}) \land(x_{8} \lor x_{71}) \land(x_{71} \lor x_{64}) \land(x_{8} \lor x_{72}) \land(x_{72} \lor x_{64}) \land(x_{8} \lor x_{73}) \land(x_{73} \lor x_{64}) \land(x_{8} \lor x_{74}) \land(x_{74} \lor x_{64}) \land(x_{8} \lor x_{75}) \land(x_{75} \lor x_{64}) \land(x_{8} \lor x_{76}) \land(x_{76} \lor x_{64}) \land(x_{64} \lor x_{9}) \land(x_{8} \lor x_{77}) \land(x_{8} \lor x_{78}) \land(x_{78} \lor x_{77}) \land(x_{8} \lor x_{79}) \land(x_{79} \lor x_{77}) \land(x_{8} \lor x_{80}) \land(x_{80} \lor x_{77}) \land(x_{8} \lor x_{81}) \land(x_{81} \lor x_{77}) \land(x_{8} \lor x_{82}) \land(x_{82} \lor x_{77}) \land(x_{8} \lor x_{83}) \land(x_{83} \lor x_{77}) \land(x_{8} \lor x_{84}) \land(x_{84} \lor x_{77}) \land(x_{8} \lor x_{85}) \land(x_{85} \lor x_{77}) \land(x_{8} \lor x_{86}) \land(x_{86} \lor x_{77}) \land(x_{8} \lor x_{87}) \land(x_{87} \lor x_{77}) \land(x_{8} \lor x_{88}) \land(x_{88} \lor x_{77}) \land(x_{8} \lor x_{89}) \land(x_{89} \lor x_{77}) \land(x_{77} \lor x_{10}) \land(x_{8} \lor x_{90}) \land(x_{8} \lor x_{91}) \land(x_{91} \lor x_{90}) \land(x_{8} \lor x_{92}) \land(x_{92} \lor x_{90}) \land(x_{8} \lor x_{93}) \land(x_{93} \lor x_{90}) \land(x_{8} \lor x_{94}) \land(x_{94} \lor x_{90}) \land(x_{8} \lor x_{95}) \land(x_{95} \lor x_{90}) \land(x_{8} \lor x_{96}) \land(x_{96} \lor x_{90}) \land(x_{8} \lor x_{97}) \land(x_{97} \lor x_{90}) \land(x_{8} \lor x_{98}) \land(x_{98} \lor x_{90}) \land(x_{8} \lor x_{99}) \land(x_{99} \lor x_{90}) \land(x_{8} \lor x_{100}) \land(x_{100} \lor x_{90}) \land(x_{8} \lor x_{101}) \land(x_{101} \lor x_{90}) \land(x_{8} \lor x_{102}) \land(x_{102} \lor x_{90}) \land(x_{90} \lor x_{11}) $$</span>
where the back transformation is given by
<span class="math-container">$$ 
|\{x \in \mathbb{B}^{11} \mid f'(x) = 1\}| = |\{x \in \mathbb{B}^{102} \mid f''(x) = 1\}| \mod 4096 \\
|\{x \in \mathbb{B}^3 \mid f(x) = 1\}| = |\{x \in \mathbb{B}^{11} \mid f'(x) = 1\}| \mod 9$$</span></p>
<p>Despite the inefficiency, this is actually a poly-time reduction, and the method of transformation is quite simple. E.g here's a implementation in &lt; 50 lines of Python:</p>
<pre><code># n = number of variables
# clauses is a list of CNF clauses, each is a list of integers, 
# where i means variable i and -i means not variable i
# the example above would be [[1, -2, 3], [1, 2, 3]]
def sat_to_2sat(n, clauses):
    fresh = n + 1
    nclauses = []
    for clause in clauses:
        if len(clause) == 2:
            nclauses.append(clause)
            continue
        v = fresh
        fresh += 1
        for lit in clause:
            nclauses.append((-lit, -v))
        for _ in range(n):
            nclauses.append((v, -fresh))
            fresh += 1
    return fresh - 1, nclauses

def sat_to_monosat(n, clauses):
    fresh = n + 1
    nclauses = []
    for clause in clauses:
        nclause = []
        for lit in clause:
            if lit &lt; 0:
                nclause.append(-lit)
            else:
                v = fresh
                fresh += 1
                nclauses.append((lit, v))
                nclause.append(v)
                for _ in range(n + 1):
                    nclauses.append((lit, fresh))
                    nclauses.append((fresh, v))
                    fresh += 1
        nclauses.append(nclause)
    return fresh - 1, nclauses

def sat_to_mono2sat(n, clauses):
    n1, clauses1 = sat_to_2sat(n, clauses)
    n2, clauses2 = sat_to_monosat(n1, clauses1)
    print(n, n1)
    return n2, clauses2

def postprocessing(n, clauses, count):
    n1, _ = sat_to_2sat(n, clauses)
    return (count % (2 ** (n1 + 1))) % (2 ** n + 1)
</code></pre>

CC BY-SA 4.0
2023-05-03T21:21:06.647Z
Thanks a lot for this very interesting answer and reference. 13 years later, my curiosity on this is still far from being extinguished...
Giorgio Camerani
CC BY-SA 4.0
2023-04-14T11:41:35.280Z
2023-04-14T11:41:35.280Z
Tuomas Laakkonen
<p>#3SAT can be reduced to #3DNF where we are talking about disjunctive normal form.  Simple take formula phi and logically negate it not(phi).  Then it's effectively trivially in DNF form.  #3SAT(phi)=2^n-#3DNF(not(phi)) where n is the number of literals.  This does not give a parsimonious reduction but takes advantage of a co-NP counterpart.  Since there are maximum 2^n solutions, we subtract the count of unsatisfiable solutions.  3DNF is in P, trivially as any term without contradicting literals is a solution, making the decision problem linear time solvable.  Converting to #2SAT will go through this route almost for sure.  #3DNF-&gt;#2SAT might involve making the formula monotonic so only clauses with all positive and all negative terms are allowed.  Then the literals are the same in 2SAT and your clause gadget is just two implication loops and a truth e.g. (x1 and x2 and x3) become (clause1 or not x1) and (x1 or not x2) and (x2 or not x3) or (x3 or not clause1) or clause1.  This means clause1,x1,x2,x3 are all true or all false and clause1 determines acceptance.  However, the monotone transform which by DeMorgans law will be inverse of how its done for CNF, introduces variables and thus extra solutions and I believe is not parsimonious.  E.g. (x or not y)=(x or u)and(not u or not y).  Now xu(not y) and x(not u)(not y) are solutions.  It might be solvable by dividing by 2 to the number of introduces variables in some way.  Regardless this is a brief sketch on thoughts for how we could create a formal proof on such topic and probably the only reasonable route to do so.</p>
<p>#3SAT can be reduced to permanent using better techniques than Valiants original method.  It normally goes:
#3SAT-&gt;#3SAT balanced-&gt;(-1,0,1) permanent-&gt;{0,...,m} permanent-&gt;(0,1) permanent.  The complicated part using some special gadgets is converting to -1,0,1 permanent.  Unfortunately this parsimonious method greatly increases the size of the instance practically speaking even if it's polynomial in terms of phi.  But when 0-1 permanent computations are O(n!×2^n), n is not going to get more than 60 or so even with the most powerful computers out there.  I even found some nice videos on YouTube detailing the full proof with these transforms if you search for 0-1 permanent, so you can even relax for an hour or two and see all the nuts and bolts.</p>

CC BY-SA 4.0
2021-12-12T02:32:11.570Z
2021-12-12T02:32:11.570Z
Gregory Morse
<p>As for the first question, that is what a reduction does.  For how to reduce #3SAT to #Monotone-2SAT, see the proof of #P-completeness of #Monotone-2SAT [Val79b], which is based on the #P-completeness of Permanent [Val79a].  To reduce #SAT to #3SAT, Cook’s reduction from any problem in NP to 3SAT is parsimonious and therefore reduces #SAT to #3SAT.</p>

<p>The answer to the second question is no.  The reduction in [Val79a] from #3SAT to Permanent does not preserve the number of solutions.  Moreover, if a reduction from #SAT to #Monotone-2SAT (or Permanent) which preserves the number of solutions were known, the same reduction would reduce the decision version of SAT to the decision version of Monotone-2SAT (or Bipartite Matching), implying P=NP.</p>

<p>References</p>

<p>[Val79a] Leslie G. Valiant.  The complexity of computing the permanent.  <em>Theoretical Computer Science</em>, 8(2):189–201, 1979.  <a href="http://dx.doi.org/10.1016/0304-3975(79)90044-6" rel="noreferrer">http://dx.doi.org/10.1016/0304-3975(79)90044-6</a></p>

<p>[Val79b] Leslie G. Valiant.  The complexity of enumeration and reliability problems.  <em>SIAM Journal on Computing</em>, 8(3):410–421, Aug. 1979.  <a href="http://dx.doi.org/10.1137/0208032" rel="noreferrer">http://dx.doi.org/10.1137/0208032</a></p>

CC BY-SA 4.0
2021-12-12T02:37:35.220Z
Even if you cannot preserve solutions from #3SAT to permanent, you can have the additional amount exactly known e.g. -2^(3m/2)×C for -1,0,1 peemanent as is usually used in proofs of thus transform where m is the number of true and false literals of a 3SAT equation which has been balanced.  Dividing the permanent result by power of 2 is not difficult.  Perhaps there is a yet discovered method to directly do it.  Similar ideas make converting counting unsatisfiable solutions of #3SAT feasible in #2SAT and subtracting it from 2^n as detailed I  my answer
Gregory Morse
CC BY-SA 2.5
2010-09-13T12:09:52.340Z
Thanks for your pointers to [Val79b] and [Val79a]. For what concerns the second answer, I can't understand it: if a problem is #P-complete it can be used to solve any other problem in #P. Now suppose I want to solve #SAT: I want to know the number K of solutions of a given formula F; in order to do so, I reduce F to an instance F' of #MONOTONE-2SAT, then I obtain the number K' of solutions to F'. Now, if knowing K' doesn't help me in knowing K (i.e. solving #MONOTONE-2SAT doesn't help me to solve #SAT) how can #MONOTONE-2SAT be #P-complete? Why shall I do all this if it doesn't solve #SAT?
Giorgio Camerani
CC BY-SA 2.5
2010-09-13T12:15:32.830Z
Let me express a side comment. Is it possible that I have to pay 40 dollars to read an article which is 31 years old? I find this absurd and against the spirit of science. I would agree if the article was 10-15 years old, as it can be considered as a "patented" discovery. But paying for a 31 years old article is a shame IMHO. Could anyone point me to a free version of it?
Giorgio Camerani
CC BY-SA 2.5
2010-09-13T12:46:42.860Z
As for the second answer, it is possible to compute K from K′ (and F); otherwise a mapping from F to F′ would not be a reduction.  However, your question is about whether it is possible to make a reduction such that K=K′.  The answer is that it is not possible.
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-13T12:47:43.473Z
@Tsuyoshi Ito: A further comment on your second answer. Having the same number of solutions doesn't imply having the same solution space. An instance A may have the same number of solutions of an instance B, but B's solutions may be distributed in a completely different manner in the solution space.
Giorgio Camerani
CC BY-SA 2.5
2010-09-13T12:52:41.107Z
@Tsuyoshi Ito: OK, I'm glad we now agree. Actually my second question was: "does K = K' or do I have to convert back K' to K through some function?".
Giorgio Camerani
CC BY-SA 2.5
2010-09-13T12:56:48.727Z
Not sure if you already understand this or not, but the answer is that you have to use a non-identity function to convert K′ to K.  I am not talking anything about the “solution space,” I am only talking about the number of solutions.
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-13T14:10:22.853Z
Of course I understood that your answer means I have to use a non-identity function. Not sure if you understood that it's OK for me, and that I'm not looking for a reduction such that K' = K. I only wanted to know which was the case: identity function or non-identity function? Now that I know that the answer is "non-identity function", it's perfectly OK for me and I'm perfectly satisfied. My comment on solution space was because I didn't immediately follow your sentence "if a reduction from #SAT to #Monotone-2SAT (or Permanent) which preserves...
Giorgio Camerani
CC BY-SA 2.5
2010-09-13T14:10:55.680Z
...the number of solutions were known, the same reduction would reduce SAT to Monotone-2SAT (or Bipartite Matching), implying P=NP". Suppose that such a reduction exists: what is not clear to me is how could it help us to find a satisfying assignment (of course it would allow us to decide if the formula is satisfiable or unsatisfiable).
Giorgio Camerani
CC BY-SA 2.5
2010-09-13T14:19:09.877Z
I just mean I do not immediately see that in such a case a satisfying assignment of F' could be converted back to a corresponding satisfying assignment of F. It doesn't seem trivial that the reduction can be used also as a bijection from solutions of F' to solutions of F.
Giorgio Camerani
CC BY-SA 2.5
2010-09-13T15:11:36.057Z
Now I see the source of confusion!  By “SAT,” “Monotone-2SAT” and “Perfect Matching,” I meant the decision versions of them (decide whether a solution exists or not), not the function versions (find a solution).  I edited the answer to clarify it.  I hope that this will clear things up.
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-13T15:25:48.103Z
Oh, yes that was the reason of confusion ;-) Now everything is clear, thanks for your help.
Giorgio Camerani
CC BY-SA 2.5
2010-09-13T15:46:00.157Z
I do not know freely available copies of the papers I cited.  A proof of the #P-completeness of Permanent is in many textbooks on computational complexity, which may be available at libraries: e.g. _Computational Complexity_ by Papadimitriou, _Computational Complexity: A Conceptual Perspective_ by Goldreich and _Computational Complexity: A Modern Approach_ by Arora and Barak contain a proof.  (more)
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-13T15:46:25.960Z
(Cont’d)  I do not know an easily available resource which contains a proof of #Monotone-2SAT if you do not have access to the journals I cited.  Although _Theory of Computational Complexity_ by Du and Ko states it as Exercise 9.3, it does not contain a hint or a solution as far as I can tell.
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-13T16:20:14.020Z
As an exercise! This is fun. A seminal paper left as an exercise for the reader. Anyhow, I've found more than a sketch of the proof here: http://en.wikipedia.org/wiki/Permanent_is_sharp-P-complete.
Giorgio Camerani
CC BY-SA 2.5
2010-09-13T16:47:55.363Z
Sorry if it confused you, but Du and Ko also give a proof of the #P-completeness of Permanent.  They leave a proof of the #P-completeness of #Monotone-2SAT as an exercise.  Also, I guess there are lecture notes available online which contain a proof of the #P-completeness of Permanent.
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-13T10:55:16.147Z
2010-09-13T15:02:01.023Z
2010-09-13T15:02:01.023Z
Tsuyoshi Ito
<p>The problem #MONOTONE-2SAT is known to be #P-complete. This means that #SAT can be reduced to it. My question is: given a #SAT instance $F$, which is the transformation that converts $F$ to its corresponding #MONOTONE-2SAT instance $F'$?</p>

<p>A second question is: let $K'$ be the number of solutions of $F'$, and let $K$ be the number of solutions of $F$. Does $K' = K$? Or we must use a back transformation that converts $K'$ to $K$?</p>

CC BY-SA 2.5
2010-09-13T09:04:37.770Z
Could you please motivate why did you vote against this question?
Giorgio Camerani
CC BY-SA 2.5
2010-09-13T11:40:22.410Z
I am not the one who voted the question down, but I will not be surprised if someone considers that the question is too basic.
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-13T11:58:58.073Z
I dont' think so. It's not more basic than some other questions raised on this website. Anyhow a question, even if basic, may nonetheless be helpful. My questions about lower bounds on #SAT and on SAT solution clusters may be considered very basic as well, but they were not voted down.
Giorgio Camerani
CC BY-SA 2.5
2010-09-13T12:16:02.610Z
The first question is pretty basic: essentially you asked what a reduction was.  The second question has trapped me once, too, but it is resolved by thinking in the right way.  The whole point of my answer is that the question is _easy_.  If you still think that the question is at the right level after reading my answer, probably my answer is written poorly.
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-13T12:33:39.043Z
I could reword my first question to "Which is the paper showing the #P-completeness of #MONOTONE-2SAT?". So I agree it's very basic, but not unuseful in general (of course it's unuseful for those knowing such paper). Your answer is not written poorly, it's very clear. I think that only crank questions and out-of-TCS questions should be banned, while easy questions should be welcome as well, because they can be helpful for someone. Please read my comment on your second answer (I can't understand it).
Giorgio Camerani
CC BY-SA 2.5
2010-09-13T13:18:26.117Z
Voting a question down is different from banning (or closing) the question.
Tsuyoshi Ito
CC BY-SA 2.5
2010-09-13T16:06:29.740Z
Walter, Tsuyoshi, while this discussion is helpful, a better place for it is on meta.cstheory.stackexchange.com. Why don't you discuss this there, and add a link to that discussion here. FWIW, I think the question is relatively harmless, but a bit more of "why I'm asking" would have been helpful.
Suresh Venkat
<cc.complexity-theory><ds.algorithms><complexity-classes><sat>
Reducing #SAT to #MONOTONE-2SAT
Giorgio Camerani
# Reducing #SAT to #MONOTONE-2SAT

(Asked by: username_0 on 2010-09-13)

The problem #MONOTONE-2SAT is known to be #P-complete. This means that #SAT can be reduced to it. My question is: given a #SAT instance $F$, which is the transformation that converts $F$ to its corresponding #MONOTONE-2SAT instance $F'$?

A second question is: let $K'$ be the number of solutions of $F'$, and let $K$ be the number of solutions of $F$. Does $K' = K$? Or we must use a back transformation that converts $K'$ to $K$?

**Tags:** cc.complexity-theory, ds.algorithms, complexity-classes, sat
> **Comments:**
> **username_0**: Could you please motivate why did you vote against this question?  
> **username_1**: I am not the one who voted the question down, but I will not be surprised if someone considers that the question is too basic.  
> **username_0**: I dont' think so. It's not more basic than some other questions raised on this website. Anyhow a question, even if basic, may nonetheless be helpful. My questions about lower bounds on #SAT and on SAT solution clusters may be considered very basic as well, but they were not voted down.  
> **username_1**: The first question is pretty basic: essentially you asked what a reduction was.  The second question has trapped me once, too, but it is resolved by thinking in the right way.  The whole point of my answer is that the question is _easy_.  If you still think that the question is at the right level after reading my answer, probably my answer is written poorly.  
> **username_0**: I could reword my first question to "Which is the paper showing the #P-completeness of #MONOTONE-2SAT?". So I agree it's very basic, but not unuseful in general (of course it's unuseful for those knowing such paper). Your answer is not written poorly, it's very clear. I think that only crank questions and out-of-TCS questions should be banned, while easy questions should be welcome as well, because they can be helpful for someone. Please read my comment on your second answer (I can't understand it).  
> **username_1**: Voting a question down is different from banning (or closing) the question.  
> **username_2**: Walter, Tsuyoshi, while this discussion is helpful, a better place for it is on meta.cstheory.stackexchange.com. Why don't you discuss this there, and add a link to that discussion here. FWIW, I think the question is relatively harmless, but a bit more of "why I'm asking" would have been helpful.  

---

## 3 answers

### Answer by username_1 on 2010-09-13. Score: 9 | Accepted answer

As for the first question, that is what a reduction does. For how to reduce #3SAT to #Monotone-2SAT, see the proof of #P-completeness of #Monotone-2SAT [Val79b], which is based on the #P-completeness of Permanent [Val79a]. To reduce #SAT to #3SAT, Cook’s reduction from any problem in NP to 3SAT is parsimonious and therefore reduces #SAT to #3SAT.

The answer to the second question is no. The reduction in [Val79a] from #3SAT to Permanent does not preserve the number of solutions. Moreover, if a reduction from #SAT to #Monotone-2SAT (or Permanent) which preserves the number of solutions were known, the same reduction would reduce the decision version of SAT to the decision version of Monotone-2SAT (or Bipartite Matching), implying P=NP.

References

[Val79a] Leslie G. Valiant. The complexity of computing the permanent. *Theoretical Computer Science*, 8(2):189–201, 1979. <http://dx.doi.org/10.1016/0304-3975(79)90044-6>

[Val79b] Leslie G. Valiant. The complexity of enumeration and reliability problems. *SIAM Journal on Computing*, 8(3):410–421, Aug. 1979. <http://dx.doi.org/10.1137/0208032>

> **Comments:**
> **username_0**: Thanks for your pointers to [Val79b] and [Val79a]. For what concerns the second answer, I can't understand it: if a problem is #P-complete it can be used to solve any other problem in #P. Now suppose I want to solve #SAT: I want to know the number K of solutions of a given formula F; in order to do so, I reduce F to an instance F' of #MONOTONE-2SAT, then I obtain the number K' of solutions to F'. Now, if knowing K' doesn't help me in knowing K (i.e. solving #MONOTONE-2SAT doesn't help me to solve #SAT) how can #MONOTONE-2SAT be #P-complete? Why shall I do all this if it doesn't solve #SAT?  
> **username_0**: Let me express a side comment. Is it possible that I have to pay 40 dollars to read an article which is 31 years old? I find this absurd and against the spirit of science. I would agree if the article was 10-15 years old, as it can be considered as a "patented" discovery. But paying for a 31 years old article is a shame IMHO. Could anyone point me to a free version of it?  
> **username_1**: As for the second answer, it is possible to compute K from K′ (and F); otherwise a mapping from F to F′ would not be a reduction.  However, your question is about whether it is possible to make a reduction such that K=K′.  The answer is that it is not possible.  
> **username_0**: @Tsuyoshi Ito: A further comment on your second answer. Having the same number of solutions doesn't imply having the same solution space. An instance A may have the same number of solutions of an instance B, but B's solutions may be distributed in a completely different manner in the solution space.  
> **username_0**: @Tsuyoshi Ito: OK, I'm glad we now agree. Actually my second question was: "does K = K' or do I have to convert back K' to K through some function?".  
> **username_1**: Not sure if you already understand this or not, but the answer is that you have to use a non-identity function to convert K′ to K.  I am not talking anything about the “solution space,” I am only talking about the number of solutions.  
> **username_0**: Of course I understood that your answer means I have to use a non-identity function. Not sure if you understood that it's OK for me, and that I'm not looking for a reduction such that K' = K. I only wanted to know which was the case: identity function or non-identity function? Now that I know that the answer is "non-identity function", it's perfectly OK for me and I'm perfectly satisfied. My comment on solution space was because I didn't immediately follow your sentence "if a reduction from #SAT to #Monotone-2SAT (or Permanent) which preserves...  
> **username_0**: ...the number of solutions were known, the same reduction would reduce SAT to Monotone-2SAT (or Bipartite Matching), implying P=NP". Suppose that such a reduction exists: what is not clear to me is how could it help us to find a satisfying assignment (of course it would allow us to decide if the formula is satisfiable or unsatisfiable).  
> **username_0**: I just mean I do not immediately see that in such a case a satisfying assignment of F' could be converted back to a corresponding satisfying assignment of F. It doesn't seem trivial that the reduction can be used also as a bijection from solutions of F' to solutions of F.  
> **username_1**: Now I see the source of confusion!  By “SAT,” “Monotone-2SAT” and “Perfect Matching,” I meant the decision versions of them (decide whether a solution exists or not), not the function versions (find a solution).  I edited the answer to clarify it.  I hope that this will clear things up.  
> **username_0**: Oh, yes that was the reason of confusion ;-) Now everything is clear, thanks for your help.  
> **username_1**: I do not know freely available copies of the papers I cited.  A proof of the #P-completeness of Permanent is in many textbooks on computational complexity, which may be available at libraries: e.g. _Computational Complexity_ by Papadimitriou, _Computational Complexity: A Conceptual Perspective_ by Goldreich and _Computational Complexity: A Modern Approach_ by Arora and Barak contain a proof.  (more)  
> **username_1**: (Cont’d)  I do not know an easily available resource which contains a proof of #Monotone-2SAT if you do not have access to the journals I cited.  Although _Theory of Computational Complexity_ by Du and Ko states it as Exercise 9.3, it does not contain a hint or a solution as far as I can tell.  
> **username_0**: As an exercise! This is fun. A seminal paper left as an exercise for the reader. Anyhow, I've found more than a sketch of the proof here: http://en.wikipedia.org/wiki/Permanent_is_sharp-P-complete.  
> **username_1**: Sorry if it confused you, but Du and Ko also give a proof of the #P-completeness of Permanent.  They leave a proof of the #P-completeness of #Monotone-2SAT as an exercise.  Also, I guess there are lecture notes available online which contain a proof of the #P-completeness of Permanent.  
> **username_4**: Even if you cannot preserve solutions from #3SAT to permanent, you can have the additional amount exactly known e.g. -2^(3m/2)×C for -1,0,1 peemanent as is usually used in proofs of thus transform where m is the number of true and false literals of a 3SAT equation which has been balanced.  Dividing the permanent result by power of 2 is not difficult.  Perhaps there is a yet discovered method to directly do it.  Similar ideas make converting counting unsatisfiable solutions of #3SAT feasible in #2SAT and subtracting it from 2^n as detailed I  my answer  

---

### Answer by username_3 on 2023-04-14. Score: 4

In arXiv:2304.02524 Konstantinos Meichanetzidis, John van de Wetering, and I give a direct reduction from #SAT to #MONOTONE-2SAT that doesn't rely on the permanent and can be easily translated to an explicit construction. It works by first translating to #2SAT and then to #MONOTONE-2SAT. For more details on how the first part works, see my other answer. Essentially it encodes an arbitrary CNF into an integer-weighted 2-CNF, then makes all the weights positive by using a back transformation that is modulo a large integer. Positive weights can then be translated into extra variables and clauses. It is hilariously inefficient! For example, it translates
$$ f = (x_{1} \lor \lnot x_{2} \lor x_{3}) \land(x_{1} \lor x_{2} \lor x_{3}) $$
first to this #2SAT formula
$$f' = (\lnot x_{1} \lor \lnot x_{4}) \land(x_{2} \lor \lnot x_{4}) \land(\lnot x_{3} \lor \lnot x_{4}) \land(x_{4} \lor \lnot x_{5}) \land(x_{4} \lor \lnot x_{6}) \land(x_{4} \lor \lnot x_{7}) \land(\lnot x_{1} \lor \lnot x_{8}) \land(\lnot x_{2} \lor \lnot x_{8}) \land(\lnot x_{3} \lor \lnot x_{8}) \land(x_{8} \lor \lnot x_{9}) \land(x_{8} \lor \lnot x_{10}) \land(x_{8} \lor \lnot x_{11})$$
and then to following #MONOTONE-2SAT formula (with 102 variables and 187 clauses):
$$ f'' = (x_{1} \lor x_{4}) \land(x_{2} \lor x_{12}) \land(x_{2} \lor x_{13}) \land(x_{13} \lor x_{12}) \land(x_{2} \lor x_{14}) \land(x_{14} \lor x_{12}) \land(x_{2} \lor x_{15}) \land(x_{15} \lor x_{12}) \land(x_{2} \lor x_{16}) \land(x_{16} \lor x_{12}) \land(x_{2} \lor x_{17}) \land(x_{17} \lor x_{12}) \land(x_{2} \lor x_{18}) \land(x_{18} \lor x_{12}) \land(x_{2} \lor x_{19}) \land(x_{19} \lor x_{12}) \land(x_{2} \lor x_{20}) \land(x_{20} \lor x_{12}) \land(x_{2} \lor x_{21}) \land(x_{21} \lor x_{12}) \land(x_{2} \lor x_{22}) \land(x_{22} \lor x_{12}) \land(x_{2} \lor x_{23}) \land(x_{23} \lor x_{12}) \land(x_{2} \lor x_{24}) \land(x_{24} \lor x_{12}) \land(x_{12} \lor x_{4}) \land(x_{3} \lor x_{4}) \land(x_{4} \lor x_{25}) \land(x_{4} \lor x_{26}) \land(x_{26} \lor x_{25}) \land(x_{4} \lor x_{27}) \land(x_{27} \lor x_{25}) \land(x_{4} \lor x_{28}) \land(x_{28} \lor x_{25}) \land(x_{4} \lor x_{29}) \land(x_{29} \lor x_{25}) \land(x_{4} \lor x_{30}) \land(x_{30} \lor x_{25}) \land(x_{4} \lor x_{31}) \land(x_{31} \lor x_{25}) \land(x_{4} \lor x_{32}) \land(x_{32} \lor x_{25}) \land(x_{4} \lor x_{33}) \land(x_{33} \lor x_{25}) \land(x_{4} \lor x_{34}) \land(x_{34} \lor x_{25}) \land(x_{4} \lor x_{35}) \land(x_{35} \lor x_{25}) \land(x_{4} \lor x_{36}) \land(x_{36} \lor x_{25}) \land(x_{4} \lor x_{37}) \land(x_{37} \lor x_{25}) \land(x_{25} \lor x_{5}) \land(x_{4} \lor x_{38}) \land(x_{4} \lor x_{39}) \land(x_{39} \lor x_{38}) \land(x_{4} \lor x_{40}) \land(x_{40} \lor x_{38}) \land(x_{4} \lor x_{41}) \land(x_{41} \lor x_{38}) \land(x_{4} \lor x_{42}) \land(x_{42} \lor x_{38}) \land(x_{4} \lor x_{43}) \land(x_{43} \lor x_{38}) \land(x_{4} \lor x_{44}) \land(x_{44} \lor x_{38}) \land(x_{4} \lor x_{45}) \land(x_{45} \lor x_{38}) \land(x_{4} \lor x_{46}) \land(x_{46} \lor x_{38}) \land(x_{4} \lor x_{47}) \land(x_{47} \lor x_{38}) \land(x_{4} \lor x_{48}) \land(x_{48} \lor x_{38}) \land(x_{4} \lor x_{49}) \land(x_{49} \lor x_{38}) \land(x_{4} \lor x_{50}) \land(x_{50} \lor x_{38}) \land(x_{38} \lor x_{6}) \land(x_{4} \lor x_{51}) \land(x_{4} \lor x_{52}) \land(x_{52} \lor x_{51}) \land(x_{4} \lor x_{53}) \land(x_{53} \lor x_{51}) \land(x_{4} \lor x_{54}) \land(x_{54} \lor x_{51}) \land(x_{4} \lor x_{55}) \land(x_{55} \lor x_{51}) \land(x_{4} \lor x_{56}) \land(x_{56} \lor x_{51}) \land(x_{4} \lor x_{57}) \land(x_{57} \lor x_{51}) \land(x_{4} \lor x_{58}) \land(x_{58} \lor x_{51}) \land(x_{4} \lor x_{59}) \land(x_{59} \lor x_{51}) \land(x_{4} \lor x_{60}) \land(x_{60} \lor x_{51}) \land(x_{4} \lor x_{61}) \land(x_{61} \lor x_{51}) \land(x_{4} \lor x_{62}) \land(x_{62} \lor x_{51}) \land(x_{4} \lor x_{63}) \land(x_{63} \lor x_{51}) \land(x_{51} \lor x_{7}) \land(x_{1} \lor x_{8}) \land(x_{2} \lor x_{8}) \land(x_{3} \lor x_{8}) \land(x_{8} \lor x_{64}) \land(x_{8} \lor x_{65}) \land(x_{65} \lor x_{64}) \land(x_{8} \lor x_{66}) \land(x_{66} \lor x_{64}) \land(x_{8} \lor x_{67}) \land(x_{67} \lor x_{64}) \land(x_{8} \lor x_{68}) \land(x_{68} \lor x_{64}) \land(x_{8} \lor x_{69}) \land(x_{69} \lor x_{64}) \land(x_{8} \lor x_{70}) \land(x_{70} \lor x_{64}) \land(x_{8} \lor x_{71}) \land(x_{71} \lor x_{64}) \land(x_{8} \lor x_{72}) \land(x_{72} \lor x_{64}) \land(x_{8} \lor x_{73}) \land(x_{73} \lor x_{64}) \land(x_{8} \lor x_{74}) \land(x_{74} \lor x_{64}) \land(x_{8} \lor x_{75}) \land(x_{75} \lor x_{64}) \land(x_{8} \lor x_{76}) \land(x_{76} \lor x_{64}) \land(x_{64} \lor x_{9}) \land(x_{8} \lor x_{77}) \land(x_{8} \lor x_{78}) \land(x_{78} \lor x_{77}) \land(x_{8} \lor x_{79}) \land(x_{79} \lor x_{77}) \land(x_{8} \lor x_{80}) \land(x_{80} \lor x_{77}) \land(x_{8} \lor x_{81}) \land(x_{81} \lor x_{77}) \land(x_{8} \lor x_{82}) \land(x_{82} \lor x_{77}) \land(x_{8} \lor x_{83}) \land(x_{83} \lor x_{77}) \land(x_{8} \lor x_{84}) \land(x_{84} \lor x_{77}) \land(x_{8} \lor x_{85}) \land(x_{85} \lor x_{77}) \land(x_{8} \lor x_{86}) \land(x_{86} \lor x_{77}) \land(x_{8} \lor x_{87}) \land(x_{87} \lor x_{77}) \land(x_{8} \lor x_{88}) \land(x_{88} \lor x_{77}) \land(x_{8} \lor x_{89}) \land(x_{89} \lor x_{77}) \land(x_{77} \lor x_{10}) \land(x_{8} \lor x_{90}) \land(x_{8} \lor x_{91}) \land(x_{91} \lor x_{90}) \land(x_{8} \lor x_{92}) \land(x_{92} \lor x_{90}) \land(x_{8} \lor x_{93}) \land(x_{93} \lor x_{90}) \land(x_{8} \lor x_{94}) \land(x_{94} \lor x_{90}) \land(x_{8} \lor x_{95}) \land(x_{95} \lor x_{90}) \land(x_{8} \lor x_{96}) \land(x_{96} \lor x_{90}) \land(x_{8} \lor x_{97}) \land(x_{97} \lor x_{90}) \land(x_{8} \lor x_{98}) \land(x_{98} \lor x_{90}) \land(x_{8} \lor x_{99}) \land(x_{99} \lor x_{90}) \land(x_{8} \lor x_{100}) \land(x_{100} \lor x_{90}) \land(x_{8} \lor x_{101}) \land(x_{101} \lor x_{90}) \land(x_{8} \lor x_{102}) \land(x_{102} \lor x_{90}) \land(x_{90} \lor x_{11}) $$
where the back transformation is given by
$$ 
|\{x \in \mathbb{B}^{11} \mid f'(x) = 1\}| = |\{x \in \mathbb{B}^{102} \mid f''(x) = 1\}| \mod 4096 \\
|\{x \in \mathbb{B}^3 \mid f(x) = 1\}| = |\{x \in \mathbb{B}^{11} \mid f'(x) = 1\}| \mod 9$$
Despite the inefficiency, this is actually a poly-time reduction, and the method of transformation is quite simple. E.g here's a implementation in < 50 lines of Python:
# n = number of variables
# clauses is a list of CNF clauses, each is a list of integers, 
# where i means variable i and -i means not variable i
# the example above would be [[1, -2, 3], [1, 2, 3]]
def sat_to_2sat(n, clauses):
    fresh = n + 1
    nclauses = []
    for clause in clauses:
        if len(clause) == 2:
            nclauses.append(clause)
            continue
        v = fresh
        fresh += 1
        for lit in clause:
            nclauses.append((-lit, -v))
        for _ in range(n):
            nclauses.append((v, -fresh))
            fresh += 1
    return fresh - 1, nclauses

def sat_to_monosat(n, clauses):
    fresh = n + 1
    nclauses = []
    for clause in clauses:
        nclause = []
        for lit in clause:
            if lit < 0:
                nclause.append(-lit)
            else:
                v = fresh
                fresh += 1
                nclauses.append((lit, v))
                nclause.append(v)
                for _ in range(n + 1):
                    nclauses.append((lit, fresh))
                    nclauses.append((fresh, v))
                    fresh += 1
        nclauses.append(nclause)
    return fresh - 1, nclauses

def sat_to_mono2sat(n, clauses):
    n1, clauses1 = sat_to_2sat(n, clauses)
    n2, clauses2 = sat_to_monosat(n1, clauses1)
    print(n, n1)
    return n2, clauses2

def postprocessing(n, clauses, count):
    n1, _ = sat_to_2sat(n, clauses)
    return (count % (2 ** (n1 + 1))) % (2 ** n + 1)

> **Comments:**
> **username_0**: Thanks a lot for this very interesting answer and reference. 13 years later, my curiosity on this is still far from being extinguished...  

---

### Answer by username_4 on 2021-12-12. Score: 0

#3SAT can be reduced to #3DNF where we are talking about disjunctive normal form. Simple take formula phi and logically negate it not(phi). Then it's effectively trivially in DNF form. #3SAT(phi)=2^n-#3DNF(not(phi)) where n is the number of literals. This does not give a parsimonious reduction but takes advantage of a co-NP counterpart. Since there are maximum 2^n solutions, we subtract the count of unsatisfiable solutions. 3DNF is in P, trivially as any term without contradicting literals is a solution, making the decision problem linear time solvable. Converting to #2SAT will go through this route almost for sure. #3DNF->#2SAT might involve making the formula monotonic so only clauses with all positive and all negative terms are allowed. Then the literals are the same in 2SAT and your clause gadget is just two implication loops and a truth e.g. (x1 and x2 and x3) become (clause1 or not x1) and (x1 or not x2) and (x2 or not x3) or (x3 or not clause1) or clause1. This means clause1,x1,x2,x3 are all true or all false and clause1 determines acceptance. However, the monotone transform which by DeMorgans law will be inverse of how its done for CNF, introduces variables and thus extra solutions and I believe is not parsimonious. E.g. (x or not y)=(x or u)and(not u or not y). Now xu(not y) and x(not u)(not y) are solutions. It might be solvable by dividing by 2 to the number of introduces variables in some way. Regardless this is a brief sketch on thoughts for how we could create a formal proof on such topic and probably the only reasonable route to do so.

#3SAT can be reduced to permanent using better techniques than Valiants original method. It normally goes:
#3SAT->#3SAT balanced->(-1,0,1) permanent->{0,...,m} permanent->(0,1) permanent. The complicated part using some special gadgets is converting to -1,0,1 permanent. Unfortunately this parsimonious method greatly increases the size of the instance practically speaking even if it's polynomial in terms of phi. But when 0-1 permanent computations are O(n!×2^n), n is not going to get more than 60 or so even with the most powerful computers out there. I even found some nice videos on YouTube detailing the full proof with these transforms if you search for 0-1 permanent, so you can even relax for an hour or two and see all the nuts and bolts.


---

