2-sat 쉽게 이해하기 [boj] 11280 2-SAT - 3

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

11280번: 2-SAT - 3

2-sat은 2개의 변수가 or (v) 관계로 이어진 1개 이상의 절(clause)을 and (⋀)로 이었을 때, 전체 식의 결과가 true를 반환하는 변수가 존재하냐를 묻는 질문이다. 변수가 4개고 2개의 절이 있는 식 f의 예시는 아래가 있다. ¬ 기호는 not 을 의미한다. 예를 들면, a가 참(true)일 때, ¬a는 거짓(false)이 된다. 

f = (a v ¬b) ⋀ (c v ¬d) 

식 f를 참으로 만드는 경우는 많다. 단순하게 a와 c가 참이면 된다. (또는 b와 d가 false 여도 a, c 와는 무관하게 참이 된다)

많은 블로그에서 명제 얘기를 하면서 어렵게 설명이 되어있어서 내가 이해한 대로 쉽게 풀어보려고 한다. 첫 번째 절 (a v ¬b)을 참으로 만들기 위해서는 a가 참이거나 ¬b가 참이면 된다. 다시 말하면 ¬b가 거짓이면 a는 무조건 참이여야 하고, a가 거짓이면 ¬b는 무조건 참이어야 한다.

이걸 다시 나타내보면 "¬b가 거짓, 즉 b가 참일 때, a는 참이여야한다" 는 관계와 "a가 거짓일 때, ¬b가 참이여야 하므로 b는 거짓이 여야 한다"의 두 가지 관계를 뽑아낼 수 있다. 

이걸 그래프로 나타내보자.

하나의 변수를 참과 거짓의 두 개의 노드로 표현할 수 있으며, 두 개의 그래프를 그릴 수 있다.

식 f를 좀 더 복잡하게 설계해보자. 아래는 변수가 3개, 절이 3개인 2-sat에 대한 식이다.

f = (a v ¬b) ⋀ (c v ¬a) ⋀ (¬b v ¬c)

이 식에서 뽑아낼 수 있는 관계는 아래와 같다. 한 쪽을 거짓으로 고정하면 나머지 한쪽은 무조건 참이 되어야 하므로 절마다 2개의 관계를 뽑을 수 있다.

그려진 그래프를 보면 사이클이 존재하지 않음을 의미하며, 이런 경우에는 항상 답이 존재함을 알 수 있다. 답이 존재하지 않으려면 "a가 참일 때, 어찌어찌 절을 따라갔더니 결국 a는 거짓이어야 한다"와 같은 모순이 존재해야 하는데, 사이클이 없다면 어찌어찌 절을 따라가서 다시 a로 오는 경우가 절대로 존재하지 않기 때문에 항상 답이 존재한다.

그럼 우리는 결국 식 f에서 사이클이 생기는 경우를 확인해봐야 하고, "이 사이클에서 모순이 있냐?" 를 봐야 한다. 그래프에서 사이클을 이루는 정점을 찾는 방법은 SCC로 확인했었다. 2020.07.17 - [Solved.ac/Class 6] - [BOJ] 백준 2150번: Strongly Connected Component

[BOJ] 백준 2150번: Strongly Connected Component

그럼 우리가 할 일은, SCC로 사이클을 찾고 a 와 ¬a가 공존하는 사이클이 있냐를 파악하는 문제로 볼 수 있다. 어려워 보였던 2-sat이 익숙한 문제로 바뀌었다.

그럼 이제 관계가 주어질 때 이 관계를 그래프로 잘만 나타낸다면 SCC 코드를 재탕해서 문제를 풀 수가 있다.

나는 네트워크 플로우에서 사용했던 정점 표현 방식을 그대로 사용했다. 정점이 n개가 주어지므로, 1번부터 n번 변수에 대한 참을 나타내는 변수는 그대로 정점 번호를 취하고 거짓을 나타내는 변수는 n을 더해서 중복된 정점 번호가 없게 표현했다. 다른 블로그에서는 2를 곱하고 1을 or 하거나 xor 하는 방식을 썼는데 난 이게 더 편했다. (사실 다른 블로그에서 한 방법이 코드가 간결하고, 잘하는 사람들이 짠 거라 그걸 따라 하는 게 정신 건강에 좋을 거 같음.. 난 허접이라..)

보통 문제에서 not 에 대한 변수는 음수로 주어지길래 a = -a와 같이 처리하고 n을 더해주었다.

if (a > 0 && b > 0) {
    // -a -> b
    // -b -> a;
    v[a + n].push_back(b);
    v[b + n].push_back(a);
    rv[a].push_back(b + n);
    rv[b].push_back(a + n);
}
else if (a > 0) {
    // a v -b
    // -a -> -b;
    // b -> a;
    b = -b;
    v[a + n].push_back(b + n);
    v[b].push_back(a);
    rv[a].push_back(b);
    rv[b + n].push_back(a + n);
}
else if (b > 0) {
    // -a v b
    a = -a;
    v[a].push_back(b);
    v[b + n].push_back(a + n);
    rv[b].push_back(a);
    rv[a + n].push_back(b + n);
}
else {
    // -a v -b
    a = -a;
    b = -b;
    v[a].push_back(b + n);
    v[b].push_back(a + n);
    rv[b + n].push_back(a);
    rv[a + n].push_back(b);
}

이렇게 하니 SCC 코드를 그대로 사용할 수 있게 전처리가 끝났다. 그 후, 각 정점이 속한 그룹 번호를 scc 배열에 저장하도록 SCC를 수행하면 우리는 하나의 변수에 대한 참, 거짓의 정점이 속한 그룹 번호를 scc 배열에 인덱싱 접근해서 바로 알 수 있다.

이후, 위에서 언급한 [그럼 우리는 결국 식 f에서 사이클이 생기는 경우를 확인해봐야 하고, "이 사이클에서 모순이 있냐?"를 봐야 한다.]의 문제를 해결하기 위해 우리는 1번 정점부터 n 번정점까지 쭉 돌면서 scc [i] == scc [i+n]이 존재하는지 판별하면 2-sat을 풀 수 있다. 만약 사이클이 없는 관계라면 모든 정점이 속한 SCC의 그룹 번호가 모두 다르므로 당연하게 답이 존재함을 알 수 있다. 

코드

#include <bits/stdc++.h>

using namespace std;

typedef long long ll;
typedef pair<int, int> pii;
typedef pair<ll, ll> pll;
int n, m;
// 변수는 n개, 절은 m 개
vector<int> v[20001];
vector<int> rv[20001];
int visited[20001]{};
stack<int> s;
int scc[20001];
void dfs(int node) {
	visited[node] = 1;
	for (auto it : v[node]) {
		if (!visited[it]) {
			dfs(it);
		}
	}
	s.push(node);
	return;
}

void dfs2(int node, int id) {
	scc[node] = id;
	visited[node] = 1;
	for (auto it : rv[node]) {
		if (!visited[it]) {
			dfs2(it, id);
		}
	}
}


void solve() {
	cin >> n >> m;
	for (int i = 0; i < m; i++) {
		int a, b;
		cin >> a >> b; // 
		if (a > 0 && b > 0) {
			// -a -> b
			// -b -> a
			v[n + a].push_back(b);
			v[n + b].push_back(a);
			rv[b].push_back(n + a);
			rv[a].push_back(n + b);
		}
		else if (a > 0) {
			// a v -b
			b = -b;
			// b -> a
			// -a -> -b
			v[n + a].push_back(n + b);
			v[b].push_back(a);
			rv[a].push_back(b);
			rv[n + b].push_back(n + a);
		}
		else if (b > 0) {
			// -a v b
			a = -a;
			// a -> b
			// -b -> -a

			v[n + b].push_back(n + a);
			v[a].push_back(b);
			rv[b].push_back(a);
			rv[n + a].push_back(n + b);
		}
		else {
			a = -a, b = -b;

			// -a v -b
			// a -> -b
			// b -> -a
			v[b].push_back(n + a);
			v[a].push_back(n + b);
			rv[n + a].push_back(b);
			rv[n + b].push_back(a);
		}
	}
	memset(visited, 0, sizeof(visited));
	for (int i = 1; i <= n + n; i++) {
		if (!visited[i]) {
			dfs(i);
		}
	}
	memset(visited, 0, sizeof(visited));
	while (!s.empty()) {
		int node = s.top(); s.pop();
		if (!visited[node]) {
			dfs2(node, node);
		}
	}
	int flag = 1;
	for (int i = 1; i <= n; i++) {
		if (scc[i] == scc[n + i]) {
			flag = 0;
		}
	}
	cout << (flag ? 1 : 0);
}


int main() {
	ios_base::sync_with_stdio(false);
	cin.tie(0);
	cout.tie(0);
	int tc = 1;
	//cin >> tc;
	for (; tc--;) {
		solve();
	}
}

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

11281번: 2-SAT - 4

이 문제를 해결했다면, 이제는 2-sat의 식 f를 만족하기 위해 각 변수에 어떠한 값이 들어가야 하는지 알아보자. 참 = 1, 거짓 = 0으로 나타낸다고 해보자.

일단 답이 존재하지 않는 경우는 찾을 필요가 없으므로 생각하지도말고, 답이 있는 경우만 알아보자. 아래 식을 예시로 하여, 그래프를 그려보면 왼쪽과 같고 보기 편하게 조금만 위치를 수정하면 오른쪽과 같다.

f = (a v b) ⋀ (c v ¬a) ⋀ (¬b v ¬c) ⋀ (b v d) 

SCC 그룹을 {a, ¬b, c}, {d}, {¬a, ¬c, b}, {¬d} 4개를 찾았다. SCC 간 연결 {a, ¬b, c} → {d} 와, {¬d} → {¬a, ¬c, b}  두 개가 구해졌다. 이 SCC 간 연결을 이 글의 처음에 얘기했던 한 절의 두 개의 변수 관계로 볼 수 있으며 {¬a, ¬c, b}가 거짓일 때 {d}가 참 또는 {d}가 거짓일 때 {¬a, ¬c, b}가 참이면 전체 식 f가 참이 되는 조건을 만족할 수 있다는 얘기와 같다.

후자의 경우 간선이 역방향이므로 전자만 생각해보자. 그러면 우리는 SCC 간 연결에 대하여 화살표의 왼쪽의 SCC 정점들을 거짓(false) 화살표 오른쪽의 SCC의 정점들은 참(true)으로 설정해 주면 된다. 2-sat의 식 f를 만족하는 경우 모든 그래프는 대칭이 되므로 모든 관계의 왼쪽 SCC 그룹에 대한 변수들의 값을 찾으면 반대쪽은 자연스럽게 찾아진다. 

이를 위해, SCC의 그룹을 위상 정렬하여 순서대로 아직 값이 할당되지 않은 변수(화살표 왼쪽에 위치한 SCC에 속한 정점들)에 대하여 false를 지정해주면 되는데, 이 위상은 이미 SCC를 구하는 과정에서 정해졌다. 어디서 구해졌냐고? 두 번째 dfs를 수행할 때이다. SCC에서 다른 그래프로 나가는 간선이 연결되어 있는 경우, 무조건 해당 SCC는 그래프에서 가장 마지막 cnt 값을 갖는다. 이건 몇 개만 그려보면 된다. 하나의 정점도 단일 SCC임을 잊지 말자.

void dfs(int node) {
	visited[node] = 1;
	for (auto it : v[node]) {
		if (!visited[it]) dfs(it);
	}
	dfsv.push_back({ cnt, node });
	cnt += 1;
	return;
}

아래와 같이 dfsv 배열에 저장된 cnt값이 큰 정점일수록 (위상이 가장 높은 정점일수록) SCC를 찾는 두번째 dfs를 먼저 수행된다. dfs 함수를 통해 {a, ¬b, c} → {d} 에서 {a, ¬b, c} 들은 {d}보다 큰 cnt값을 갖는다. 이러한 이유로, {a, ¬b, c} 나 {¬d}의각 정점마다 아래 코드와 같이 idx 값을 1씩 증가시켜 넘겨주면서 dfs2 함수를 호출한다.

int idx = 0;
sort(dfsv.rbegin(), dfsv.rend());
for (auto node : dfsv) {
    if (!visited[node.second]) {
        dfs2(node.second, idx);
    }
    idx++;
}

아래의 dfs2 함수에서 볼 수 있듯, 먼저 수행된 정점들은 작은 scc 값을 갖는다. 

void dfs2(int node, int id) {
	scc[node] = id;
	visited[node] = 1;
	for (auto it : rv[node]) {
		if (!visited[it]) {
			dfs2(it, id);
		}
	}
}

두 번째 dfs를 마무리하면, scc 배열의 값이 작은 노드가 먼저 탐색해야 할 화살표 왼쪽의 정점들이 된다.

화살표 왼쪽의 SCC에 속한 정점들의 변수 값을 false로 하기 위해서, not에 해당하는 정점 번호가 n+1 이상인 경우 해당 정점에 1을 저장하고, 그러지 않다면 0을 저장했다. 

예를 들어 {a, ¬b, c}의 정점들은 false의 값을 가져야 하므로, a = 0, b= 1, c = 0라고 설정하면 {¬a, ¬c, b}는 자연스럽게 반대의 값이 된다. 이와 마찬가지로 {¬d}를 false로 하기 위해서 d = 1로 지정하면 {a, ¬b, c} → {d} 관계에서 false→ true가 된 것을 볼 수 있다. 즉, SCC 그룹의 위상 순으로 false를 채우다 보면 2-sat의 식 f가 true를 만족할 때, 모든 변수의 값이 자동으로 정해진다.

코드

#include <bits/stdc++.h>

using namespace std;

typedef long long ll;
typedef pair<int, int> pii;
typedef pair<ll, ll> pll;
int n, m;
// 변수는 n개, 절은 m 개
vector<int> v[20202];
vector<int> rv[20202];
int visited[20202]{};
vector<pii> dfsv;
int scc[20202];
int ans[10001]{};
int cnt = 0;
vector<pii> tmp; // 포함된 scc 순서, 정점 번호 저장
void dfs(int node) {
	visited[node] = 1;
	for (auto it : v[node]) {
		if (!visited[it]) {
			dfs(it);
		}
	}
	dfsv.push_back({ cnt,node });
	cnt += 1;
	return;
}

void dfs2(int node, int id) {
	scc[node] = id;
	visited[node] = 1;
	for (auto it : rv[node]) {
		if (!visited[it]) {
			dfs2(it, id);
		}
	}
}


void solve() {
	cin >> n >> m;
	for (int i = 0; i < m; i++) {
		int a, b;
		cin >> a >> b; // 
		if (a > 0 && b > 0) {
			v[n + a].push_back(b);
			v[n + b].push_back(a);
			rv[b].push_back(n + a);
			rv[a].push_back(n + b);
		}
		else if (a > 0) {
			b = -b;
			v[n + a].push_back(n + b);
			v[b].push_back(a);
			rv[a].push_back(b);
			rv[n + b].push_back(n + a);
		}
		else if (b > 0) {
			a = -a;
			v[n + b].push_back(n + a);
			v[a].push_back(b);
			rv[b].push_back(a);
			rv[n + a].push_back(n + b);
		}
		else {
			a = -a, b = -b;
			v[b].push_back(n + a);
			v[a].push_back(n + b);
			rv[n + a].push_back(b);
			rv[n + b].push_back(a);
		}
	}
	memset(visited, 0, sizeof(visited));
	for (int i = 1; i <= n + n; i++) {
		if (!visited[i]) {
			dfs(i);
		}
	}
	memset(visited, 0, sizeof(visited));
	int idx = 0;
	sort(dfsv.rbegin(), dfsv.rend());
	for(auto node : dfsv){
		if (!visited[node.second]) {
			dfs2(node.second, idx);
		}
		idx++;
	}
	for (int i = 1; i <= n; i++) {
		if (scc[i] == scc[n + i]) {
			cout << "0";
			return;
		}
	}
	cout << "1\n";
	
	memset(ans, -1, sizeof(ans)); // -1로 초기화
		
	for (int i = 1; i <= n + n; i++) {
		tmp.push_back({ scc[i], i });
	}
	sort(tmp.begin(), tmp.end(), [&](pii a, pii b) {
		return a.first < b.first;
		});

	// scc 번호가 큰 순서대로 탐색 -> 위상 정렬
	for (auto it : tmp) {
		int node = it.second;
		if (node > n) {
			// not 변수
			if (ans[node - n] == -1) {
				ans[node - n] = 1;
			}
		}
		else {
			if (ans[node] == -1) {
				ans[node] = 0;
			}

		}
	}

	for (int i = 1; i <= n; i++) {
		cout << ans[i] << " ";
	}
	
}


int main() {
	ios_base::sync_with_stdio(false);
	cin.tie(0);
	cout.tie(0);
	int tc = 1;
	//cin >> tc;
	for (; tc--;) {
		solve();
	}
}

2-sat을 이해하는데 도움이 됐으면 좋겠다. 이만 글을 마친다.

잘못된 정보나, 틀린 표현이 있다면 댓글로 지적해 주시면 수정하겠습니다. 공부한 것을 정리하고자 쓴 글이기 때문에 잘못된 표현이 있을 수 있습니다.