[백준] 11280 2-SAT-3

식 f : (x1||x2)&&(x2||x3)&&(~x1||x3) 와 같이 Or로 연결된 K개의 절로 이루어진 식을 만족하는 해가 존재하는지 묻는 문제입니다.

 

 

 

식 f 의 해는 네이브하게 x1 ,x2 ,x3에 각각 0과 1을 넣으면서 확인이 가능합니다. 하지만 변수의 개수가 많아지면....너무 오래걸립니다.

 

따라서 다른방법을 고안한게 SCC를 이용한 방법입니다. 

하나의 절 x1||x2는 두개의 명제로 나눌 수 있습니다

~x1->x2 와 ~x2->x1입니다.

x1또는 x2둘중에 적어도 하나는 참이여야 하기 때문입니다.

 

이 명제만을 이용해 함의 그래프를 그릴 수 있습니다.

이 그래프는 대칭을 이룹니다.

 

P->Q 명제를 함의하는 이 그래프는

P가 참일때는 Q는 반드시 참이여야하고

P가 거짓일때는 Q는 참이든 거짓이든 상관 없이 참입니다.

 

따라서 P가 참이고 Q가 거짓인 간선만 없으면 됩니다.

SCC를 이용해 해가 없는 경우를 찾을 수 있습니다.

바로 SCC중에 하나의 변수를 가리키는 A와 !A정점이 동시에 존재하면 해는 없습니다.

 

이때 타잔 알고리즘을 사용해서 하나의 SCC안에 두개의 정점이 동시에 존재하는지 확인하면 됩니다.

#include<bits/stdc++.h>

using namespace std;
typedef pair<int, int> pi;
int N, M, A, B;
vector<pi> cl;
int v[20001], s[20001];
int cnt = 0, num = 0;
vector<int>adj[20001];
vector<int>st;
vector<vector<int>>scc;
int dfs(int k){
	int parent=v[k] = ++cnt; //카운트
	st.push_back(k); //스택에 푸쉬합니다
	for (auto r : adj[k]) { //모든 간선에 접근 O(E)
		if (!v[r]) { //만약 미방문시 방문합니다
			parent = min(parent, dfs(r));
		}
		else if (!s[r]) { //방문했고, scc안에 들어있지 않으면 scc입니다.
			parent = min(parent, v[r]);
		}
	}

	if (v[k] == parent) {
		++num;
		vector<int>temp;
		while (auto t = st.back()) {
			st.pop_back();
			s[t] = num;
			temp.push_back(t);
			if (t == k)break;
		}
		scc.push_back(temp);
	}
	return parent;
}
void tarjan() { //타잔 ALL DFS O(V)
	for (int i = 1; i <= 2 * N; i++) {
		if (!v[i])
			dfs(i);
	}
}
bool SAT2() {
	tarjan();
	for (int i = 1; i <= 2 * N; i+=2) {
		if(s[i]==s[i+1])return false;  //i번째 정점과 i+1번째 정점은 같은 변수를 가리킵니다
        //만약 s[i]와 s[i+1]이 같다면, 하나의 scc안에 두 정점이 동시에 존재하므로 false입니다
	}
	return true;
}
int main() {
	ios_base::sync_with_stdio(false);
	cin.tie(NULL);

	cin >> N >> M;
	for (int i = 0; i < M; i++) {
		cin >> A >> B;
		int a, na, b, nb;
		if (A > 0) {
			a = A * 2 - 1;
			na = A * 2;
		}
		else {
			a = -A * 2;
			na = -A * 2 - 1;
		}

		if (B > 0) {
			b = B * 2 - 1;
			nb = B * 2;
		}
		else {
			b = -B * 2;
			nb = -B * 2-1;
		}
		adj[nb].push_back(a);
		adj[na].push_back(b); //하나의 정점에 대해 두개의 간선
	}
	cout << SAT2();//2-SAT
}