Шарп-САТ

В информатике проблема выполнимости Шарпа (иногда называемая Sharp-SAT , #SAT или подсчет моделей ) — это проблема подсчета количества интерпретаций , удовлетворяющих заданной булевой формуле , введенная Валиантом в 1979 году. Другими словами, он спрашивает, сколькими способами переменные данной логической формулы могут быть последовательно заменены значениями ИСТИНА или ЛОЖЬ таким образом, чтобы формула имела значение ИСТИНА . Например, формула $a\lor \neg b$ выполнимо тремя различными присвоениями логических значений переменных, а именно, для любого из присвоений ( $a$ = ИСТИНА, $b$ = ЛОЖЬ), ( $a$ = ЛОЖЬ, $b$ = ЛОЖЬ) и ( $a$ = ИСТИНА, $b$ = ИСТИНА), имеем $a\lor \neg b={\textsf {TRUE}}.$

#SAT отличается от задачи булевой выполнимости (SAT), которая спрашивает, существует ли решение булевой формулы. Вместо этого #SAT просит перечислить все решения булевой формулы. #SAT сложнее, чем SAT, в том смысле, что, как только известно общее количество решений булевой формулы, SAT можно решить за постоянное время. Однако обратное неверно, поскольку знание того, что булева формула имеет решение , не помогает нам подсчитать все решения , поскольку существует экспоненциальное число возможностей.

#SAT — известный пример класса задач на счёт , известного как #P-complete (читается как «точное P завершение»). Другими словами, каждый экземпляр проблемы класса сложности #P можно свести к экземпляру проблемы #SAT. Это важный результат, поскольку многие сложные задачи счета возникают в перечислительной комбинаторике , статистической физике , надежности сетей и искусственном интеллекте без какой-либо известной формулы. Если показано, что проблема сложна, это дает теоретическое объяснение отсутствия красивых формул.

#P-Полнота

#SAT является #P-полным . Чтобы доказать это, сначала заметим, что #SAT явно находится в #P.

Далее мы докажем, что #SAT #P-труден. Возьмите любую задачу #А из #P. Мы знаем, что A можно решить с помощью недетерминированной машины Тьюринга M. С другой стороны, из доказательства теоремы Кука-Левина мы знаем, что мы можем свести M к логической формуле F. Теперь каждое допустимое присвоение F соответствует уникальному приемлемому пути в M, и наоборот. Однако каждый приемлемый путь, выбранный M, представляет собой решение A. Другими словами, существует взаимное соответствие между действительными назначениями F и решениями A. Таким образом, сокращение, используемое в доказательстве теоремы Кука-Левина, является экономным. Это означает, что #SAT является #P-сложным.

Трудноразрешимые особые случаи

Подсчет решений неразрешим (#P-полный) во многих особых случаях, для которых выполнимость разрешима (в P), а также когда выполнимость неразрешима (NP-полная). Сюда входит следующее.

#3САТ

Это счетная версия 3SAT . Можно показать, что любую формулу в SAT можно переписать в виде формулы в форме 3- КНФ с сохранением числа удовлетворяющих присвоений. Следовательно, #SAT и #3SAT считаются эквивалентными, а #3SAT также #P-полным.

#2САТ

Несмотря на то, что 2SAT (решение о том, имеет ли формула 2CNF решение) является полиномиальным, подсчет количества решений является #P -полным. #P-полнота уже в монотонном случае, т. е. когда нет отрицаний (#MONOTONE-2-CNF).

Известно, что, предполагая, что NP отличается от RP , #MONOTONE-2-CNF также не может быть аппроксимирован полностью полиномиальной схемой аппроксимации (FPRAS), даже если предположить, что каждая переменная встречается не более чем в 6 предложениях, но что Схема аппроксимации полностью полиномиального времени (FPTAS) существует, когда каждая переменная встречается не более чем в 5 предложениях: это следует из аналогичных результатов по задаче ♯IS подсчета числа независимых множеств в графах .

#Horn-SAT

Аналогично, хотя выполнимость по Хорну полиномиальна, подсчет количества решений #P-полный. Этот результат следует из общей дихотомии, характеризующей, какие SAT-подобные задачи являются #P-полными.

Планар #3SAT

Это счетная версия Planar 3SAT . Снижение твердости с 3SAT до Planar 3SAT, данное Лихтенштейном. является экономным. Это означает, что Planar #3SAT является #P-полным.

Плоский Монотонный Прямолинейный #3SAT

Это счетная версия Planar Monotone Rectilinear 3SAT. Снижение твердости NP, данное де Бергом и Хосрави. является экономным. Следовательно, эта задача также является #P-полной.

#ДНФ

Для формул дизъюнктивной нормальной формы (ДНФ) подсчет решений также #P -полный, даже если все предложения имеют размер 2 и нет отрицаний : это потому, что по законам Де Моргана подсчет количества решений ДНФ составляет к подсчету количества решений отрицания формулы конъюнктивной нормальной формы (КНФ). Неразрешимость сохраняется даже в случае, известном как #PP2DNF, когда переменные разделены на два набора, причем каждое предложение содержит по одной переменной из каждого набора.

Напротив, можно легко аппроксимировать количество решений формулы дизъюнктивной нормальной формы, используя алгоритм Карпа-Луби , который является FPRAS для этой задачи.

Разрешаемые особые случаи

Проблемы удовлетворения аффинных ограничений

Вариант SAT, соответствующий аффинным отношениям в смысле теоремы дихотомии Шефера , т.е. где предложения представляют собой уравнения по модулю 2 с оператором XOR , является единственным вариантом SAT, для которого проблема #SAT может быть решена за полиномиальное время.

Ограниченная ширина дерева

Если экземпляры SAT ограничены с помощью параметров графа , проблема #SAT может стать разрешимой. Например, #SAT на экземплярах SAT, ширина дерева которых ограничена константой, может выполняться за полиномиальное время . Здесь ширина дерева может быть шириной основного дерева, двойной шириной дерева или шириной дерева инцидентности гиперграфа , связанного с формулой SAT, вершины которого являются переменными и где каждое предложение представлено как гиперребро.

Ограниченные классы схем и схем

Подсчет моделей возможен (решается за полиномиальное время) для (упорядоченных) BDD и для некоторых схемных формализмов, изучаемых при компиляции знаний , таких как d-DNNF .

Обобщения

Взвешенный подсчет моделей (WMC) обобщает #SAT, вычисляя линейную комбинацию моделей, а не просто подсчитывая модели. В варианте WMC с литеральным взвешиванием каждому литералу присваивается вес, такой что ${\text{WMC}}(\phi ;w)=\sum _{M\models \phi }\prod _{l\in M}w(l)$.

WMC используется для вероятностного вывода, поскольку вероятностные запросы над дискретными случайными величинами, например, в байсовских сетях, могут быть сведены к WMC.

Алгебраическая модель подсчета дополнительно обобщает #SAT и WMC на произвольные коммутативные полукольца .