Шарп-САТ
Эта статья нуждается в дополнительных цитатах для проверки . ( июнь 2019 г. ) |
В информатике проблема выполнимости Шарпа (иногда называемая Sharp-SAT , #SAT или подсчет моделей ) — это проблема подсчета количества интерпретаций , удовлетворяющих заданной булевой формуле , введенная Валиантом в 1979 году. [1] Другими словами, он спрашивает, сколькими способами переменные данной логической формулы могут быть последовательно заменены значениями ИСТИНА или ЛОЖЬ таким образом, чтобы формула имела значение ИСТИНА . Например, формула выполнимо тремя различными присвоениями логических значений переменных, а именно, для любого из присвоений ( = ИСТИНА, = ЛОЖЬ), ( = ЛОЖЬ, = ЛОЖЬ) и ( = ИСТИНА, = ИСТИНА), имеем
#SAT отличается от задачи булевой выполнимости (SAT), которая спрашивает, существует ли решение булевой формулы. Вместо этого #SAT просит перечислить все решения булевой формулы. #SAT сложнее, чем SAT, в том смысле, что, как только известно общее количество решений булевой формулы, SAT можно решить за постоянное время. Однако обратное неверно, поскольку знание того, что булева формула имеет решение , не помогает нам подсчитать все решения , поскольку существует экспоненциальное число возможностей.
#SAT — известный пример класса задач на счёт , известного как #P-complete (читается как «точное P завершение»). Другими словами, каждый экземпляр проблемы класса сложности #P можно свести к экземпляру проблемы #SAT. Это важный результат, поскольку многие сложные задачи счета возникают в перечислительной комбинаторике , статистической физике , надежности сетей и искусственном интеллекте без какой-либо известной формулы. Если показано, что проблема сложна, это дает теоретическое объяснение отсутствия красивых формул. [2]
#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 -полным. [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-полной.
#ДНФ
[ редактировать ]Для формул дизъюнктивной нормальной формы (ДНФ) подсчет решений также #P -полный, даже если все предложения имеют размер 2 и нет отрицаний : это потому, что по законам Де Моргана подсчет количества решений ДНФ составляет к подсчету количества решений отрицания формулы конъюнктивной нормальной формы (КНФ). Неразрешимость сохраняется даже в случае, известном как #PP2DNF, когда переменные разделены на два набора, причем каждое предложение содержит по одной переменной из каждого набора. [8]
Напротив, можно легко аппроксимировать количество решений формулы дизъюнктивной нормальной формы, используя алгоритм Карпа-Луби , который является FPRAS для этой задачи. [9]
Разрешаемые особые случаи
[ редактировать ]Проблемы удовлетворения аффинных ограничений
[ редактировать ]Вариант SAT, соответствующий аффинным отношениям в смысле теоремы дихотомии Шефера , т.е. где предложения представляют собой уравнения по модулю 2 с оператором XOR , является единственным вариантом SAT, для которого проблема #SAT может быть решена за полиномиальное время. [10]
Ограниченная ширина дерева
[ редактировать ]Если экземпляры SAT ограничены с помощью параметров графа , проблема #SAT может стать разрешимой. Например, #SAT на экземплярах SAT, ширина дерева которых ограничена константой, может выполняться за полиномиальное время . [11] Здесь ширина дерева может быть шириной основного дерева, двойной шириной дерева или шириной дерева инцидентности гиперграфа , связанного с формулой SAT, вершины которого являются переменными и где каждое предложение представлено как гиперребро.
Ограниченные классы схем и схем
[ редактировать ]Подсчет моделей возможен (решается за полиномиальное время) для (упорядоченных) BDD и для некоторых схемных формализмов, изучаемых при компиляции знаний , таких как d-DNNF .
Обобщения
[ редактировать ]Взвешенный подсчет моделей (WMC) обобщает #SAT, вычисляя линейную комбинацию моделей, а не просто подсчитывая модели. В варианте WMC с литеральным взвешиванием каждому литералу присваивается вес, такой что .
WMC используется для вероятностного вывода, поскольку вероятностные запросы над дискретными случайными величинами, например, в байсовских сетях, могут быть сведены к WMC. [12]
Алгебраическая модель подсчета дополнительно обобщает #SAT и WMC на произвольные коммутативные полукольца . [13]
Ссылки
[ редактировать ]- ^ Валиант, Л.Г. (1979). «Сложность вычислений перманентна» . Теоретическая информатика . 8 (2): 189–201. дои : 10.1016/0304-3975(79)90044-6 .
- ^ Вадхан, Салил Вадхан (20 ноября 2018 г.). «Лекция 24: Проблемы со счетом» (PDF) .
- ^ Валиант, Лесли Г. (1979). «Сложность перечисления и проблемы надежности». SIAM Journal по вычислительной технике . 8 (3): 410–421. дои : 10.1137/0208032 .
- ^ Лю, Цзинчэн; Лу, Пиньян (2015). «ФПТАС для подсчета монотонных КНФ» . Общество промышленной и прикладной математики: 1531–1548. arXiv : 1311.3728 . дои : 10.1137/1.9781611973730.101 . ISBN 978-1-61197-374-7 .
{{cite journal}}
: Для цитирования журнала требуется|journal=
( помощь ) - ^ Крейну, Надя; Германн, Мики (1996). «Сложность задач подсчета обобщенной выполнимости». Информация и вычисления . 125 : 1–12. дои : 10.1006/inco.1996.0016 . hdl : 10068/41883 .
- ^ Лихтенштейн, Дэвид (1982). «Плоские формулы и их использование». SIAM Journal по вычислительной технике . 11:2 (2): 329–343. дои : 10.1137/0211025 .
- ^ Jump up to: а б де Берг, Марк ; Хосрави, Амирали (2010). «Оптимальные разбиения двоичного пространства на плоскости». На тайском языке My T.; Сахни, Сартадж (ред.). Вычисления и комбинаторика: 16-я ежегодная международная конференция COCOON 2010, Нячанг, Вьетнам, 19–21 июля 2010 г., Материалы . Конспекты лекций по информатике. Том. 6196. Берлин: Шпрингер. стр. 216–225. дои : 10.1007/978-3-642-14031-0_25 . МР 2720098 .
- ^ Сучу, Дэн; Олтяну, Дэн; Ре, Кристофер; Кох, Кристоф (2011), Сучу, Дэн; Олтяну, Дэн; Ре, Кристофер; Кох, Кристоф (ред.), «Проблема оценки запросов» , Вероятностные базы данных , Синтезирующие лекции по управлению данными, Cham: Springer International Publishing, стр. 45–52, номер документа : 10.1007/978-3-031-01879-4_3 , ISBN 978-3-031-01879-4 , получено 16 сентября 2023 г.
- ^ Карп, Ричард М; Луби, Майкл; Мадрас, Нил (1 сентября 1989 г.). «Алгоритмы аппроксимации Монте-Карло для задач перечисления» . Журнал алгоритмов . 10 (3): 429–448. дои : 10.1016/0196-6774(89)90038-2 . ISSN 0196-6774 .
- ^ Крейну, Надя; Германн, Мики (25 февраля 1996 г.). «Сложность задач подсчета обобщенной выполнимости» . Информация и вычисления . 125 (1): 1–12. дои : 10.1006/inco.1996.0016 . ISSN 0890-5401 .
- ^ ФИХТЕ, ИОХАННЕС К.; ХЕЧЕР, МАРКУС; Тьер, Патрик; ВОЛТРАН, СТЕФАН (12 марта 2021 г.). «Использование систем управления базами данных и ширины дерева для подсчета» . Теория и практика логического программирования . 22 (1): 128–157. arXiv : 2001.04191 . дои : 10.1017/s147106842100003x . ISSN 1471-0684 .
- ^ Чавира, Марк; Дарвич, Аднан (апрель 2008 г.). «О вероятностном выводе путем подсчета взвешенных моделей». Искусственный интеллект . 172 (6–7): 772–799. дои : 10.1016/j.artint.2007.11.002 .
- ^ Киммиг, Анжелика; Ван ден Брук, Гай; Де Радт, Люк (июль 2017 г.). «Алгебраический расчет моделей». Журнал прикладной логики . 22 : 46–62. arXiv : 1211.4475 . дои : 10.1016/j.jal.2016.11.031 .