SAT únicos vs modelos Exactamente

El SAT único es el problema bien conocido: dada una fórmula CNF , ¿es cierto que F tiene exactamente un modelo?$F$$F$

Estoy interesado en el problema «Exactamente -SAT»: dada una fórmula F de CNF y un entero m > 1 , ¿es cierto que F tiene exactamente m modelos?$m$$F$$m>1$$F$$m$

Ambos problemas se parecen. Entonces mis preguntas son:

1- ¿Es «exacto -SAT» polytime (muchos uno o Turing) reducible a Unique SAT?$m$

2- ¿Conoces alguna referencia sobre el tema?

Gracias por sus respuestas.

Adición , primeros artículos sobre la complejidad de Exactly SAT:$m$

1- Janos Simon, sobre la diferencia entre uno y muchos, en las actas del cuarto coloquio sobre autómatas, idiomas y programación, 480-491, 1977.

2- Klaus W. Wagner, La complejidad de los problemas combinatorios con una representación de entrada sucinta, Acta Informatica, 23, 325-356, 1986.

En ambos artículos, Exactamente SAT ( m ≥ 1 ) se muestra como C = completo (bajo muchas reducciones), donde la clase C es de la Jerarquía de Conteo (CH) de clases de complejidad. De manera informal, C contiene todos los problemas que se pueden expresar como de decidir si una instancia dada tiene al menos m muchas pruebas de tamaño polinómicos (la clase C se conoce para coincidir con la clase P P ). La clase C = es una variante de C , donde "exactamente m " reemplaza "al menos m ".$m$$m \geq 1$$C=$$C$$C$$m$$C$$PP$$C=$$C$$m$$m$

$m$

$m$