2SAT:Решение — различия между версиями
BenderBot (обсуждение | вклад) м (реплицировано из внутренней CustisWiki) |
StasFomin (обсуждение | вклад) м (math->m) |
||
Строка 2: | Строка 2: | ||
Рассмотрим входную [[2SAT]]-формулу. | Рассмотрим входную [[2SAT]]-формулу. | ||
− | Во-первых, ясно, что можно быстро исключить все дизъюнкции, состоящие из одного терма — если это дизъюнкция типа < | + | Во-первых, ясно, что можно быстро исключить все дизъюнкции, состоящие из одного терма — если это дизъюнкция типа <m>x_i</m>, то для выполнимости формулы необходимо <m>x_i=1</m>, соответственно мы фиксируем <m>x_i \equiv 1</m> и автоматически исключаются все дизъюнкты, куда эта переменная входит в положительной степени, т.к. их выполнимость гарантирована. Если есть дизъюнкт, куда такая переменная входит в отрицательной степени - формула неразрешима. Аналогично (с точностью до наоборот) избавляемся от переменных, "засветившихся" в дизъюнкции <m>(\neg x_i)</m>. Если после редукции, неразрешимость формулы еще не проявилась, у нас остается формула, состоящая из дизъюнктов включающих ровно два терма. |
− | Теперь заметим, что формула < | + | Теперь заметим, что формула <m>x \lor y</m> эквивалентна формуле <m>(\neg x \rightarrow y) \land (\neg y \rightarrow x)</m>. Последней формуле, легко придать интерпретацию на графе: для [[2SAT]]-формулы, содержащей ''n'' переменных <m>x_i</m>, сопоставим ориентированный граф из ''2n'' узлов: <m>\forall i\ x_i,\ \neg x_i</m>, а для каждой дизъюнкции <m>(x \lor y)</m> он будет содержать два ребра <m>(\neg x \rightarrow y)</m> и <m>(\neg y \rightarrow x)</m>. В разрешимой формуле, истинность терма <m>x^{\sigma_i}_i</m> означает истинность всех термов <m>x^{\sigma_j}_j</m> достижимых (в смысле путей в ориентированном графе) в графе из узла, соответствующему терму <m>x^{\sigma_i}_i</m>. |
− | Обозначим через < | + | Обозначим через <m>x \Rightarrow y</m> существование пути из узла ''x'' в узел ''y''. Тогда |
− | если для некоторого < | + | если для некоторого <m>x_i</m> будет существовать пути |
− | < | + | <m>x_i \Rightarrow \neg x_i</m> и <m>\neg x_i \Rightarrow x_i</m>, то формула будет неразрешима. Действительно, при <m>x_i=1</m>, "нарушается" первый путь, а при <m>x_i=0</m>, «нарушается» второй путь. |
В противном случае, покажем, как сделать выполняющее присваивание. | В противном случае, покажем, как сделать выполняющее присваивание. | ||
− | Для каждой переменной ''x'', если есть путь < | + | Для каждой переменной ''x'', если есть путь <m>x \Rightarrow \neg x</m>, то присваиваем ей «0», в противном случае «1». |
Поиск путей в графе выполняется за полиномиальное время, таким образом, задача полиномиально разрешима. | Поиск путей в графе выполняется за полиномиальное время, таким образом, задача полиномиально разрешима. |
Версия 20:37, 15 января 2007
Идея
Рассмотрим входную 2SAT-формулу. Во-первых, ясно, что можно быстро исключить все дизъюнкции, состоящие из одного терма — если это дизъюнкция типа , то для выполнимости формулы необходимо , соответственно мы фиксируем и автоматически исключаются все дизъюнкты, куда эта переменная входит в положительной степени, т.к. их выполнимость гарантирована. Если есть дизъюнкт, куда такая переменная входит в отрицательной степени - формула неразрешима. Аналогично (с точностью до наоборот) избавляемся от переменных, "засветившихся" в дизъюнкции . Если после редукции, неразрешимость формулы еще не проявилась, у нас остается формула, состоящая из дизъюнктов включающих ровно два терма.
Теперь заметим, что формула эквивалентна формуле . Последней формуле, легко придать интерпретацию на графе: для 2SAT-формулы, содержащей n переменных , сопоставим ориентированный граф из 2n узлов: , а для каждой дизъюнкции он будет содержать два ребра и . В разрешимой формуле, истинность терма означает истинность всех термов достижимых (в смысле путей в ориентированном графе) в графе из узла, соответствующему терму .
Обозначим через существование пути из узла x в узел y. Тогда если для некоторого будет существовать пути и , то формула будет неразрешима. Действительно, при , "нарушается" первый путь, а при , «нарушается» второй путь.
В противном случае, покажем, как сделать выполняющее присваивание. Для каждой переменной x, если есть путь , то присваиваем ей «0», в противном случае «1».
Поиск путей в графе выполняется за полиномиальное время, таким образом, задача полиномиально разрешима.
Представление 2SAT на графе
Любые правки этой статьи будут перезаписаны при следующем сеансе репликации. Если у вас есть серьезное замечание по тексту статьи, запишите его в раздел «discussion».
Репликация: База Знаний «Заказных Информ Систем» → «2SAT:Решение»