# Reduction over Exactly $m$ models

Let introduce the "Exactly $\{m_{1},m_{2}\}$-SAT" problem : Given a CNF formula $F$ and $2$ integers $m_{1}$ and $m_{2}$, is it true that $F$ has exactly $m_{1}$ or $m_{2}$ models ?

I guess Exactly $\{m_{1},m_{2}\}$-SAT ($m_{1}\leq m_{2}$) is many-one polynomial time reducible to the parametrized problem "Exactly $m_2$-SAT" with $m_2$ considered as a parameter : Given a CNF formula $F$ is it true that $F$ has exactly $m_{2}$ models.

Is it correct ?

No, that's not correct. Finding the solution to an Exactly {$m_1$,$m_2$}-SAT problem can't be done with a single call to an Exactly {$m$}-SAT solver for any $m$, so there is no many-one reduction from the former to the latter. The weaker Turing reduction does apply, since you can solve Exactly {$m_1$,$m_2$}-SAT problem with at most two calls to an Exactly {$m$}-SAT solver.
• Tks for your answer. Let me reformulate the question : consider $m_1$ and $m_2$ as parameters, is it possible to solve Exactly $\{m_1,m_2\}$-SAT in polynomial time with a single call to Exactly $m_2$-SAT ? – Xavier Labouze Jan 2 '12 at 22:34
• Only if $m_1 = m_2$. Otherwise the call tells you nothing useful about the $m_1$ case. – Kyle Jones Jan 2 '12 at 23:51