Текст: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.Список авторов доступен на этом ресурсе в статье под тем же названием.