백준 11281번
오늘 풀어본 문제는 백준의 11281번 문제1이다. 문제 풀이에 사용한 언어는 C++ 이다.
solved.ac 기준 CLASS
문제 정보
이 문제의 내용과 조건은 다음과 같다.
문제
2-SAT은 N개의 불리언 변수 $(x_1, x_2, …, x_n)$ 가 있을 때, 2-CNF 식을 true로 만들기위해 (x_i)를 어떤 값으로 정해야하는지를 구하는 문제이다.
2-CNF식은 $\left( x \lor y \right) \land \left( \lnot y \lor z \right) \land \left( x \lor \lnot z \right) \land \left( z \lor y \right)$ 와 같은 형태이다. 여기서 괄호로 묶인 식을 절(clause)라고 하는데, 절은 2개의 변수를 $\lor$ 한 것으로 이루어져 있다. $\lor$ 는 OR, $\land$ 는 AND, $\lnot$ 은 NOT을 나타낸다.
변수의 개수 $N$과 절의 개수 $M$, 그리고 식 $f$ 가 주어졌을 때, 식 $f$ 를 true로 만들 수 있는지 없는지를 구하는 프로그램을 작성하시오.
예를 들어, $N = 3$, $M = 4$ 이고, $f = \left( \lnot x_1 \lor x_2 \right) \land \left( \lnot x_2 \lor x_3 \right) \land \left( x_1 \lor x_3 \right) \land \left( x_3 \lor x_2 \right)$ 인 경우에 $x_1$ 을 false, $x_2$ 을 false, $x_3$ 를 true로 정하면 식 $f$ 를 true로 만들 수 있다. 하지만, $N = 1$, $M = 2$ 이고, $f = \left( x_1 \lor x_1 \right) \land \left( \lnot x_1 \lor \lnot x_1 \right)$ 인 경우에는 $x_1$ 에 어떤 값을 넣어도 식 $f$ 를 true로 만들 수 없다.
입력
첫째 줄에 변수의 개수 $N$ $(1 \leq N \leq 10,000)$ 과 절의 개수 $M$ $(1 \leq M \leq 100,000)$ 이 주어진다. 둘째 줄부터 $M$ 개의 줄에는 절이 주어진다. 절은 두 정수 $i$ 와 $j$ $(1 \leq |i|, |j| \leq N)$ 로 이루어져 있으며, $i$ 와 $j$ 가 양수인 경우에는 각각 $x_i$, $x_j$ 를 나타내고, 음수인 경우에는 $\lnot x_{-i}$, $\lnot x_{-j}$ 를 나타낸다.
출력
첫째 줄에 식 $f$ 를 true로 만들 수 있으면 $1$ 을, 없으면 $0$ 을 출력한다.
$f$ 를 true로 만들 수 있는 경우에는 둘째 줄에 식 $f$ 를 true로 만드는 $x_i$ 의 값을 $x_1$ 부터 순서대로 출력한다. true는 $1$, false는 $0$ 으로 출력한다.
풀이과정
1번째 시도
이 문제는 강한 연결 요소 (SCC) 를 이용하여 해결할 수 있는 문제이다. 논리 문제가 왜 갑자기 그래프 문제가 되는 것인가 하면, 어떤 변수와 그의 역을 그래프 정점으로 생각하고, 논리 관계를 간선으로 생각하여 그래프를 구성하면 된다.
SCC들을 모두 알아내게 되면, 어떤 변수라도 그 변수의 역과 같은 SCC안에 포함되면, 해가 존재하지 않고, 포함되면 해가 존재한다.
해가 존재할 때, 구하는 방법은 위상 정렬 순서대로 SCC를 방문하여 먼저 나오는 변수를 거짓으로 할당하면 된다. 이는 앞 변수가 거짓임은 명제를 해치지 않기 때문에 가능한 방법이다. Tarjan 알고리즘은 SCC들을 위상 정렬의 역순으로 알아낼 수 있기 때문에, 역방향으로 탐색하여 알아낼 수 있는 것이다.
나는 이 문제를 해결하기 위해 예전에 풀었던 문제인 Strongly Connected Component 의 코드2를 가져와 수정하였다. 또한 SCC들을 모두 거꾸로 탐색하는 대신, 각 변수들과 역이 속한 SCC의 번호를 비교하는 방식으로 참 거짓 여부를 판별했다.
코드는 다음과 같이 작성하였다.
#include <bits/stdc++.h>
using namespace std;
bool alreadyInGroup[10001] = { 0, };
int result[10001] = { -1, };
int orderOfFound[10001] = { 0, };
int highestReachable[10001] = { 0, };
int numberOfGroup[10001] = { 0, };
int tempOrder = 1;
int numberOfSCCs = 0;
vector<vector<int>> graph(10001);
stack<int> s;
vector<vector<int>> SCCs(10001);
int logicToVertex(int logic);
int vertexToLogic(int vertex);
void tarjan(int nodeToCheck);
bool checkSatisfiability(int N);
void caculateResult(int N);
int main(void) {
ios::sync_with_stdio(0);
cin.tie(0);
cout.tie(0);
int N, M, A, B;
cin >> N >> M;
for (int i = 0; i < M; i++) {
cin >> A >> B;
graph[logicToVertex((-1) * A)].emplace_back(logicToVertex(B));
graph[logicToVertex((-1) * B)].emplace_back(logicToVertex(A));
}
for (int i = 1; i <= 2 * N; i++) {
if (orderOfFound[i] == 0) {
tarjan(i);
}
}
bool satisfiability = checkSatisfiability(N);
if (satisfiability == true) {
cout << 1 << "\n";
caculateResult(N);
for (int i = 1; i <= N; i++) {
cout << result[i] << " ";
}
}
else {
cout << 0;
}
return 0;
}
// 1 2 3 4 5
// original: 1 3 5 7 9
// -1 -2 -3 -4 -5
// inversed: 2 4 6 8 10
int logicToVertex(int logic) {
if (logic < 0) {
return logic * (-2);
}
else {
return 2 * logic - 1;
}
}
int vertexToLogic(int vertex) {
if (vertex % 2 == 0) {
return (-1) * vertex / 2;
}
else {
return (vertex + 1) / 2;
}
}
void tarjan(int nodeToCheck) {
orderOfFound[nodeToCheck] = highestReachable[nodeToCheck] = tempOrder;
tempOrder++;
s.push(nodeToCheck);
for (auto i : graph[nodeToCheck]) {
if (orderOfFound[i] == 0) {
tarjan(i);
highestReachable[nodeToCheck] = min(highestReachable[nodeToCheck], highestReachable[i]);
}
else if (alreadyInGroup[i] == false) {
highestReachable[nodeToCheck] = min(highestReachable[nodeToCheck], orderOfFound[i]);
}
}
if (highestReachable[nodeToCheck] == orderOfFound[nodeToCheck]) {
while (s.top() != nodeToCheck) {
int currentNode = s.top();
s.pop();
alreadyInGroup[currentNode] = true;
SCCs[numberOfSCCs].emplace_back(currentNode);
numberOfGroup[currentNode] = numberOfSCCs;
}
int highestInSCC = s.top();
s.pop();
alreadyInGroup[highestInSCC] = 1;
SCCs[numberOfSCCs].emplace_back(highestInSCC);
numberOfGroup[highestInSCC] = numberOfSCCs;
numberOfSCCs++;
}
}
bool checkSatisfiability(int N) {
for (int i = 1; i <= N; i++) {
if (numberOfGroup[logicToVertex(i)] == numberOfGroup[logicToVertex(-i)]) {
return false;
}
}
return true;
}
void caculateResult(int N) {
for (int i = 1; i <= N; i++) {
result[i] = -1;
}
for (int i = 1; i <= N; i++) {
result[i] = numberOfGroup[logicToVertex(i)] < numberOfGroup[logicToVertex(-i)];
}
}
그러자 ‘런타임 에러 (OutOfBounds)’ 가 발생하였다.
2번째 시도
오류 이름을 보고 3초간 멍하니 있다가, 이내 문제점이 뭔지 바로 이해하게 되었다. OutOfBounds 라는 말은 말 그대로 범위를 벗어났다는 말로, 어떤 논리 변수와 그 역까지 정점으로 삼으면서 필요한 공간의 개수가 2배로 늘어났지만, 코드 상의 변수들의 범위도 더 증가시키는 것을 깜빡했던 것이다.
코드를 다음과 같이 수정하였다.
#include <bits/stdc++.h>
#define MAX_SIZE 20002
using namespace std;
bool alreadyInGroup[MAX_SIZE] = { 0, };
int result[MAX_SIZE] = { -1, };
int orderOfFound[MAX_SIZE] = { 0, };
int highestReachable[MAX_SIZE] = { 0, };
int numberOfGroup[MAX_SIZE] = { 0, };
int tempOrder = 1;
int numberOfSCCs = 0;
vector<vector<int>> graph(MAX_SIZE);
stack<int> s;
vector<vector<int>> SCCs(MAX_SIZE);
int logicToVertex(int logic);
int vertexToLogic(int vertex);
void tarjan(int nodeToCheck);
bool checkSatisfiability(int N);
void caculateResult(int N);
int main(void) {
ios::sync_with_stdio(0);
cin.tie(0);
cout.tie(0);
int N, M, A, B;
cin >> N >> M;
for (int i = 0; i < M; i++) {
cin >> A >> B;
graph[logicToVertex((-1) * A)].emplace_back(logicToVertex(B));
graph[logicToVertex((-1) * B)].emplace_back(logicToVertex(A));
}
for (int i = 1; i <= 2 * N; i++) {
if (orderOfFound[i] == 0) {
tarjan(i);
}
}
bool satisfiability = checkSatisfiability(N);
if (satisfiability == true) {
cout << 1 << "\n";
caculateResult(N);
for (int i = 1; i <= N; i++) {
cout << result[i] << " ";
}
}
else {
cout << 0;
}
return 0;
}
// 1 2 3 4 5
// original: 1 3 5 7 9
// -1 -2 -3 -4 -5
// inversed: 2 4 6 8 10
int logicToVertex(int logic) {
if (logic < 0) {
return logic * (-2);
}
else {
return 2 * logic - 1;
}
}
int vertexToLogic(int vertex) {
if (vertex % 2 == 0) {
return (-1) * vertex / 2;
}
else {
return (vertex + 1) / 2;
}
}
void tarjan(int nodeToCheck) {
orderOfFound[nodeToCheck] = highestReachable[nodeToCheck] = tempOrder;
tempOrder++;
s.push(nodeToCheck);
for (auto i : graph[nodeToCheck]) {
if (orderOfFound[i] == 0) {
tarjan(i);
highestReachable[nodeToCheck] = min(highestReachable[nodeToCheck], highestReachable[i]);
}
else if (alreadyInGroup[i] == false) {
highestReachable[nodeToCheck] = min(highestReachable[nodeToCheck], orderOfFound[i]);
}
}
if (highestReachable[nodeToCheck] == orderOfFound[nodeToCheck]) {
while (s.top() != nodeToCheck) {
int currentNode = s.top();
s.pop();
alreadyInGroup[currentNode] = true;
SCCs[numberOfSCCs].emplace_back(currentNode);
numberOfGroup[currentNode] = numberOfSCCs;
}
int highestInSCC = s.top();
s.pop();
alreadyInGroup[highestInSCC] = 1;
SCCs[numberOfSCCs].emplace_back(highestInSCC);
numberOfGroup[highestInSCC] = numberOfSCCs;
numberOfSCCs++;
}
}
bool checkSatisfiability(int N) {
for (int i = 1; i <= N; i++) {
if (numberOfGroup[logicToVertex(i)] == numberOfGroup[logicToVertex(-i)]) {
return false;
}
}
return true;
}
void caculateResult(int N) {
for (int i = 1; i <= N; i++) {
result[i] = -1;
}
for (int i = 1; i <= N; i++) {
result[i] = numberOfGroup[logicToVertex(i)] < numberOfGroup[logicToVertex(-i)];
}
}
그러자 모든 테스트 케이스를 통과하고 정답이 나오는 것을 확인할 수 있었다.
마무리
세미나에서 배워서 이미 알고는 있었지만, 전혀 관련없어 보이던 2-SAT 문제가 그래프의 SCC를 찾는 문제로 변환될 수 있다는 것이 되게 신기했다. 한편으로는, 혼자서는 이게 그런 식의 변환을 거칠 수 있는 문제인 건지 알아낼 수 있었을까 하는 생각도 든다.
앞으로 다양한 문제를 만나게 되면서 세미나에서 가르쳐주지 않는 문제들도 만나게 될텐데, 그 때마다 이런 창의적이고 신기한 아이디어를 내고, 적용가능성을 증명하고, 코드로 잘 구현해낼 수 있을지 심히 걱정스럽다. 물론 걱정을 한다고 달라질 건 없으니 열심히 문제를 풀어나가는 수 밖에는 없는 것 같다.
오늘의 PS는 여기까지!
1: https://www.acmicpc.net/problem/11281
2: https://github.com/ChoiCube84/baekjoon-solutions/blob/main/C%2B%2B/2150/source.cpp