10

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

Giorgio Camerani
  • 6,842
  • 1
  • 34
  • 64
  • Could you please motivate why did you vote against this question? – Giorgio Camerani Sep 13 '10 at 09: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. – Tsuyoshi Ito Sep 13 '10 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. – Giorgio Camerani Sep 13 '10 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. – Tsuyoshi Ito Sep 13 '10 at 12:16
  • 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 Sep 13 '10 at 12:33
  • Voting a question down is different from banning (or closing) the question. – Tsuyoshi Ito Sep 13 '10 at 13:18
  • 1
    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 Sep 13 '10 at 16:06

3 Answers3

8

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

Tsuyoshi Ito
  • 16,466
  • 2
  • 55
  • 106
  • 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 Sep 13 '10 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? – Giorgio Camerani Sep 13 '10 at 12:15
  • 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. – Tsuyoshi Ito Sep 13 '10 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. – Giorgio Camerani Sep 13 '10 at 12:47
  • @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 Sep 13 '10 at 12:52
  • 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 Sep 13 '10 at 12:56
  • 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 Sep 13 '10 at 14:10
  • ...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 Sep 13 '10 at 14:10
  • 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 Sep 13 '10 at 14:19
  • 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 Sep 13 '10 at 15:11
  • Oh, yes that was the reason of confusion ;-) Now everything is clear, thanks for your help. – Giorgio Camerani Sep 13 '10 at 15:25
  • 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) – Tsuyoshi Ito Sep 13 '10 at 15:46
  • (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 Sep 13 '10 at 15:46
  • 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 Sep 13 '10 at 16:20
  • 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 Sep 13 '10 at 16:47
  • 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 Dec 12 '21 at 02:37
3

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)
Tuomas Laakkonen
  • 191
  • 1
  • 3
  • 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 May 03 '23 at 21:21
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.

Gregory Morse
  • 109
  • 3