2-SAT

2-SAT문제는, 두 개씩 묶인 boolian 변수들의 AND 연산을 true로 만들 수 있는 변수들의 boolian 설정이

가능한지 묻는 문제이다. 역시 글로 쓰니 어렵다. 식으로 알아보자.

f: (x1∨x2) ∧(~x3∨x4)∧.... 일 때, xn을 true/false(boolian 변수이므로)로 설정해서 이 전체 식이 true가 될 수 있는지

여부를 판단하는 것이다. 당신은 명제의 화살표를 그래프의 간선에 대응시킬 수 있다는 생각을 해 본적 있는가?

본인도 물론 없다. 어떤 훌륭한 친구가 그런걸 생각하겠는가. 근데 누가 했대...

각 절(저 괄호로 묶인 단위를 절이라 한다)이 true가 되기 위한 조건을 생각해 보자. 첫 번째 절에서, x1이 true이면? x2는 true이던지 false이던지 그게 먼 좃상관임;; 그러나, x1이 false이면 이야기는 달라진다. x2가 true가 되어야지, 안그러면

절들을 잇는 AND연산에 의해 f는 장렬히 false가 되버린다. 그래서 이렇게 필수적인 관계를 간선으로 나타내어, 잇는거다.

위 사례를 예시로 들어보자.

이렇게 되는 건 알겠다, 그런데 이걸로 이제 멀해야함?

당신은 SCC를 알아야 한다(모르면 kks227님 블로그나 justicehui님 블로그 가서 보고와라).

이러한 일명 '명제 간선'들로 사이클이 생길 수 있다. 이들을 묶는 알고리즘이 SCC이므로, SCC가 필요함은 자명하다.

한 명제 SCC 내부에서는 어느 것이 참이 되면, 나머지도 다 참이 되고, 또 필연적으로 이러한 SCC의 반전 사이클(그 명제들의 대우 관계로 이루어진 하나의 사이클)도 존재함은 당연하다. 이 경우, SCC내부에서 어느 것이 거짓이 되면, 그 반전 사이클 내부의 정점들은 모두 참이 되어, 정당성을 지닐 수 있다.

 이제 SCC를 돌려 묶자. (반전 쌍과 일반 쌍에 대해). 이렇게 되면 뭔가 한것같아서 기분은 좋은데, 그래서 왜하는거임?이라는 의문이 생길 수 있다. 이 때 이를 하는 이유는, 한 변수와 그 변수에 NOT을 붙인 변수가 한 SCC에 있는 친구가 한 SCC 안에 있으면 논리적 모순이 발생하기 때문이다. 이렇게 묶이면 f는 true가 될 수 없다.

https://www.acmicpc.net/problem/11280

11280번: 2-SAT - 3

#include<bits/stdc++.h>
#define INF 10000
using namespace std;
typedef long long int ll;
ll N, M, sn[20001], num, dfsn[20001], cnt;
vector<ll> a[20001];
bool finished[20001];
stack<ll> s;
ll DFS(int now){
	dfsn[now]=++cnt;
	s.push(now);
	ll res=dfsn[now];
	for(ll i:a[now]){
		if(dfsn[i]==0) res=min(res, DFS(i));
		if(!finished[i]) res=min(res, dfsn[i]);
	}
	if(res==dfsn[now]){
		while(1){
			ll t=s.top();
			s.pop();
			sn[t]=num;
			finished[t]=true;
			if(t==now) break;
		}
		num++;
	}
	return res;
}
int main(){
	cin >> N >> M;
	for(int i=1;i<=M;i++){
		int b, c;
		cin >> b >> c;
		if(b<0 and c<0){
			a[-b].push_back(-c+INF);
			a[-c].push_back(-b+INF);
		}
		else if(b<0 and c>0){
			a[-b].push_back(c);
			a[c+INF].push_back(-b+INF);
		}
		else if(b>0 and c<0){
			a[b+INF].push_back(-c+INF);
			a[-c].push_back(b);
		}
		else{
			a[b+INF].push_back(c);
			a[c+INF].push_back(b);
		}
	}
	for(int i=1;i<=N;i++){
		if(dfsn[i]==0) DFS(i);
		if(dfsn[i+INF]==0) DFS(i+INF);
	}
	for(int i=1;i<=N;i++){
		if(sn[i]==sn[i+INF]){
			cout << "0";
			return 0;
		}
	}
	cout << "1";
}

이건 코드다. kks227님의 SCC구현을 참고한 코드이다.

이제 그러면 이러한 변수 x1, ... xn을 어떻게 찾느냐! 할 수 있다.

이는 한 명제 p=>q관계에서, p가 true이면 q가 true"여야만"한다. 빡빡한 관계다. 그런데 말입니다, p가 false이면

q는 뭐가되던 상관없다. 그렇기에, 강한 조건보다는 약한 조건으로부터 전파시켜가기 위해, topological sorting 이후 첫 번째 SCC부터 false로 설정하며(이 때 내부의 변수들은 false : 반전 변수들은 true) 진행시킬 수 있다.

그런데, 메모리 초과다.

그렇다면 다른 topological sorting 방법을 써야 하는데, 사실 이미 저 SCC들은 정렬되어 있다.

왜냐? dfs를 실행하면서 queue에 넣는 과정을 역으로 실행하면 방문순서가 튀어나온다. 이는 머릿속에서 시뮬 돌려도 알 수 있다. 그렇기에, dfs하면서 어떻게 보면 SCC를 묶어 준 우리는, 은연중에 정렬을 한 것이다. 즉, SCC의 번호가 클수록 위상 정렬 순서 앞에 있다. 

https://www.acmicpc.net/problem/11281

11281번: 2-SAT - 4

#include<bits/stdc++.h>
using namespace std;
typedef long long int ll;
ll N, M, sn[20001], num, dfsn[20001], cnt, in_deg[20001], INF, result[20001];
vector<ll> a[20001];
bool finished[20001];
vector<vector<ll>> SCC;
stack<ll> s;
queue<int> q;
ll DFS(int now){
	dfsn[now]=++cnt;
	s.push(now);
	ll res=dfsn[now];
	for(ll i:a[now]){
		if(dfsn[i]==0) res=min(res, DFS(i));
		if(!finished[i]) res=min(res, dfsn[i]);
	}
	if(res==dfsn[now]){
		while(1){
			ll t=s.top();
			s.pop();
			sn[t]=num;
			finished[t]=true;
			if(t==now) break;
		}
		num++;
	}
	return res;
}
int main(){
	memset(result ,-1, sizeof(result));
	cin >> N >> M;
	INF=N;
	for(int i=1;i<=M;i++){
		int b, c;
		cin >> b >> c;
		if(b<0 and c<0){
			a[-b].push_back(-c+INF);
			a[-c].push_back(-b+INF);
		}
		else if(b<0 and c>0){
			a[-b].push_back(c);
			a[c+INF].push_back(-b+INF);
		}
		else if(b>0 and c<0){
			a[b+INF].push_back(-c+INF);
			a[-c].push_back(b);
		}
		else{
			a[b+INF].push_back(c);
			a[c+INF].push_back(b);
		}
	}
	for(int i=1;i<=2*N;i++){
		if(dfsn[i]==0) DFS(i);
	}
	for(int i=1;i<=N;i++){
		if(sn[i]==sn[i+INF]){
			cout << "0";
			return 0;
		}
	}
	cout << "1" << '\n';
	for(int i=1;i<=N;i++){
		if(sn[i]>sn[i+INF]){
			result[i]=0;
		}
		else result[i]=1;
	}
	for(int i=1;i<=N;i++) cout << result[i] << ' ';
}

끗