!SAT

Определение

Задачи типа SAT (от англ. satisfaction) - это задачи на поиск набора аргументов, удволетворяющих заданной булевой функции, записанной в КНФ. Отдельные ее вариации, в которых в каждом клозе ровно $n$ переменных имеют свое название $n-SAT$. Стандартная запись: $(x_{11}\cup x_{12}\cup \dots x_{1k_1})\cap (x_{21}\cup x_{22}\cup \dots x_{2k_2})\cap \cdots \cap (x_{n1}\cup x_{n2}\cup \dots x_{n{k}_n})$

2-SAT

Описание

Самая популярная разновидность задачи SAT, иначе называемая КФН в форме Крона. Имеет полиномиальное решение за $O(n+m)$ по времени, где n - кол-во задаваемых аргументов функции, а m - кол-во клозов в записи.

Алгоритм

Заметим, что $(x_{11}\cup x_{12})⟺(\overline{x_{11}}\to x_{12})\cap (\overline{x_{12}}\to x_{11})$. Тогда давайте сделаем замену всех клозов, используя это преобразование и построим на этом ориентированный граф создавая ребро из u в v, если существут клоз $(u\to v)$ в нашей формуле. Тогда поймем, что наша задача свелась к тому, что мы хотим расставить 0 и 1 в графе так, что у нас нет стрелки из 1 в 0, а также $x_i\ne \overline{x_i}$. Утверждение. $\forall x_1,x_2\in C:x_1=x_2$, где $C$ - какой-то цикл в полученном графе. Доказательство. Предположим нашлись $x_1$ и $x_2$ разные по значению, лежащие в одном цикле. Тогда не умаляя общности $x_1$ равен 1, пойдем от него дальше по циклу. Так как стрелка ведет из 1, то она ведет в 1, значит элемент в цикле за $x_1$ тоже 1. Будем продолжать по нему идти, пока не дойдем до $x_0$, он должын быть и 0 и 1, противоречие. Значит не бывает двух переменных, имеющих разные значения и лежащих в одном цикле. Заметим, что раз у нас каждый элемент в цикле равен либо 0, либо 1, мы можем сжать все циклы в вершины. Алгоритм, делающий это с асимптотикой $O(n)$ уже существует, он называется конденсация графа, воспользуемся им. Единственное изменение которое нам нужно сделать, это отследить, что в одном цикле не оказалась вершина и ее отрицание. В таких случаях решения нет. В остальных случаях у нас есть DAG, для которого мы хотим решать аналогичную задачу. Давайте сделаем topsort этого графа и теперь расставим значения 0 и 1 соответственно следующему правило. Правило. Если в получившемся отсортированном массиве $x_i$ имеет номер, меньший номера $\overline{x_i}$, то $x_i=0$, иначе $x_i=1$. Доказательство работы. Разберемся, что может пойти не так. Так как у нас DAG, то у нас нет пути из $x_i$ в $\overline{x_i}$ напрямую, значит это сломаться не могло. Также из