[그래프] 2-SAT문제 - 1 | JusticeHui가 PS하는 블로그

2-SAT문제란?

2-SAT(2-SATisfiability)문제는 충족 가능성 문제(satisfiability problem)의 한 종류입니다.
충족 가능성 문제란, 여러 개의 boolean변수들로 이루어진 식이 있을 때 각 변수에 값을 할당하여 식을 참으로 만드는 조합을 찾거나, 그러한 조합이 없음을 찾는 문제입니다.

2-SAT문제는
(a₁ ∨ b₁) ∧ (a₂ ∨ b₂) ∧ … ∧ (a_m ∨ b_m)
위와 같은 논리식에서 식을 참으로 만드는 변수 값의 조합을 찾거나, 그러한 조함이 없음을 찾는 것을 목표로 합니다.

아래 식을 봅시다.
f = (x₂ ∨ ￢x₁) ∧ (￢x₁ ∨ ￢x₂) ∧ (x₁ ∨ x₃) ∧ (￢x₂ ∨ ￢x₃) ∧ (x₁ ∨ x₄)
이 식은 {x1 : false, x2 : false, x3 : true, x4 : true} 인 경우에 참이 됩니다.
하지만 아래 식은 어떻게 할당하든 항상 거짓이 됩니다.
f = (x₁ ∨ x₂) ∧ (x₁ ∨ ￢x₂) ∧ (￢x₁ ∨ x₃) ∧ (￢x₁ ∨ ￢x₃)
x1을 true라고 잡으면 x3과 ￢x3 모두 참이 되어야 하고, x1을 false라고 잡으면 x2와 ￢x2 모두 참이 되어야 하기 때문에 항상 거짓이 된다는 것을 알 수 있습니다.

해결 방법

이제, 2-SAT문제를 어떻게 푸는지 알아봅시다.
2-SAT문제에서 주어지는 식은 그래프로 나타낼 수 있습니다. 각 정점들은 x_i와 ￢x_i에 대응됩니다.

정점은 각 변수와 그의 부정형에 대응시킨다고 했으니, 이제 간선을 잘 이어주면 됩니다. (x_i ∨ x_j)를 봅시다.
만약 x_i가 false라면 x_j는 true가 나와야 합니다.
반대로 x_j가 false라면 x_i는 true가 나와야 합니다.
그러므로 ￢x_i → x_j 와 ￢x_j → x_i, 두 개의 간선을 만들어줍시다. 이는 어느 하나가 거짓이라면, 반드시 다른 하나는 참이 되어야 한다는 것을 의미합니다.

주어진 식이 참이 되도록 하는 변수 값의 조합의 존재 여부는 위에서 모델링한 그래프에 따라 결정이 됩니다.
가능한 경우는 x_i와 ￢x_i가 같은 SCC에 속하는 일이 없는 경우와 동치입니다.
만약 같은 SCC에 속해있다면, x_i에서 ￢x_i로 가는 경로, ￢x_i에서 x_i로 가는 경로가 모두 존재한다는 것을 의미합니다. 따라서 x_i와 ￢x_i 모두 참이 되어야 하지만 불가능합니다.
그러므로 참이 되도록 하는 조합의 존재 여부는 SCC 알고리즘을 이용해 구할 수 있습니다.

구현

icpc.me/11280 문제(2-SAT - 3)는 아래 코드를 이용해 풀 수 있습니다.

#include <bits/stdc++.h>
using namespace std;

vector<int> gph[20202], rev[20202];

inline int notX(int x){ return x ^ 1; }
inline int trueX(int x){ return x << 1; }
inline int falseX(int x){ return x << 1 | 1; }

int visit[20202];
vector<int> dfn;
int scc[20202];

void dfs(int v){
	visit[v] = 1;
	for(auto u : gph[v]) if(!visit[u]) dfs(u);
	dfn.push_back(v);
}

void revdfs(int v, int color){
	visit[v] = 1;
	scc[v] = color;
	for(auto u : rev[v]) if(!visit[u]) revdfs(u, color);
}

void getSCC(int n){
	memset(visit, 0, sizeof visit);
	for(int i=1*2; i<=n*2+1; i++){
		if(!visit[i]) dfs(i);
	}
	memset(visit, 0, sizeof visit);
	reverse(dfn.begin(), dfn.end());
	int cnt = 1;
	for(auto i : dfn){
		if(!visit[i]){
			revdfs(i, cnt); cnt++;
		}
	}
}

int main(){
	ios_base::sync_with_stdio(0); cin.tie(0);
	int n, m; cin >> n >> m;

	for(int i=0; i<m; i++){
		int a, b; cin >> a >> b;
		if(a > 0) a = trueX(a);
		else a = falseX(-a);
		if(b > 0) b = trueX(b);
		else b = falseX(-b);

		gph[notX(a)].push_back(b);
		gph[notX(b)].push_back(a);
		rev[b].push_back(notX(a));
		rev[a].push_back(notX(b));
	}

	getSCC(n);

	for(int i=1; i<=n; i++){
		if(scc[trueX(i)] == scc[falseX(i)]){
			cout << "0"; return 0;
		}
	}
	cout << "1";
}

2-SAT문제란?

해결 방법

구현

추천 문제