# Reducing #SAT to #MONOTONE-2SAT

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$?

• Could you please motivate why did you vote against this question? Sep 13, 2010 at 9:04
• 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. Sep 13, 2010 at 11:40
• 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. Sep 13, 2010 at 11:58
• 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. Sep 13, 2010 at 12:16
• 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. Sep 13, 2010 at 16:06

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

• 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? Sep 13, 2010 at 12:09
• 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? Sep 13, 2010 at 12:15
• 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. Sep 13, 2010 at 12:46
• @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. Sep 13, 2010 at 12:47
• 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) Sep 13, 2010 at 15:46

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)

• Thanks a lot for this very interesting answer and reference. 13 years later, my curiosity on this is still far from being extinguished... May 3, 2023 at 21:21

#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.