(출처) https://www.acmicpc.net/problem/11281
종만북 MEETINGROOM 문제
책의 MEETINGROOM 문제를 고민하다 포기하고 해답을 봤는데 2-SAT 문제로 판명하고 문제를 해결하더라. 나는 책의 문제 말고 다른 문제로 직접 풀어보고 싶어서 백준의 같은 유형 문제를 풀어보았다.
2-SAT
SAT 문제에서는 논리식을 다루어 문제를 해결한다.
참 혹은 거짓으로 구분될 수 있는 특정 변수(상황)들을 OR 관계로 짝을 지어 하나의 절을 구성시키고, 각 절을 AND로 묶어 나열하면 하나의 논리식이 되는데, 해당 논리식을 성립 가능 한 것인지 불가능한 것인지 판단하는 것이 SAT 문제를 해결하는 과정이다.
논리식의 절에 포함된 변수들이 K 개씩으로 형성되어 있을 때 K-SAT이라고 부른다. 2-SAT에서는 절의 변수가 2개씩 존재한다.
이 2-SAT을 해결하는 과정은 책에 워낙 설명이 잘 되어있고, 이 이상으로 이것을 내가 풀어서 잘 설명하기는 불가능할 것 같으니 그냥 내가 이해하면서 느낀 바를 적어보고자 한다.
논리식
논리식을 해결하는 SAT 문제의 해결 과정은 귀류법 판단의 진행과정과 비슷했다.
만약 특정 절 (A || B)가 주어졌다면 식이 성립하기 위해서는 A와 B 둘 중 하나는 True가 되어야 한다.
A와 B 둘 중 하나는 True가 돼야 한다는 조건을 A와 B에 대한 확실한 명제로 표현하면 !A -> B , !B -> A 로 나타낼 수 있다.
이런 식으로 각 절을 명제로 표현하고 꼬리를 이어주면 기존의 논리식을 명제식 모음으로 전환시킬 수 있다. 이렇게 논리식을 명제식으로 변환하면 이 후의 논리판단 과정은 이제 완벽한 귀류법이다.
만약 명제식 중 특정변수가 자신의 부정으로 이어지게 된다면(X -> !X) 해당 명제식은 당연하게도 모순이다. 따라서 X -> !X 로 이어지는 명제식이 있는지 찾는 것으로 전체 논리식의 True or False 여부를 판단할 수 있다.
이때 A -> B와 같이 하나의 상황에서 다른 상황으로 이어지는 명제식은, 하나의 노드에서 다른 노드로 이어지는 방향그래프의 개념으로 추상화시키기 굉장히 적합하다.
따라서 변환한 명제식을 바탕으로 그래프를 작성하고, 그래프를 탐색하면서 A -> !A 과 같은 경로가 존재하는지 판단한다면 전체 논리식의 성립가능여부를 판단할 수 있다.
논리식에서 개별변수의 답(True or False)을 확정하기
위와 같이 X->!X의 경로가 존재하는지 그래프를 탐색하는 것만으로 논리식의 성립가능여부를 판단할 수는 있지만, 이것만으로는 성립되는 경우의 개별변수들 값들이 각각 어떤 값으로 설정되는지에 대한 정보를 알 수 없다.
따라서 개별변수들의 True or False 값을 확정 짓기 위해서는 명제식의 조건을 하나씩 따라가보며 판단해야 한다. (그래프의 정점을 하나씩 따라가보며)
가장 처음, 논리식의 각 절 (A || B) 를 명제로 변환할 때를 떠올려보면 총 2가지의 경우를 모두 가정했었다. (B가 거짓이 되고 A가 참인 경우와 A가 거짓이 되고 B가 참인 경우, !B -> A // !A -> B)
이 때 어떤 명제식을 참으로 둬야 논리식을 성립하게 만드는 것인지는 모르지만 적어도 모든 명제식의 조건을 전부 참으로 바라볼 수 없다는 것은 당연히 알 수 있다. (!B 정점과 B 정점 혹은 !A정점 A 정점이 동시에 참이 될 수는 없기 때문)
따라서 대칭으로 나눠진 2가지의 명제식 조건 중 하나는 거짓이 되는 조건이고 다른 하나를 참이 되는 조건 일 텐데, 그렇다면 참이 되게 하는 명제식 모음이 과연 어떤 것들인지 판단하여 찾아주는 것이 결국 답을 구하기 위한 목표가 된다.
2가지로 나눠진 명제식 중 어느 것이 답을 성립하게 하는 명제식인지 판단할 수 있다면, 해당 명제식에 포함된 정점들을 보면서 개별변수의 답들이 어떻게 구성되는지 판단할 수 있게 되기 때문이다.
어떤 것이 참이 되는 명제식인가
바로 본론부터 답을 성립하게 하는 명제식이 어떤 것인지를 판단하는 과정의 핵심을 말해보자면 참인 조건에서 거짓으로 가는 조건이 명제에 존재할 수 없다는 사실을 이용하여 정점을 하나씩 구분해 나가는 것이라고 할 수 있다. (하나씩 정점을 구분해서 거짓이 되는 명제식과 참이 되는 명제식에 알맞게 분류하여 넣어준다)
참인 조건에서 거짓으로 가는 조건이 존재한다면 명제식 자체가 모순이 되어버린다. 그렇기 때문에 명제식에는 이와 같은 모순이 존재해서는 안 된다.
만약 만든 명제식이 참인 조건에서 거짓으로 가는 경우가 반드시 존재할 수밖에 없는 경우였다면 (X -> !X) 이미 전체 논리식 판단과정에서 모순이 발견되어 논리식을 False로 판정하고 걸러졌을 것이다.
따라서 전체 논리식이 True가 된다고 이미 판정한 경우에는, 참인 조건에서 거짓으로 어쩔 수 없이 갈 수밖에 없는 상황은 존재하지 않는다. 따라서 이 조건을 계속 유지하면서(참 -> 거짓 논리연결이 존재하지 않게끔) 모든 정점들을 참이 되는 명제식과 거짓이 되는 명제식에 하나씩 분류해 준다면 올바르게 거짓과 참인 명제식을 구분하게 될 것이다.
그렇다면 위 조건을 계속 유지되도록 하면서 참, 거짓 정점을 분류하는 과정을 어떻게 진행해야 하는 것일까?
명제식 그래프에서 Indegree가 0인 정점을 처음으로 골라, 해당 정점부터 참인 명제식과 거짓 명제식 두 곳중 어느 집단에 소속시킬 것인지를 판단하려고 한다 해보자.
분류과정 동안 참인 조건에서 거짓으로 가는 조건이 명제에 존재할 수 없다(존재해서는 안된다) 라는 조건을 계속 유지 시키기 위해서는, 이 정점을 거짓인 명제식에 소속시켜 버리는 것이 앞의 조건을 절대 해치지 않는다는 것을 알 수 있다.
앞의 정점을 그냥 거짓으로 소속시켜 버리면 이어서 따라오는 정점의 참, 거짓 여부 판단에 영향을 끼치지 못하므로 해당 정점과 이어지는 다음 정점도 자유롭게 참, 거짓 여부를 결정지을 수 있게 된다.
즉 명제식에서 가장 첫 스타트가 되는 정점들을 거짓으로 분류하는 것은 어떠한 경우에도 옳다.
그리고 명제식 그래프에는 하나의 정점과 반대되는 정점이 반드시 존재하므로 이렇게 하나의 정점을 거짓으로 분류시키면 자연스럽게 다른 하나를 참으로 결정짓는 것이 된다.
따라서 모든 정점이 분류가 완료되도록 그래프에서 indegree가 0인 정점을 하나씩 잘라 계속 거짓으로 분류시켜 나간다면 참이 되는 명제식과 거짓이 되는 명제식을 완벽하게 구분 지을 수 있게 된다.
이 때 같은 사이클에 포함된 정점들을 하나의 정점으로 묶어서 바라본다면 위상정렬만으로 위의 분류과정을 진행할 수 있게 된다.
즉 이 분류과정을 구현하는 방법은 명제식 그래프를 scc로 분류하고 컴포넌트별로 위상정렬을 진행시킨 뒤 먼저 정렬된 컴포넌트부터 거짓으로 분류하는 작업을 모든 컴포넌트가 분류될 때 까지 진행시키면 된다.
코드
#include <iostream>
#include <vector>
#include <algorithm>
#include <cstdlib>
#include <stack>
using namespace std;
vector<vector<int>> graph;
vector<int> discoverd;
vector<int> scc_ids;
int sccid;
int vertex_counter;
stack<int> st;
//O(N)
void making_graph(int a, int b) {
if (a == -b) return;
//graph[0] = 1, graph[1] = -1, graph[2] = 2, graph[3] = -2 , ...
int t_a = 2 * (abs(a) - 1);
int t_b = 2 * (abs(b) - 1);
int n_a = 2 * (abs(a) - 1) + 1;
int n_b = 2 * (abs(b) - 1) + 1;
if (a < 0) {
t_a = 2 * (abs(a) - 1) + 1;
n_a = 2 * (abs(a) - 1);
}
if (b < 0) {
t_b = 2 * (abs(b) - 1) + 1;
n_b = 2 * (abs(b) - 1);
}
if (a == b) graph[n_a].push_back(t_b);
else {
graph[n_a].push_back(t_b);
graph[n_b].push_back(t_a);
}
}
int scc(int here) {
vertex_counter++;
discoverd[here] = vertex_counter;
st.push(here);
int ret = vertex_counter;
for (int i = 0; i < graph[here].size(); i++) {
int there = graph[here][i];
if (discoverd[there] == -1) {
ret = min(ret, scc(there));
}
else if (scc_ids[there] == -1) ret = min(ret, discoverd[there]);
}
if (ret == discoverd[here]) {
int st_vertex = -1;
while (st_vertex != here ) {
st_vertex = st.top();
scc_ids[st_vertex] = sccid;
st.pop();
}
sccid++;
}
return ret;
}
vector<pair<int,int>> tajan_scc(int n) {
scc_ids = vector<int> (2 * n, -1);
discoverd = vector<int>(2 * n, -1);
sccid = 0;
vertex_counter = -1;
for (int i = 0; i < 2 * n; i++) {
if (scc_ids[i] == -1) scc(i);
}
for (int i = 0; i < 2 * n; i+= 2) {
if (scc_ids[i] == scc_ids[i + 1]) return vector<pair<int, int>> ();
}
vector<pair<int, int>> ret(2 * n);
for (int i = 0; i < 2 * n; i++) {
ret[i].first = -scc_ids[i];
ret[i].second = i;
}
return ret;
}
vector<int> two_sat(int n) {
vector<pair<int, int>> t_scc = tajan_scc(n);
if (t_scc.empty()) return vector<int>();
sort(t_scc.begin(), t_scc.end());
vector<int> ret (n, -1);
for (int i = 0; i < 2 * n; i++) {
int vertex = t_scc[i].second;
int variable = vertex / 2, is_true = (vertex % 2 == 0);
if (ret[variable] != -1) continue;
ret[variable] = !is_true;
}
return ret;
}
int main() {
ios_base::sync_with_stdio(false);
cin.tie(NULL);
cout.tie(NULL);
int n, m;
cin >> n >> m;
graph.reserve(2 * n);
graph = vector<vector<int>> (2 * n);
for (int i = 0; i < m; i++) {
int a, b;
cin >> a >> b;
making_graph(a, b);
}
vector<int> ret = two_sat(n);
if (ret.empty()) cout << 0 << "\n";
else {
cout << 1 << "\n";
for (auto i = ret.begin(); i < ret.end(); i++) {
if (i == ret.end() - 1) {
cout << *i << "\n";
break;
}
cout << *i << " ";
}
}
return 0;
}기억하고 싶은 점
정 모르겠다고 싶은 건 빠르게 포기하고 풀이를 보면서 내 것으로 흡수하는식으로 하는 게 나을 것 같다.
