Теорема Кука – Левина или теорема Кука
В теории вычислительной сложности теорема Кука-Левина, также известная как теорема Кука, утверждает, что проблема булевой выполнимости является NP-полной. То есть она находится в NP, а любая проблема в NP может быть сведена за полиномиальное время с помощью детерминированной машины Тьюринга к булевой проблеме выполнимости.
Стивен Артур Кук и Л. А. Левин в 1973 году независимо друг от друга доказали, что проблема выполнимости (SAT) является NP-полной. Стивен Кук в 1971 году опубликовал важную статью под названием «Сложность процедур доказательства теорем», в которой он описал способ получения доказательства NP-полной задачи путем сведения ее к SAT . Он доказал, что задачи Circuit-SAT и 3CNF-SAT не менее сложны, чем SAT . Точно так же Леонид Левин самостоятельно работал над этой проблемой в тогдашнем Советском Союзе. Доказательство того, что SAT является NP-полным, было получено благодаря усилиям этих двух ученых. Позже Карп свел 21 задачу оптимизации, такую как гамильтонов тур, вершинное покрытие и клика, к SAT и доказал, что эти задачи являются NP-полными.
Следовательно, SAT представляет собой серьезную проблему, и ее можно сформулировать следующим образом:
Если задано логическое выражение F , имеющее n переменных x 1 ,x 2 ,….,x n и логические операторы, возможно ли иметь присваивание переменных true или false таким образом, чтобы бинарное выражение F было истинным?
Эта задача также известна как формула — SAT . SAT (формула-SAT или просто SAT) принимает логическое выражение F и проверяет, является ли данное выражение (или формула) выполнимым. Говорят, что логическое выражение удовлетворяет некоторым допустимым присваиваниям переменных, если оценка оказывается истинной. Прежде чем обсуждать детали SAT, давайте теперь обсудим некоторые важные термины булевых выражений.
- Логическая переменная: переменная, скажем x , которая может иметь только два значения, true или false, называется логической переменной.
- Литерал : литерал может быть логической переменной, скажем, x или ее отрицанием, то есть x или x̄ ; x называется положительным литералом, а x̄ называется отрицательным литералом
- Предложение: Последовательность переменных (x 1 ,x 2 ,….,x n ) , которые могут быть разделены логическим оператором ИЛИ , называется предложением. Например, (x 1 V x 2 V x 3 ) — это предложение из трех литералов.
- Выражения: можно объединить все предыдущие предложения, используя логический оператор, чтобы сформировать выражение.
- Форма CNF: выражение находится в форме CNF (конъюнктивная нормальная форма), если набор предложений разделен оператором AND (^) , а литералы связаны оператором OR (v) . Ниже приведен пример выражения в форме CNF:
- f = (x 1 V x̄ 2 V x 3) ∧ (x 1 V x̄ 3 V x 2 )
- 3 — CNF: говорят, что выражение находится в 3-CNF, если оно находится в конъюнктивной нормальной форме, и каждое предложение имеет ровно три литерала.
Таким образом, SAT является одной из самых сложных задач, поскольку не существует другого известного алгоритма, кроме подхода грубой силы. Алгоритм грубой силы будет алгоритмом с экспоненциальным временем, так как 2 n необходимо попробовать возможные присваивания, чтобы проверить, является ли данное логическое выражение истинным или нет. Стивен Кук и Леонид Левин доказали, что SAT является NP-полным.
Кук продемонстрировал сведение других сложных задач к SAT. Карп представил доказательство 21 важной проблемы, такой как гамильтонов тур, вершинное покрытие и клика, сведя ее к SAT с помощью редукции Карпа.
Кратко представим три типа SAT. Они следующие:
- Circuit-SAT: Circuit-SAT можно сформулировать следующим образом: для заданной логической схемы, которая представляет собой набор вентилей, таких как И , ИЛИ , НЕ и n входов, есть ли какие-либо входные назначения логических переменных, чтобы выход данной схемы верно? Опять же, сложность с этими задачами заключается в том, что для n входов в схему. 2 н возможные выходы должны быть проверены. Следовательно, этот алгоритм грубой силы является экспоненциальным алгоритмом, и, следовательно, это сложная задача.
- CNF-SAT: эта проблема является ограниченной проблемой SAT , где выражение должно быть в конъюнктивной нормальной форме. Говорят, что выражение находится в форме конъюнкции, если все предложения связаны логическим оператором И. Как и в случае с SAT , речь идет о присвоении значений истинности n переменным таким образом, чтобы вывод выражения был истинным .
- 3-CNF-SAT(3-SAT): эта проблема является еще одним вариантом, где дополнительным ограничением является то, что выражение находится в конъюнктивной нормальной форме и что каждое предложение должно содержать ровно три литерала. Эта проблема также связана с присвоением n значений истинности n переменным логического выражения таким образом, чтобы вывод выражения был истинным. Проще говоря, по заданному выражению в 3-CNF задача 3-SAT состоит в том, чтобы проверить, является ли данное выражение выполнимым.
Эти задачи можно использовать для доказательства NP-полноты некоторых важных задач.