Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску
Правильный заголовок этой статьи - #SAT . Замена # связана с техническими ограничениями .

В информатике , то Sharp выполнимости проблема (иногда называемый Sharp-СБ или #SAT ) является проблема подсчета числа интерпретаций , что удовлетворяет данная булева формула , введенный Отважном в 1979 году [1] Другими словами, он спрашивает сколько способов переменные данной логической формулы могут быть последовательно заменены значениями ИСТИНА или ЛОЖЬ таким образом, чтобы формула оценивалась как ИСТИНА . Например, формула может быть выполнена с помощью трех различных логических значений переменных, а именно, для любого из присвоений ( = ИСТИНА, = ЛОЖЬ), ( = ЛОЖЬ, = ЛОЖЬ), ( = ИСТИНА, = ИСТИНА), мы имеем = ИСТИНА.

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

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

# P-Завершенность [ править ]

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

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

Непреодолимые особые случаи [ править ]

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

# 3SAT [ править ]

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

# 2SAT [ править ]

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

# Horn-SAT [ править ]

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

Планар №3САТ [ править ]

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

Планарный монотонный прямолинейный # 3SAT [ править ]

Это счетная версия Planar Monotone Rectilinear 3SAT. [5] Снижение NP-твердости, данное de Berg & Khosravi [5], является скупым. Следовательно, эта задача также является # P-полной.

Подчиняемые особые случаи [ править ]

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

Программное обеспечение [ править ]

SharpSAT - это программа для решения практических примеров проблемы #SAT. "SharpSAT - Марк Терли" . sites.google.com . Проверено 30 апреля 2019 .

Ссылки [ править ]

  1. Перейти ↑ Valiant, LG (1979). «Сложность вычисления постоянного». Теоретическая информатика . 8 (2): 189–201. DOI : 10.1016 / 0304-3975 (79) 90044-6 .
  2. ^ Vadhan, Салил Вадхен (20 ноября 2018). «Лекция 24: Задачи подсчета» (PDF) .
  3. ^ Крейну, Надя; Германн, Мики (1996). «Сложность задач подсчета обобщенной выполнимости». Информация и вычисления . 125 : 1–12. DOI : 10.1006 / inco.1996.0016 . ЛВП : 10068/41883 .
  4. ^ Лихтенштейн, Дэвид (1982). «Планарные формулы и их использование». SIAM Journal on Computing . 11: 2 : 329–343.
  5. ^ а б Хосрави, Амирали; Берг, Марк де (2010). «Оптимальные двоичные разбиения пространства на плоскости» . не определено . Проверено 1 мая 2019 .