2SAT:Решение - История изменений

StasFomin: Содержимое страницы заменено на «#REDIRECT discopal:{{PAGENAME}}»

2011-06-13T17:46:28Z

Содержимое страницы заменено на «#REDIRECT [[discopal:{{PAGENAME}}]]»

Внесённые изменения

WikiSysop: 1 версия

2008-08-04T09:55:46Z

1 версия

BenderBot: реплицировано из внутренней CustisWiki

2007-01-16T04:49:23Z

реплицировано из внутренней CustisWiki

Внесённые изменения

StasFomin: math->m

2007-01-15T17:37:04Z

math->m

BenderBot: реплицировано из внутренней CustisWiki

2005-12-08T04:39:02Z

реплицировано из внутренней CustisWiki

← Предыдущая	Версия 09:55, 4 августа 2008
(не показана 1 промежуточная версия 1 участника)
(нет различий)

@@ Строка 2: / Строка 2: @@
 Рассмотрим входную [[2SAT]]-формулу.
-Во-первых, ясно, что можно быстро исключить все дизъюнкции, состоящие из одного терма — если это дизъюнкция типа <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».
 Поиск путей в графе выполняется за полиномиальное время, таким образом, задача полиномиально разрешима.

@@ Строка 2: / Строка 2: @@
 Рассмотрим входную [[2SAT]]-формулу.
-Во-первых, ясно, что можно быстро исключить все дизъюнкции, состоящие из одного терма — если это дизъюнкция типа <m>x_i</m>, то для выполнимости формулы необходимо <m>x_i=1</m>, соответственно мы фиксируем <m>x_i \equiv 1</m> и автоматически исключаются все дизъюнкты, куда эта переменная входит в положительной степени, т.к. их выполнимость гарантирована. Если есть дизъюнкт, куда такая переменная входит в отрицательной степени - формула неразрешима. Аналогично (с точностью до наоборот) избавляемся от переменных, "засветившихся" в дизъюнкции <m>(\neg x_i)</m>. Если после редукции, неразрешимость формулы еще не проявилась, у нас остается формула, состоящая из дизъюнктов включающих ровно два терма.
+Во-первых, ясно, что можно быстро исключить все дизъюнкции, состоящие из одного терма — если это дизъюнкция типа <math>x_i</math>, то для выполнимости формулы необходимо <math>x_i=1</math>, соответственно мы фиксируем <math>x_i \equiv 1</math> и автоматически исключаются все дизъюнкты, куда эта переменная входит в положительной степени, т.к. их выполнимость гарантирована. Если есть дизъюнкт, куда такая переменная входит в отрицательной степени - формула неразрешима. Аналогично (с точностью до наоборот) избавляемся от переменных, "засветившихся" в дизъюнкции <math>(\neg x_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 \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 \Rightarrow y</m> существование пути из узла ''x'' в узел ''y''. Тогда
+Обозначим через <math>x \Rightarrow y</math> существование пути из узла ''x'' в узел ''y''. Тогда
-если для некоторого <m>x_i</m> будет существовать пути
+если для некоторого <math>x_i</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>, «нарушается» второй путь.
+<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>, «нарушается» второй путь.
 В противном случае, покажем, как сделать выполняющее присваивание.
-Для каждой переменной ''x'', если есть путь <m>x \Rightarrow \neg x</m>, то присваиваем ей «0», в противном случае «1».
+Для каждой переменной ''x'', если есть путь <math>x \Rightarrow \neg x</math>, то присваиваем ей «0», в противном случае «1».
 Поиск путей в графе выполняется за полиномиальное время, таким образом, задача полиномиально разрешима.