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 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$".