# Unique SAT vs Exactly $m$ models

Unique SAT is the well known problem : given a CNF formula $F$, is it true that $F$ has exactly one model ?

I am interested in « Exactly $m$-SAT » problem : given a CNF formula $F$ and an integer $m>1$, is it true that $F$ has exactly $m$ models ?

Both problems look similar. So my questions are :

1- Is «Exactly $m$-SAT » polytime (many-one or Turing) reducible to Unique SAT?

2- Do you know any reference on the subject ?

Addendum, first articles about complexity of Exactly $m$ SAT :

1- Janos Simon, On the Difference Between One and Many, In Proceedings of the Fourth Colloquium on Automata, Languages and Programming, 480-491, 1977.

2- Klaus W. Wagner, The complexity of combinatorial problems with succinct input representation, Acta Informatica, 23, 325-356, 1986.

In both articles, Exactly $m$ SAT ($m \geq 1$) is shown to be $C=$ complete (under many-one reductions), where the class $C$ is from the Counting Hierarchy (CH) of complexity classes. Informally, $C$ contains all problems which can be expressed as deciding whether a given instance has at least $m$ many polynomial size proofs (the class $C$ is known to coincide with the class $PP$). The class $C=$ is a variant of $C$, where “exactly $m$” replaces “at least $m$".

-
It is polytime Turing reducible: find a solution, add a clause eliminating it, and repeat till the formula becomes unsatisfiable. –  Kaveh Sep 27 '11 at 6:06
1. the machine will tell the number of solutions or that it has more than $m$ solutions. 2. you can add the negation of conjunction describing the solution. –  Kaveh Sep 27 '11 at 21:05
If you do not know the relation between PP and counting the number of solutions, please check a textbook on complexity theory such as Papadimitriou. –  Tsuyoshi Ito Sep 30 '11 at 13:51
(1) If m is polynomially bounded, your problem is polynomial-time many-one reducible to Unique SAT by treating a list of m solutions sorted in the lexicographical order as a single certificate. (2) Please do not take my giving an answer as an evidence that you asked your question in the right place. I think that this particular question is on the border line between on-topic and off-topic. You should really consider asking your future questions somewhere else. –  Tsuyoshi Ito Oct 2 '11 at 23:37
Although you state that m is polynomially bounded, some of the statements in the question require m to be arbitrary and no longer hold if you constrain m to be polynomially bounded. You have to understand what you are talking about before you can ask a coherent question. This is why I do not want to post an answer to this question here, where questions are expected to be at research level. –  Tsuyoshi Ito Oct 8 '11 at 13:05

For general $m$, exactly-m-sat is strictly harder than u-sat (thus does not reduce to it) unless the PH collapses. The reason is that PP can be obtained using an existential quantifier over exactly-m-SAT queries (exists m>(half of the assignments) such that exactly-m-SAT), thus if exactly-m-sat is in the k'th level of PH, then PP is in the (k+1)'st level, and then the hierarchy collapses (since P^PP contains PH). But u-sat is clearly in the second level of PH (actually in a subclass called DP).
On the other hand, as @Tsuyoshi mentioned above, if $m$ is polynomial, then exactly-m-sat is many-one reudcible to u-sat.
Thank you for your answer. 1) If $m$ is small enough (ie polynomially bounded in $n$, the size of the formula) then Exactly $m$ SAT is reducible to US. Besides, if $m$, as part of the input, is big enough (ie $m= 2^{O(n)}$) then Exactly $m$ SAT is in P. Why would it be such a drastic change for $m$ in between ? 2) What do you think of the update post ? (why is it not correct ?) –  Xavier Labouze Oct 11 '11 at 7:39
$m$ is part of the input. Let introduce $m$ new variables, $y_1,y_2 \cdots y_m$. Let $F'=F\land y_1 \land y_2 \land \cdots \land y_m$. $F'$ has exactly the same number of models as $F$, and $m$ is polynomially bound in the size of $F'$. Why not conclude that the reduction to US (via $F'$) holds ? –  Xavier Labouze Oct 12 '11 at 22:27
$F'$ is exponential in size of $F$ (if $m$ is exponential in $|F|$), thus the reduction is not poly-time in general. –  Opt Oct 15 '11 at 0:48