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