Задача выполнимости булевых формул | это... Что такое Задача выполнимости булевых формул? (original) (raw)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

См. также

Ссылки

2.5-ВЫПОЛНИМОСТЬ (вопросы сведения 3-SAT к 2-SAT)
The international SAT Competitions web page
SATLIB - The Satisfiability Library
Sat Live - общий сайт о SAT.

Примечания

NP-полные задачи
Математика
Исследование операций:Оптимизация:Комбинаторная оптимизация
Максимизационная задача укладки (упаковки)	Упаковка в контейнеры (двумерная упаковка • линейная упаковка • упаковка по весу • упаковка по стоимости) • Задача о ранце (рюкзаке)
Теория графов теория множеств	Задача о вершинном покрытии • Задача о клике • Задача о независимом множестве (наборе) • Задача о покрытии множества • Задача Штейнера • Задача коммивояжёра • Обобщённая задача коммивояжёра
Алгоритмические задачи	Задача выполнимости булевых формул (в конъюнктивной нормальной форме)
Логические игры и головоломки	Обобщённые пятнашки с костяшками >15) (задача поиска кратчайшего решения) • Задачи, решения которых применяются в Тетрис • Задача обобщённого судоку • Задача о заполнении латинского квадрата • Задача какуро
См. также	Прикладная математика • Теория алгоритмов • Динамическое программирование • 21 NP-полная задача Карпа
Классы сложности