Главная
Новости
Строительство
Ремонт
Дизайн и интерьер

















Яндекс.Метрика

Задача выполнимости булевых формул

Задача выполнимости булевых формул (SAT или ВЫП) — важная для теории вычислительной сложности алгоритмическая задача.

Экземпляром задачи SAT является булева формула, состоящая только из имен переменных, скобок и операций ∧ {displaystyle wedge } (И), ∨ {displaystyle vee } (ИЛИ) и ¬ {displaystyle eg } (HE). Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной.

Согласно теореме Кука, доказанной Стивеном Куком в 1971 году, задача SAT для булевых формул, записанных в конъюнктивной нормальной форме, является NP-полной. Требование о записи в конъюнктивной форме существенно, так как, например, задача SAT для формул, представленных в дизъюнктивной нормальной форме, тривиально решается за линейное время в зависимости от размера записи формулы (для выполнимости формулы требуется только наличие хотя бы одной конъюнкции, не содержащей одновременно x и NOT x для некоторой переменной x).

Точная формулировка

Чтобы чётко сформулировать задачу распознавания, необходимо условиться об алфавите, с помощью которого задаются экземпляры языка. Этот алфавит должен быть фиксирован и конечен. В своей книге Хопкрофт, Мотвани и Ульман предлагают использовать следующий алфавит: {« ∧ {displaystyle wedge } », « ∨ {displaystyle vee } », « ¬ {displaystyle eg } », « ( {displaystyle (} », « ) {displaystyle )} », « x {displaystyle x} », « 0 {displaystyle 0} », « 1 {displaystyle 1} »}.

При использовании такого алфавита скобки и операторы записываются естественным образом, а переменные получают следующие имена: x1, x10, x11, x100 и т. д., согласно их номерам, записанным в двоичной системе счисления.

Пусть некоторая булева формула, записанная в обычной математической нотации, имела длину N {displaystyle N} символов. В ней каждое вхождение каждой переменной было описано хотя бы одним символом, следовательно, всего в данной формуле не более N {displaystyle N} переменных. Значит, в предложенной выше нотации каждая переменная будет записана с помощью O ( log ⁡ N ) {displaystyle Oleft(log {N} ight)} символов. В таком случае, вся формула в новой нотации будет иметь длину O ( N log ⁡ N ) {displaystyle Oleft(Nlog {N} ight)} символов, то есть длина строки возрастет в полиномиальное число раз.

Например, формула a ∧ ¬ ( b ∨ c ) {displaystyle awedge eg (bvee c)} примет вид x 1 ∧ ¬ ( x 10 ∨ x 11 ) {displaystyle x1wedge eg (x10vee x11)} .

Вычислительная сложность

В 1970-м году в статье Стивена Кука был впервые введен термин «NP-полная задача», и задача SAT была первой задачей, для которой доказывалось это свойство.

В доказательстве теоремы Кука каждая задача из класса NP в явном виде сводится к SAT. После появления результатов Кука была доказана NP-полнота для множества других задач. При этом чаще всего для доказательства NP-полноты некоторой задачи приводится полиномиальная сводимость задачи SAT к данной задаче, возможно в несколько шагов, то есть с использованием нескольких промежуточных задач.

Частные случаи задачи SAT

Интересными важными частными случаями задачи SAT являются:

  • Задача выполнимости булевых формул в конъюнктивной нормальной форме (SATCNF или ВКНФ) — аналогичная задача, с наложенным на формулу условием: она должна быть записана в конъюнктивной нормальной форме. Задача ВКНФ также NP-полна.
  • Задача выполнимости булевых формул в k-конъюнктивной нормальной форме (k-SAT или k-ВЫП) — задача выполнимости при условии, что формула записана в k-конъюнктивной нормальной форме. Эта задача является NP-полной при k ≥ 3 {displaystyle kgeq 3} .
  • Задача выполнимости булевых формул в 2-конъюнктивной нормальной форме имеет полиномиальное решение, то есть принадлежит классу P.

CDCL-решатели

Одним из наиболее эффективных методов распараллеливания задач SAT являются CDCL-решатели (CDCL, англ. conflict-driven clause learning), основывающиеся на нехронологических вариантах алгоритма DPLL.