2-SAT 연구일지
2-SAT에 대하여 공부해봅시다.
2-Satisfiability의 약자로 boolean variable들의 충족 가능성을 묻는 문제입니다.
BOJ 2-SAT 3(11280), 2-SAT 4(11281)를 기반으로 연구합니다.
공부하는 데에 도움이 된 블로그 링크들
1(https://blog.naver.com/kks227/220803009418)
2(https://everenew.tistory.com/140)
22.04.03 연구일지
CNF(Conjunctive Normal Form) 식을 true가 될 수 있게 boolean variable의 조합이 있는지 조합이 있다면 어떤 조합으로 이루어지는지 알아내는 알고리즘입니다.
2-SAT에서 CNF는 2-CNF로 이는 한 Clause당 boolean variable이 최대 2개가 있다는 뜻입니다.
한 Clause안에서 boolean variable들끼리는 OR연산(논리합)이 되어있으며 Clause끼리는 AND연산(논리곱)으로 이루어집니다.
f = (x1 | ~x2) & (x2 | ~x3) & (x3 | ~x1) & (~x4 | ~x2)
&연산에 의해 모든 Clause는 true값을 내놓아야 합니다.
즉, 2-SAT 문제는 각 Clause의 변수들 중 적어도 하나가 true가 되게 하는 것이 문제를 푸는 방향이 됩니다.
OR이 true가 되는 조건은
1) x1 = true, x2 = true
2) x1 = true, x2 = false
3) x1 = false, x2 = true
가 있습니다.
두 variable 중에 적어도 하나만 true를 내놓는다면?
논리합이기 때문에 두 변수 모두 다 true가 아니어도 됩니다.
즉, 이렇게 정리할 수 있습니다.
✔️2-SAT 핵심 아이디어(1): 각 Clause에서 true를 내놓으려면?
~x1 -> x2: x1이 false라면, x2가 true여야 한다.
~x2 -> x1: x2가 false라면, x1이 true여야 한다.
+ 논리학(Logics)에서도 위 내용은 논리적 동치라고 나와있습니다.
(p V q) ≡ (~ p -> q)
+ (p V q)는 교환 법칙이 성립함으로 (~q -> p)를 도출할 수 있습니다.
그러면 아까 위의 식에서 다음 true propostion 조건문들을 도출할 수 있습니다.
~x1 -> ~x2
x2 -> x1
~x2 -> ~x3
x3 -> x2
~x3 -> ~x1
x1 -> x3
x4 -> ~x2
x2 -> ~x4
이들을 삼단논법을 이용해서 추론하여 그래프로 나타낼 수 있습니다.
다음과 같이 그래프로 나타내면 SCC가 형성되어있는 것을 확인할 수 있습니다.
모순
✔️2-SAT 핵심 아이디어(2): 2-SAT이 성립하지 않는 순간, 모순
위 그림에는 없지만 추론하는 과정에서 같은 SCC안에 ~p와 p가 같이 들어있다면, 이건 모순을 의미합니다.
같은 SCC안에 들어있다는 것은 함축하였을 때, ~p -> p와 p -> ~p임을 의미하기 때문입니다.
둘 중 하나의 명제가 좌변이 false이고, 우변이 true라면 이는 성립하겠지만 그 반대는 성립하지 않기 때문에 모순입니다.
>> 이와 관련에서 무슨 말인지 밑에서 다루겠습니다. (명제 논리, 조건문)
즉, 모순이 없다면 식 f에서 true값을 가져올 수 있는 boolean variable의 조합이 있다는 뜻입니다.
명제 논리, 조건문
✔️2-SAT 핵심 아이디어(3): 명제 논리에 따른 조건문이 참 혹은 거짓이 되는 경우
명제 논리에 따르면 조건문은 아래 표와 같은 경우에서 참임을 의미합니다.
| p | q | p -> q |
| T | F | F |
| F | F | T |
| T | T | T |
| F | T | T |
p가 참일 때, q가 거짓인 경우를 제외하면 모든 경우에서 참입니다.
>> 즉, SCC를 구성하는 노드 중 하나라도 참이 있다면 해당 SCC는 모두 참이어야 합니다.
여기까지의 지식을 가지고서 2-SAT을 만족하는 조합이 있는지 없는지를 찾을 수 있습니다.
이를 코드로 표현하기 위해 모델링하려면
- 각 Clause에서 두 가지 명제를 도출해낸다.
- 도출해낸 명제들을 가지고, 그래프를 만든다.
- 그래프에서 SCC를 구하고, 어떤 한 변수와 그 변수의 NOT 변수가 같은 SCC에 없다면 이는 성립함을 의미한다.
여기까지의 지식을 가지고서 2-SAT 3 (11280)을 풀 수 있습니다.
+변수에 대해서 변수 그 자체는 2를 곱하여 짝수로 나타내고, NOT 변수는 2를 곱하여 1을 더해주었습니다.
#include <iostream>
#include <vector>
#include <stack>
#include <algorithm>
#define MAX 20002
using namespace std;
vector<vector<int>> SCC;
vector<int> adj[MAX];
int visitedOrder[MAX];
int sccNum[MAX];
stack<int> s;
int order = 0, sccCnt = 0;
int n, m;
int dfs(int now){
int parent = visitedOrder[now] = ++order;
s.push(now);
for(int i = 0; i < adj[now].size(); i++){
int next = adj[now][i];
if(visitedOrder[next] == -1){
parent = min(parent, dfs(next));
}
else if(sccNum[next] == -1){
parent = min(parent, visitedOrder[next]);
}
}
if(visitedOrder[now] == parent){
vector<int> scc;
while(1){
int temp = s.top(); s.pop();
scc.push_back(temp);
sccNum[temp] = sccCnt;
if(temp == now) break;
}
SCC.push_back(scc);
sccCnt++;
}
return parent;
}
void tarjan(){
fill(visitedOrder, visitedOrder + MAX, -1);
fill(sccNum, sccNum + MAX, -1);
for(int i = 2; i <= 2 * n + 1; i++){
if(visitedOrder[i] == -1) dfs(i);
}
}
int main(){
cin >> n >> m;
for(int i = 0; i < m; i++){
int a, b; cin >> a >> b;
//a = 2 * i, NOT a = 2 * i + 1
// 2가지 명제 도출 과정
int not_a, not_b;
if(a < 0){ // NOT
a = -a;
a *= 2; a++;
not_a = a - 1;
}
else{
a *= 2;
not_a = a + 1;
}
if(b < 0){
b = -b;
b *= 2; b++;
not_b = b - 1;
}
else{
b *= 2;
not_b = b + 1;
}
// 그래프 만들기
adj[not_a].push_back(b);
adj[not_b].push_back(a);
}
tarjan();
// 모순이 있는지 확인
bool flag = 1;
for(int i = 2; i <= 2 * n; i += 2){
if(sccNum[i] == sccNum[i + 1]){
flag = 0; break;
}
}
if(flag == 1) cout << 1;
else cout << 0;
return 0;
}여기까지 2-SAT이 성립하는지에 대하여 알아보았습니다.
✔️2-SAT 핵심 아이디어(4): 2-SAT이 성립한다면 변수들은 어떤 값인지 알 수 있을까?
만약 2-SAT이 성립한다면 각 boolean variable들은 어떤 값을 가져야 할까요?
위에서 말했듯이 SCC를 구성하는 변수들은 모두 같은 값을 가져야 합니다.
그렇게 되면 SCC를 노드 단위로 보면 됩니다.
아까 위의 그림을 다시 가져와서 보면, {x4} -> {~x1, ~x2, ~x3}로 가고 있습니다.
| p | q | p -> q |
| T | F | F |
| F | F | T |
| T | T | T |
| F | T | T |
이 표에 의거하여 x4를 false로 두는 것이 명제를 해치지 않기 때문에 좋습니다.
즉, 위상 정렬을 통해 처음 방문한 값들을 false로 두는 것이 좋습니다. ~x4도 indegree가 없기 때문에 ~x4를 false로 두어도 됩니다.
>> 변수 혹은 not 변수 중 먼저 방문하는 순서대로 false를 준다는 뜻입니다.
✔️2-SAT 핵심 아이디어(5): 위상 정렬을 통한 SCC끼리의 조건문
위상 정렬을 확인하는 방법은 Tarjan Algorithm의 특성으로 만들어진 순서를 반대로 뒤집으면 위상 정렬이 됩니다.
즉, SCC에 생긴 순서대로 번호를 매기고, 이를 내림차순으로 정렬하면 됩니다.
>> 이 아이디어에서 좀 놀랬습니다..
왜 위상 정렬이 되는지는 자세한 내용은 Tarjan Algortihm 연구일지를 참고하길 바랍니다.
(https://draw-code-boy.tistory.com/274)
+ 예를 들어, ~x1 -> x1의 경로가 있다면 이는 상관없습니다. 이미 ~x1을 방문하면서 ~x1은 false가 되었고, x1은 true가 되었기 때문입니다.
여기까지 내용을 인지하고, 코드로 모델링한다면
- 각 Clause에서 두 가지 명제를 도출해낸다.
- 도출해낸 명제들을 가지고, 그래프를 만든다.
- 그래프에서 SCC를 구하고, 어떤 한 변수와 그 변수의 NOT 변수가 같은 SCC에 없다면 이는 성립함을 의미한다.
- 성립한다면 각 변수가 어떤 값을 지니는지 알 수 있다.
- 각 SCC를 하나의 노드로 보고, 위상 정렬에 의해 제일 늦게 만들어진 SCC를 순서로 노드를 방문하여 만나는 변수에 false값을 준다.
여기까지의 지식을 가지고서 2-SAT 4 (11281)을 풀 수 있습니다.
#include <iostream>
#include <vector>
#include <algorithm>
#include <stack>
#define MAX 20002
#define pii pair<int, int>
using namespace std;
vector<vector<int>> SCC;
vector<int> adj[MAX];
stack<int> s;
int visitedOrder[MAX];
int sccNum[MAX];
int order = 0, sccCnt = 0;
int n, m;
bool cmp(pii a, pii b){
return a.second > b.second;
}
int dfs(int now){
int minOrder = visitedOrder[now] = ++order;
s.push(now);
for(int i = 0; i < adj[now].size(); i++){
int next = adj[now][i];
if(visitedOrder[next] == -1){
minOrder = min(minOrder , dfs(next));
}
else if(sccNum[next] == -1){
minOrder = min(minOrder, visitedOrder[next]);
}
}
if(visitedOrder[now] == minOrder){
vector<int> scc;
while(true){
int temp = s.top(); s.pop();
sccNum[temp] = sccCnt;
scc.push_back(temp);
if(temp == now) break;
}
SCC.push_back(scc);
sccCnt++;
}
return minOrder;
}
void tarjan(){
fill(visitedOrder, visitedOrder + MAX, -1);
fill(sccNum, sccNum + MAX, -1);
for(int i = 2; i <= 2 * n + 1; i++){
if(visitedOrder[i] == -1) dfs(i);
}
}
int main(){
cin >> n >> m;
for(int i = 0; i < m; i++){
int a, b; cin >> a >> b;
int not_a, not_b;
if(a < 0){
a = -a; a *= 2; a += 1;
not_a = a - 1;
}
else{
a *= 2;
not_a = a + 1;
}
if(b < 0){
b = -b; b *= 2; b += 1;
not_b = b - 1;
}
else{
b *= 2;
not_b = b + 1;
}
adj[not_a].push_back(b);
adj[not_b].push_back(a);
}
tarjan();
bool flag = 1;
for(int i = 2; i <= 2 * n; i += 2){
if(sccNum[i] == sccNum[i + 1]){
flag = 0; break;
}
}
if(flag){
cout << 1 << '\n';
vector<pii> satOrder;
for(int i = 2; i <= 2 * n + 1; ++i){
//{vertex || ~vertex, vertex's SCCnum}
satOrder.push_back({i, sccNum[i]});
}
// SCC가 만들어진 순서를 내림차순으로 정렬해주었다.
sort(satOrder.begin(), satOrder.end(), cmp);
vector<int> answer(n + 1, -1);
for(int i = 0; i < satOrder.size(); i++){
int vertex = satOrder[i].first;
int varIdx = vertex / 2;
int isTrue = (vertex % 2 == 0);
if(answer[varIdx] != -1) continue;
// 처음 방문하는 변수에 true이면 false, false이면 true를 준다.
answer[varIdx] = !isTrue;
}
for(int i = 1; i < answer.size(); i++){
cout << answer[i] << ' ';
}
}
else{
cout << 0 << '\n';
}
return 0;
}결론
여태껏 그래프 알고리즘만 공부하다가 논리학에 관련된 알고리즘을 공부하다 보니 시간을 들여야 했습니다. 물론, SCC를 활용하여 그래프 알고리즘이기도 하지만. 다른 영역의 알고리즘을 건드려야겠다는 생각이 부쩍 들었었는데 한 걸음 나아간 것 같습니다.
그리고, 반년 전쯤 알고리즘을 막 시작할 때, '2-SAT'이라는 이름이 멋져 보여서 저런 알고리즘은 엄청 어려울 거 같아서 언젠간 배우고 싶었는데 SCC를 공부하다 보니 자연스럽게 2-SAT을 건드리게 되어 기분이 오묘한 순간이었습니다.
아직은 미숙지 된 내용들에 대해 계속 추가적으로 수정하거나 구현을 해보며 익혀야겠습니다.