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$?
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
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)
#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.
