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? Thank you for your answers.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 giveninstance 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$.
Unique SAT vs Exactly $m$ models
cc.complexity theory;reference request;np hardness;sat;reductions
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.