Текст:2SAT:Решение

From Традиция
(Redirected from 2SAT:Решение)
Jump to navigation Jump to search

Идея[edit | edit source]

Рассмотрим входную 2SAT-формулу. Во-первых, ясно, что можно быстро исключить все дизъюнкции, состоящие из одного терма — если это дизъюнкция типа x i x_i , то для выполнимости формулы необходимо x i = 1 x_i=1 , соответственно мы фиксируем x i 1 x_i \equiv 1 и автоматически исключаются все дизъюнкты, куда эта переменная входит в положительной степени, т.к. их выполнимость гарантирована. Если есть дизъюнкт, куда такая переменная входит в отрицательной степени - формула неразрешима. Аналогично (с точностью до наоборот) избавляемся от переменных, "засветившихся" в дизъюнкции ( ¬ x i ) (\neg x_i) . Если после редукции, неразрешимость формулы еще не проявилась, у нас остается формула, состоящая из дизъюнктов включающих ровно два терма.

Теперь заметим, что формула x y x \lor y эквивалентна формуле ( ¬ x y ) ( ¬ y x ) (\neg x \rightarrow y) \land (\neg y \rightarrow x) . Последней формуле, легко придать интерпретацию на графе: для 2SAT-формулы, содержащей n переменных x i x_i , сопоставим ориентированный граф из 2n узлов: i   x i ,   ¬ x i \forall i\ x_i,\ \neg x_i , а для каждой дизъюнкции ( x y ) (x \lor y) он будет содержать два ребра ( ¬ x y ) (\neg x \rightarrow y) и ( ¬ y x ) (\neg y \rightarrow x) . В разрешимой формуле, истинность терма x i σ i x^{\sigma_i}_i означает истинность всех термов x j σ j x^{\sigma_j}_j достижимых (в смысле путей в ориентированном графе) в графе из узла, соответствующему терму x i σ i x^{\sigma_i}_i .

Обозначим через x y x \Rightarrow y существование пути из узла x в узел y. Тогда если для некоторого x i x_i будет существовать пути x i ¬ x i x_i \Rightarrow \neg x_i и ¬ x i x i \neg x_i \Rightarrow x_i , то формула будет неразрешима. Действительно, при x i = 1 x_i=1 , "нарушается" первый путь, а при x i = 0 x_i=0 , «нарушается» второй путь.

В противном случае, покажем, как сделать выполняющее присваивание. Для каждой переменной x, если есть путь x ¬ x x \Rightarrow \neg x , то присваиваем ей «0», в противном случае «1».

Поиск путей в графе выполняется за полиномиальное время, таким образом, задача полиномиально разрешима.

Представление 2SAT на графе[edit | edit source]


По крайней мере часть этого текста взята с ресурса http://lib.custis.ru/ под лицензией GDFL.Список авторов доступен на этом ресурсе в статье под тем же названием.