Sharp-SAT

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

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

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

#P-Полнота

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

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

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

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

#3СБ

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

#2СБ

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

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

#Horn-SAT

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

Планар #3SAT

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

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

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

#DNF

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

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

Особые случаи, поддающиеся разрешению

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

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

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

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

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

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

Обобщения

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

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

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

Ссылки

1. Валиант, LG (1979). «Сложность вычисления постоянного». Теоретическая информатика . 8 (2): 189–201. doi : 10.1016/0304-3975(79)90044-6 .
2. Вадхан, Салил Вадхан (20 ноября 2018 г.). «Лекция 24: Проблемы со счетом» (PDF) .
3. Валиант, Лесли Г. (1979). «Сложность проблем перечисления и надежности». Журнал SIAM по вычислениям . 8 (3): 410–421. doi :10.1137/0208032.
4. Лю, Цзинчэн; Лу, Пиньян (2015). FPTAS для подсчета монотонных КНФ. Общество промышленной и прикладной математики. стр. 1531–1548. arXiv : 1311.3728 . doi :10.1137/1.9781611973730.101. ISBN 978-1-61197-374-7.
5. Creignou, Nadia; Hermann, Miki (1996). «Сложность проблем подсчета обобщенной выполнимости». Информация и вычисления . 125 : 1–12. doi :10.1006/inco.1996.0016. hdl : 10068/41883 .
6. Лихтенштейн, Дэвид (1982). «Планарные формулы и их использование». Журнал SIAM по вычислениям . 11 (2): 329–343. doi :10.1137/0211025.
7. de Berg, Mark ; Khosravi, Amirali (2010). "Optimal binary space partitions in the plane". На тайском языке, My T.; Sahni, Sartaj (ред.). Computing and Combinatorics: 16th Annual International Conference, COCOON 2010, Nha Trang, Vietnam, July 19-21, 2010, Proceedings . Lecture Notes in Computer Science. Vol. 6196. Berlin: Springer. pp. 216–225. doi :10.1007/978-3-642-14031-0_25. ISBN 978-3-642-14030-3. МР  2720098.
8. Сучу, Дэн; Олтяну, Дэн; Ре, Кристофер; Кох, Кристоф (2011), Сучу, Дэн; Олтяну, Дэн; Ре, Кристофер; Кох, Кристоф (ред.), «Проблема оценки запроса», Вероятностные базы данных , Синтезирующие лекции по управлению данными, Cham: Springer International Publishing, стр. 45–52, номер документа : 10.1007/978-3-031-01879-4_3, ISBN 978-3-031-01879-4, получено 2023-09-16
9. Карп, Ричард М.; Луби, Майкл; Мадрас, Нил (1989-09-01). «Аппроксимационные алгоритмы Монте-Карло для задач перечисления». Журнал алгоритмов . 10 (3): 429–448. doi :10.1016/0196-6774(89)90038-2. ISSN  0196-6774.
10. Creignou, Nadia; Hermann, Miki (1996-02-25). «Сложность проблем подсчета обобщенной выполнимости». Информация и вычисления . 125 (1): 1–12. doi : 10.1006/inco.1996.0016 . ISSN  0890-5401.
11. FICHTE, JOHANNES K.; HECHER, MARKUS; THIER, PATRICK; WOLTRAN, STEFAN (2021-03-12). «Использование систем управления базами данных и ширины дерева для подсчета». Теория и практика логического программирования . 22 (1): 128–157. arXiv : 2001.04191 . doi :10.1017/s147106842100003x. ISSN  1471-0684.
12. Чавира, Марк; Дарвич, Аднан (апрель 2008 г.). «О вероятностном выводе с помощью подсчета взвешенных моделей». Искусственный интеллект . 172 (6–7): 772–799. doi :10.1016/j.artint.2007.11.002.
13. Киммиг, Анжелика; Ван ден Брук, Гай; Де Радт, Люк (июль 2017 г.). «Алгебраический расчет моделей». Журнал прикладной логики . 22 : 46–62. arXiv : 1211.4475 . дои : 10.1016/j.jal.2016.11.031.