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

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

Идея[править]

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

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

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

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

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

Представление 2SAT на графе[править]


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

Представление — метафора