1 files changed, 124 insertions, 0 deletions
diff --git a/reports/lab5/lab5.tex b/reports/lab5/lab5.tex
new file mode 100644
index 0000000..5da74b6
--- /dev/null
+++ b/reports/lab5/lab5.tex
@@ -0,0 +1,124 @@
+\documentclass[spec, och, labwork]{SCWorks}
+\usepackage{preamble}
+
+\begin{document}
+\include{titlepage.tex}
+
+В лабораторной работе №4 было продемонстрировано, что задача NP-полноты языка,
+состоящего из булевых функций, не являющихся тавтологиями является NP-полной.
+Таким образом, её невозможно решить за полиномиальное время и следует
+использовать некоторое приближенное решение.
+
+Такой приближённой задачей является задача 2-ВЫП или 2-КНФ, которая может быть
+решена за полиномиальное время.
+
+Сначала приведём задачу к другой форме - так называемой импликативной форме.
+Заметим, что выражение вида $a \lor b$ эквивалентно $\neg a \implies b$ или
+$\neg b \implies a$. Это можно воспринимать следующим образом: если есть
+выражение $a \lor b$, и нам необходимо добиться обращения его в $true$, то, если
+$a = false$, то необходимо $b = true$, и наоборот, если $b = false$, то
+необходимо $a = true$.
+
+Построим теперь так называемый граф импликаций: для каждой переменной в графе
+будет по две вершины, обозначим их через $x_i$ и $\neg x_i$. Рёбра в графе будут
+соответствовать импликативным связям.
+
+Например, для 2-КНФ формы:
+\begin{equation*}
+    (a \lor b) \land (b \lor \neg c)
+\end{equation*}
+
+Граф импликаций будет содержать следующие рёбра (ориентированные):
+\begin{align*}
+    \neg a &\implies b \\
+    \neg b &\implies a \\
+    \neg b &\implies \neg c \\
+    c &\implies b
+\end{align*}
+
+Стоит обратить внимание на такое свойство графа импликаций, что если есть ребро
+$a \implies b$, то есть и ребро $\neg b \implies \neg a$.
+
+Теперь заметим, что если для какой-то переменной $x$ выполняется, что из $x$
+достижимо $\neg x$, а из $\neg x$ достижимо $x$, то задача решения не имеет.
+Действительно, какое бы значение для переменной $x$ мы бы ни выбрали, мы всегда
+придём к противоречию - что должно быть выбрано и обратное ему значение.
+Оказывается, что это условие является не только достаточным, но и необходимым
+(доказательством этого факта будет описанный ниже алгоритм). Переформулируем
+данный критерий в терминах теории графов. Напомним, что если из одной вершины
+достижима другая, а из той вершины достижима первая, то эти две вершины
+находятся в одной сильно связной компоненте. Тогда мы можем сформулировать
+критерий существования решения следующим образом:
+
+Для того, чтобы данная задача 2-ВЫП имела решение, необходимо и достаточно,
+чтобы для любой переменной $x$ вершины $x$ и $\neg x$ находились в разных
+компонентах сильной связности графа импликаций.
+
+Этот критерий можно проверить за время $O(N + M)$ с помощью алгоритма поиска
+сильно связных компонент.
+
+Теперь построим собственно алгоритм нахождения решения задачи 2-ВЫП в
+предположении, что решение существует.
+
+Заметим, что, несмотря на то, что решение существует, для некоторых переменных
+может выполняться, что из $x$ достижимо $\neg x$, или (но не одновременно), из
+$\neg x$ достижимо $x$. В таком случае выбор одного из значений переменной $x$
+будет приводить к противоречию, в то время как выбор другого - не будет.
+Научимся выбирать из двух значений то, которое не приводит к возникновению
+противоречий. Сразу заметим, что, выбрав какое-либо значение, мы должны
+запустить из него обход в глубину/ширину и пометить все значения, которые
+следуют из него, т.е. достижимы в графе импликаций. Соответственно, для уже
+помеченных вершин никакого выбора между $x$ и $\neg x$ делать не нужно, для них
+значение уже выбрано и зафиксировано. Нижеописанное правило применяется только к
+непомеченным ещё вершинам.
+
+Утверждается следующее. Пусть $comp[v]$ обозначает номер компоненты сильной
+связности, которой принадлежит вершина $v$, причём номера упорядочены в порядке
+топологической сортировки компонент сильной связности в графе компонентов (т.е.
+более ранним в порядке топологической сортировки соответствуют большие номера:
+если есть путь из $v$ в $w$, то $comp[v] \leq comp[w]$). Тогда, если $comp[x] <
+comp[\neg x]$, то выбираем значение $\neg x$, иначе, т.е. если $comp[x] >
+comp[\neg x]$, то выбираем $x$.
+
+Докажем, что при таком выборе значений мы не придём к противоречию. Пусть, для
+определённости, выбрана вершина $x$ (случай, когда выбрана вершина $\neg x$,
+доказывается симметрично).
+
+Во-первых, докажем, что из $x$ не достижимо $\neg x$. Действительно, так как
+номер компоненты сильной связности $comp[x]$ больше номера компоненты $comp[\neg
+x]$, то это означает, что компонента связности, содержащая $x$, расположена
+левее компоненты связности, содержащей $\neg x$, и из первой никак не может быть
+достижима последняя.
+
+Во-вторых, докажем, что никакая вершина $y$, достижимая из $x$, не является
+<<плохой>>, т.е. неверно, что из $y$ достижимо $\neg y$. Докажем это от
+противного. Пусть из $x$ достижимо $y$, а из $y$ достижимо $\neg y$. Так как из
+$x$ достижимо $y$, то, по свойству графа импликаций, из $\neg y$ будет достижимо
+$\neg x$. Но, по предположению, из $y$ достижимо $\neg y$. Тогда мы получаем,
+что из $x$ достижимо $\neg x$, что противоречит условию, что и требовалось
+доказать.
+
+Итак, мы построили алгоритм, который находит искомые значения переменных в
+предположении, что для любой переменной $x$ вершины $x$ и $\neg x$ находятся в
+разных компонентах сильной связности. Выше показали корректность этого
+алгоритма. Следовательно, мы одновременно доказали указанный выше критерий
+существования решения.
+
+Теперь мы можем собрать весь алгоритм воедино:
+\begin{itemize}
+    \item
+        Построим граф импликаций.
+    \item
+        Найдём в этом графе компоненты сильной связности за время O (N + M),
+        пусть $comp[v]$ "--- это номер компоненты сильной связности, которой
+        принадлежит вершина $v$.
+    \item
+        Проверим, что для каждой переменной $x$ вершины $x$ и $\neg x$ лежат в
+        разных компонентах, т.е. $comp[x] \neq comp[\neg x]$. Если это условие
+        не выполняется, то вернуть "решение не существует".
+    \item
+        Если $comp[x] > comp[\neg x]$, то переменной $x$ выбираем значение
+        $true$, иначе "--- $false$.
+\end{itemize}
+
+\end{document}