Уникальные SAT против ровно

Уникальная SAT является хорошо известной проблемой: учитывая формулу CNF , верно ли, что F имеет ровно одну модель?$F$$F$

Меня интересует проблема «точно -SAT»: учитывая формулу CNF F и целое число m > 1 , правда ли, что F имеет ровно m моделей?$m$$F$$m>1$$F$$m$

Обе проблемы выглядят одинаково. Итак, мои вопросы:

1- Приводит ли Polytime «точно -SAT» (много-один или Тьюринг) к уникальному SAT?$m$

2- Знаете ли вы какие-либо ссылки на эту тему?

Спасибо за ваши ответы.

Приложение , первые статьи о сложности Exactly SAT:$m$

1- Янош Симон, «О разнице между одним и многими», в трудах четвертого коллоквиума по автоматам, языкам и программированию, 480–491, 1977.

2. Клаус В. Вагнер. Сложность комбинаторных задач с кратким входным представлением, Acta Informatica, 23, 325-356, 1986.

В обеих статьях показано , что точно SAT ( m ≥ 1 ) является C = полной (при сокращениях много-один), где класс C относится к Иерархии подсчета (CH) классов сложности. Неформально C содержит все проблемы, которые можно выразить как решение о том, имеет ли данный экземпляр хотя бы m много полиномиальных размерных доказательств (известно, что класс C совпадает с классом P P ). Класс C = является вариантом C , где «ровно m » заменяет «не менее m ».$m$$m \geq 1$$C=$$C$$C$$m$$C$$PP$$C=$$C$$m$$m$

$m$

$m$