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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

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

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

Точная формулировка[править | править вики-текст]

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

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

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

Например, формула a\wedge\neg(b\vee c) примет вид x1\wedge\neg(x10\vee x11).

Вычислительная сложность[править | править вики-текст]

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

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

Частные случаи задачи SAT[править | править вики-текст]

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

CDCL-решатели[править | править вики-текст]

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

См. также[править | править вики-текст]

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

Примечания[править | править вики-текст]

  1. Marques-Silva J. P. GRASP: A search algorithm for propositional satisfiability / J. P. Marques-Silva, K. A. Sakallah // IEEE Transactions on Computers. – 1999. – Vol. 48, N 5. – P. 506–521.
  2. Семенов А. А., Заикин О. С. Алгоритмы построения декомпозиционных множеств для крупноблочного распараллеливания SAT-задач. Серия «Математика» 2012. Т. 5, No 4. С. 79—94