Семинар 5.

1.	Пусть у нас есть выражение в 2-CNF форме. Это значит, что выражение задано
	в виде конъюнкции дизъюнкций, каждая из которых содержит ровно два литерала.
	Задача SAT-2 состоит в нахождении такого набора значений булевых переменных,
	что значение всего выражения становится истиной. Для начала, приведём задачу
	к импликативной форме. Дизъюнкция (a ⋁ b) эквивалентна любой из импликаций:
	(¬a ⇒ b) и (¬b ⇒ a).

2.	Мы можем построить граф, соответствующий заданному выражению: вершинами графа
	будут все переменные выражения, а так же их отрицания. Каждой импликации будет
	соответствовать ребро. Таким образом, по выражению, содержащему n переменных и
	состоящему из k 2-дизъюнкций, мы построим орграф, содержащий 2n вершин и 2k
	рёбер. Граф этот будет кососимметричным: транспонированный граф изоморфен
	исходному, причём при таком изоморфизме вершины перейдут в свои логические
	дополнения. Другими словами, если есть ребро из a в b, то есть и ребро из
	¬b в ¬a.

3.	Предположим, что нам удалось назначить переменным такие значения, что они
	удовлетворяют требованиям задачи SAT-2. Заметим тогда, что если в этом графе
	есть путь из вершины a в вершину b, то из a следует b. Это означает, что
	в любом пути нашего графа сначала идёт какое-то (возможно нулевое) число
	значений "ложь", а оставшийся путь целиком состоит из значений "истина".
	Отсюда следует, что в цикле все значения одинаковы. Другими словами, все
	переменные лежащие в одной компоненте сильной связности принимают одно и
	то же значение. Откуда сразу следует необходимое условие решаемости задачи
	SAT-2: любая переменная должна лежать в компоненте отличной от той, в которой
	лежит её отрицание. Оказывается, это условие является и достаточным.

4.	Итак, ясно, что для успешного решения задачи, нужно назначать значения целиком
	компонентам связности. Это даёт нам моральное право перейти от исходного графа
	к его конденсации. Заметим, что конденсация также будет кососимметричной.
	Так как конденсация не содержит циклов, то мы можем перебирать вершины в
	топологическом порядке, каждой следующей вершине, которой ещё не присвоено
	значение, мы присваиваем значение "ложь", а её дополнению — значение "истина".
	(Или можно идти с конца и тогда присваивать новым вершинам значение "истина".)
	Таким образом у нас ни на каком пути не будет перехода "истина ⇒ ложь".
	Действительно, пусть у нас есть такой переход: a ⇒ b, это значит, что ¬a идёт
	раньше a по топологическому порядку (так работает алгоритм), b идёт раньше ¬b,
	a идёт раньше b (иначе не существовало бы ребра a ⇒ b), а ¬b идёт раньше ¬a
	(существование ребра ¬b ⇒ ¬a следует из кососимметричности графа). Полученное
	противоречие доказывает утверждение, а вместе с ним и то, что алгоритм строит
	правильное решение задачи SAT-2.

5.	Стоит заметить, что предложенный алгоритм, конечно, следует имплементировать
	так, чтобы он работал за один проход. Для этого берётся тот же самый алгоритм
	Тарьяна для нахождения компонент сильной связности, и в момент, когда из стека
	вынимается очередная непомеченная компонента, входящим в её состав вершинам
	приписывается значение "истина", а их дополнениям — "ложь".