Jump to content

Шарп-САТ

В информатике проблема выполнимости Шарпа (иногда называемая 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-полная). Сюда входит следующее.

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

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

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

Аналогично, хотя выполнимость по Хорну полиномиальна, подсчет количества решений #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]

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