Boj 11281) 2 Sat 4

문제

백준 11281

설명

2-SAT 란?

2-SAT 문제는 a->b 꼴의 여러 단순조건명제들을 and 로 묶은 복합명제가 참이 될 수 있는지, 만약 그렇다면 단순명제들의 진리값을 어떻게 했을 때 참인지 판별하는 문제이다.

• 조건명제는 or 로 풀어쓸 수 있기 때문에 우리가 원하는 복합명제는 (a or b) and (c or d or e) and ... 이렇게 나타낼 수 있다. 이렇게 and 사이에는 or 만 들어있는 식을 CNF(Conjuctive Normal Form) 이라고 하고 괄호에 해당되는 부분을 Clause 라고 한다.
• CNF 를 Satify 되는 조건이라고 해서 SAT 문제라 불린다. 이때 Clause 안에 단순명제가 1개 있으면 1-SAT, 2개 있으면 2-SAT 라고 한다. 3개 이상인 경우 3-SAT 으로 환원이 되지만 NP-Hard 문제라고 한다.

풀이

2-SAT 는 명제의 특성 상 a or b <=> (~a)->b 임을 이용해 그래프를 만들어 문제를 해결한다. 2-SAT 에서 모순은 a <-> ~a 일 때 생겨나므로 동치인 문장의 집합을 구성해야한다. 이는 SCC 을 통해 구할 수 있다.

• 이때 명제의 대우를 그래프의 간선에 추가 해야한다는 것을 잊지 말자. 또한 동치인 문장의 집합의 특성상 a 가 포함된 집합이 존재한다면 ~a 가 포함된 집합이 항상 존재한다.

진리값을 결정하는 방법은 SCC 를 DAG Graph 를 위상정렬했을 때 Leaf Node 에 가까운 순서대로 T 를 부여하는 것이다. 혹은 Leaf Node 와 먼 순으로 F 를 부여해도 된다. 전건이 거짓인 경우나 후건이 참인 경우는 명제가 항상 참이기 때문에 Greedy 전략이 성립한다.

• DFS 탐색 순서가 아님에 주의하자. DFS 순서대로 부여하면 대우에 해당되는 Graph 는 Greedy 조건에서 벗어나게 된다. 예를들어 1 -> ~2, 2 -> ~1 에서 1 -> ~2 를 DFS 한다고 하면 1 을 거짓으로 두고 ~2 를 거짓으로 두게 된다. 그러면 2 -> ~1 가 거짓이 된다. 굳이 DFS 를 쓴다고 한다면 Leaf Node 순서대로 T 를 부여하면 이런 문제가 생기지 않는다.
• 아래 코드처럼 Tarjan 를 쓰는 경우 SCC 의 위상정렬 시의 인덱스를 얻게 되므로 부등식만으로 진리값을 알 수 있다.

시간 복잡도

O(\(\vert \mathrm{V} \vert + \vert \mathrm{E} \vert\))

코드

const int MAX_IN = 20001;

vector<int> lines[MAX_IN];
stack<int> st;
int visits[MAX_IN], n_visit;
int roots[MAX_IN], n_root;

int SCC(int cur)
{
	int res = visits[cur] = ++n_visit;
	st.push(cur);

	for (auto l : lines[cur])
	{
		if (roots[l]) continue;
		if (visits[l]) res = min(res, visits[l]);
		else res = min(res, SCC(l));
	}

	if (res == visits[cur])
	{
        n_root++;
		while (1)
		{
			int tmp = st.top();
			roots[tmp] = n_root;
			st.pop();
			if (tmp == cur) break;
		}
	}

	return res;
}

int n;
int Neg(int a) { return a > n ? a - n : a + n; }

int main()
{
	int m; cin >> n >> m;

	for (int i = 0; i < m; i++)
	{
		int a, b; cin >> a >> b;
		if (a < 0) a = -a + n;
		if (b < 0) b = -b + n;
		lines[Neg(a)].push_back(b);
		lines[Neg(b)].push_back(a);
	}

	bool ans = true;
	for(int i = 1; i <= 2 *n; i++) if(visits[i]== 0) SCC(i);

	for (int i = 1; i <= n; i++) if (roots[i] == roots[i + n]) { ans = false; break; }
	cout << ans << endl;
	if (ans) {
		for (int i = 1; i <= n; i++) cout << (roots[i] < roots[n + i]) << ' ';
	}
}