�� 2-SAT

�� 2-SAT (2-satisfiability) - �� , �� .

�� 2-SAT �� , �� ; �� 2-CNF (2-conjunctive normal form). ��:

(a || c) && (a || !d) && (b || !d) && (b || !e) && (c || d)

��

�� 2-SAT �� , �� , �� 2 �� , � �� :

�� .
�� , �� .
�� , �� , �� , �� general satisfiability, �� NP-��. ��, �� , �� 2-SAT.
�� .
�� , �� , �� 2-SAT.
�� .
�� , �� , � �� -��, � �� .
� �.�.

��

�� - �� . ��, �� a || b �� !a => b �� !b => a. �� : �� a || b, � �� true, ��, �� a=false, �� b=true, � ��, �� b=false, �� a=true.

�� �� : �� , �� x_i � !x_i. и�� .

��, �� 2-CNF ��:

(a || b) && (b || !c)

�� (��):

!a => b
!b => a
!b => !c
c => b

�� , �� a => b, �� !b => !a.

�� , �� -�� x ��, �� x �� !x, � �� !x �� x, �� . ��, �� x �� , �� - �� . ��, �� , �� (�� ). �� . ��, �� , � �� , �� . �� ��  �� :

�� , �� 2-SAT �� , �� , �� x �� x � !x �� � ��  �� .

�� O (N + M) � �� .

�� �� �� 2-SAT � ��, �� .

��, ��, �� , �� , �� , �� x �� !x, �� (�� ), �� !x �� x. � �� x �� , � �� - �� . �� , �� . �� , ��, �� -�� , �� /�� , �� , �.�. �� . ��, �� x � !x �� , �� . �� .

�� ��. �� comp[v] �� , �� v, �� (�.�. �� : �� v � w, �� comp[v] <= comp[w]). ��, �� comp[x] < comp[!x], �� !x, ��, �.�. �� comp[x] > comp[!x], �� x.

��, �� . ��, �� , �� x (��, �� !x, �� ).

��-��, ��, �� x �� !x. ��, �� comp[x] �� comp[!x], �� , �� , �� x, �� , �� !x, � �� .

��-��, ��, �� y, �� x, �� "��", �.�. ��, �� y �� !y. �� . �� x �� y, � �� y �� !y. �� x �� y, ��, �� , �� !y �� !x. ��, �� , �� y �� !y. �� , �� x �� !x, �� , �� .

��, �� , �� , �� x �� x � !x �� . �� . ��, �� .

�� ��  ��:

�� .
�� O (N + M), �� comp[v] - �� , �� v.
��, �� x �� x � !x �� , �.�. comp[x] ≠ comp[!x]. �� , �� "�� ".
�� comp[x] > comp[!x], �� x �� true, �� - false.

��

�� 2-SAT �� g � �� gt (�.�. � �� ).

�� , �� "NO SOLUTION", �� .

int n;
vector < vector<int> > g, gt;
vector<bool> used;
vector<int> order, comp;

void dfs1 (int v) {
	used[v] = true;
	for (size_t i=0; i<g[v].size(); ++i) {
		int to = g[v][i];
		if (!used[to])
			dfs1 (to);
	}
	order.push_back (v);
}

void dfs2 (int v, int cl) {
	comp[v] = cl;
	for (size_t i=0; i<gt[v].size(); ++i) {
		int to = gt[v][i];
		if (comp[to] == -1)
			dfs2 (to, cl);
	}
}

int main() {
	... ������ n, ����� g, ���������� ����� gt ...

	used.assign (n, false);
	for (int i=0; i<n; ++i)
		if (!used[i])
			dfs1 (i);

	comp.assign (n, -1);
	for (int i=0, j=0; i<n; ++i) {
		int v = order[n-i-1];
		if (comp[v] == -1)
			dfs2 (v, j++);
	}

	for (int i=0; i<n; ++i)
		if (comp[i] == comp[i^1]) {
			puts ("NO SOLUTION");
			return 0;
		}
	for (int i=0; i<n; ++i) {
		int ans = comp[i] > comp[i^1] ? i : i^1;
		printf ("%d ", ans);
	}

}

������ 2-SAT

����������

��������

����������

�� 2-SAT

��

��

��