Задача выполнимости булевых формул
Зада́ча выполни́мости бу́левых фо́рмул (SAT или ВЫП) — важная для теории вычислительной сложности алгоритмическая задача.
Экземпляром задачи SAT является булева формула, состоящая только из имен переменных, скобок и операций <math>\wedge</math> (И), <math>\vee</math> (ИЛИ) и <math>\neg</math> (HE). Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной.
Согласно теореме Кука, доказанной Стивеном Куком в 1971-м году, задача SAT для булевых формул, записанных в конъюнктивной нормальной форме, является NP-полной. Требование о записи в конъюнктивной форме существенно, так как, например, задача SAT для формул, представленных в дизъюнктивной нормальной форме, тривиально решается за линейное время от размера записи формулы.
Точная формулировка
Чтобы четко сформулировать задачу распознавания, необходимо условиться об алфавите, с помощью которого задаются экземпляры языка. Этот алфавит должен быть фиксирован и конечен. В своей книге Хопкрофт, Мотвани и Ульман предлагают использовать следующий алфавит: {«<math>\wedge</math>», «<math>\vee</math>», «<math>\neg</math>», «<math>(</math>», «<math>)</math>», «<math>x</math>», «<math>0</math>», «<math>1</math>»}.
При использовании такого алфавита скобки и операторы записываются естественным образом, а переменные получают следующие имена: x1, x10, x11, x100 и т. д., согласно их номерам, записанным в двоичной системе счисления.
Пусть некоторая булева формула, записанная в обычной математической нотации, имела длину <math>N</math> символов. В ней каждое вхождение каждой переменной было описано хотя бы одним символом, следовательно, всего в данной формуле не более <math>N</math> переменных. Значит, в предложенной выше нотации каждая переменная будет записана с помощью <math>O\left(\log{N}\right)</math> символов. В таком случае, вся формула в новой нотации будет иметь длину <math>O\left(N\log{N}\right)</math> символов, то есть длина строки возрастет в полиномиальное число раз.
Например, формула <math>a\wedge\neg(b\vee c)</math> примет вид <math>x1\wedge\neg(x10\vee x11)</math>.
Вычислительная сложность
В 1971-м году в статье Стивена Кука был впервые введен термин «NP-полная задача», и задача SAT была первой задачей, для которой доказывалось это свойство.
В доказательстве теоремы Кука каждая задача из класса NP в явном виде сводится к SAT. После появления результатов Кука была доказана NP-полнота для множества других задач. При этом чаще всего для доказательства NP-полноты некоторой задачи приводится полиномиальное сведение задачи SAT к данной задаче, возможно в несколько шагов, то есть с использованием нескольких промежуточных задач.
Частные случаи задачи SAT
Интересными важными частными случаями задачи SAT являются:
- Задача выполнимости булевых формул в конъюнктивной нормальной форме (SATCNF или ВКНФ) — аналогичная задача, с наложенной на формулу условием: она должна быть записана в конъюнктивной нормальной форме. Задача ВКНФ также NP-полна.
- Задача выполнимости булевых формул в k-конъюнктивной нормальной форме (k-SAT или k-ВЫП) — задача выполнимости при условии, что формула записана в k-конъюнктивной нормальной форме. Эта задача является NP-полной при <math>k\geq 3</math>.
- Задача выполнимости булевых формул в 2-конъюнктивной нормальной форме имеет полиномиальное решение, то есть принадлежит классу P.
См. также
Ссылки
- 2.5-ВЫПОЛНИМОСТЬ (вопросы сведения 3-SAT к 2-SAT)
- The international SAT Competitions web page
- SATLIB - The Satisfiability Library
- Sat Live - общий сайт о SAT.
Примечания
de:Erfüllbarkeitsproblem der Aussagenlogik en:Boolean satisfiability problem eo:Bulea plenumebloproblemo es:Problema de satisfacibilidad booleana fr:Problème SAT he:בעיית הספיקות it:Soddisfacibilità booleana ja:充足可能性問題 ko:충족 가능성 문제 nl:Vervulbaarheidsprobleem pl:Problem spełnialności sr:САТ проблем th:ปัญหาความสอดคล้องแบบบูล uk:Задача здійсненностіі бульових формул zh:布尔可满足性问题
Если вам нравится SbUP.com Сайт, вы можете поддержать его - BTC: bc1qppjcl3c2cyjazy6lepmrv3fh6ke9mxs7zpfky0 , TRC20 и ещё....