2SAT:Решение

Материал из CustisWiki

Идея

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

Теперь заметим, что формула эквивалентна формуле . Последней формуле, легко придать интерпретацию на графе: для 2SAT-формулы, содержащей n переменных , сопоставим ориентированный граф из 2n узлов: , а для каждой дизъюнкции он будет содержать два ребра и . В разрешимой формуле, истинность терма означает истинность всех термов достижимых (в смысле путей в ориентированном графе) в графе из узла, соответствующему терму .

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

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

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

Представление 2SAT на графе

---

Репликация: База Знаний «Заказных Информ Систем» → «2SAT:Решение»

Любые правки этой статьи будут перезаписаны при следующем сеансе репликации. Если у вас есть серьезное замечание по тексту статьи, запишите его в раздел «discussion».