2-ВЫПОЛНИМОСТЬ (2-SAT) — задача выполнимости КНФ, каждая скобка которой содержит не более двух литералов. В отличие от общего SAT и 3-SAT, задача 2-SAT принадлежит классу
В курсе полиномиальность доказывается последовательным исключением переменных. Формула преобразуется в равновыполнимую 2-КНФ с на одну переменную меньше. После не более чем \(n-1\) исключений остаётся формула от одной переменной. Для выбранного кодирования весь алгоритм реализуется детерминированной МТ за \(O(L^5)\)
Что важно запомнить
- 2-КНФ — конъюнкция скобок длины не более двух литералов.
- Теорема курса: \(2\text{-SAT}\in P\)
- Если имеется единичная скобка с литералом \(\ell\), соответствующую переменную фиксируют так, чтобы \(\ell=1\), и упрощают формулу.
- Если единичных скобок нет, для выбранной переменной \(x\) объединяют условия \((\neg x\vee y_i)\) и \((x\vee z_j)\) в скобки \((y_i\vee z_j)\), исключая \(x\).
- Каждый шаг сохраняет выполнимость и уменьшает число переменных. Общая оценка в доказательстве — \(O(L^5)\).
Постановка 2-SAT
В 2-КНФ каждый сомножитель имеет вид \((a)\) или \((a\vee b)\), где \(a,b\) — литералы. Нужно определить, существует ли набор значений, обращающий все скобки в 1.
Исключение единичного литерала
Если формула содержит единичный множитель \(\ell\), соответствующую переменную фиксируют так, чтобы \(\ell=1\). В доказательстве случай записан как \(\ell=x\): тогда полагают \(x=1\), удаляют уже выполненные скобки и упрощают скобки с \(\neg x\). Для литерала \(\neg x\) действует симметричное правило с \(x=0\). Если после упрощения возникает противоречие, формула
Исключение переменной из двухбуквенных скобок
Если единичных скобок нет, выберем переменную \(x\). Пусть \(K_0\) состоит из скобок \((\neg x\vee y_i)\), \(K_1\) — из скобок \((x\vee z_j)\), а \(K_2\) не зависит от \(x\). Тогда существование подходящего значения \(x\) эквивалентно выполнению всех резольвент
\((y_i\vee z_j)\)
вместе с \(K_2\). Полученная КНФ не содержит \(x\) и остаётся
Полиномиальная оценка
После каждого шага число переменных уменьшается. Не более чем за \(n-1\) исключений задача сводится к формуле от одной переменной, которую легко проверить непосредственно. Подробный анализ кодирования в пособии даёт детерминированную оценку \(O(L^5)\). Поэтому
Оценка \(O(L^5)\) здесь нужна как конструктивная полиномиальная верхняя граница для доказательства принадлежности \(P\). Она не утверждается как оптимальная трудоёмкость 2-SAT.
Пример простыми словами
Рассмотрим скобки \((\neg x\vee y)\) и \((x\vee z)\). Если существует значение \(x\), удовлетворяющее обеим скобкам при фиксированных \(y,z\), то обязательно истинна \(y\vee z\). И наоборот, если \(y\vee z=1\), можно выбрать подходящее значение \(x\). Поэтому пару условий можно заменить резольвентой \((y\vee z)\) и исключить \(x\).
Частые ошибки
- Делать вывод, что 2-SAT полиномиальна только потому, что в каждой скобке два литерала. Нужен алгоритм и оценка его трудоёмкости.
- При исключении \(x\) просто удалять все скобки с \(x\) и \(\neg x\). Нужно добавить резольвенты, сохраняющие условия совместной выполнимости.
- Переносить этот результат на 3-SAT. Добавление третьего литерала принципиально меняет сложность: 3-SAT является NP-полной задачей.
