5. DFS - 회의실 배정(meetingroom) 문제

문제를 해결하기 위해서는 각 팀의 회의들에 대해서 이 회의를 할지, 하지 않을 지를 결정해야 한다.

이렇게 참이냐 거짓이냐의 결정을 여러번 해야하는 문제들을 불린값 만족성 문제(Boolean Satisfiability Problem, SAT) 라고 한다.

SAT 문제는 Boolean 값 변수(A)의 참 형태(A)와 거짓 형태(!A 또는 ~A) 들로 구성된 식이 주어질 때, 

이 식의 값을 참으로 하는 변수의 조합이 있는지 찾는 것이다.

예를 들어,

a && (!b || !a) && (c && (!a || b))

위와 같은 식이 있다고 하자.

그러면 이 전체 식의 결과가 참이 되는 (a,b,c) 의 조합이 있을까?

우선 a는 무조건 참이 되어야 한다.

그러면 (!b || !a) 를 만족하기 위해 b는 거짓이 되어야 한다.

그런데 마지막 (!a || b)의 식이 거짓이 되어버리기 때문에 전체 식을 참을 만드는 값은 존재하지 않는다는 것을 알 수 있다.

이렇게 SAT문제는 전체 논리식이 주어졌을 때 식이 참이 되게하는 변수값들의 참, 거짓 조합을 만드는 것이다.

위 문제에서 각 팀당 두개의 회의 시간이 주어지게 된다.

각 회의에 0부터 2n-1까지 번호를 매긴 뒤, i번 회의를 할 것인지의 여부를 boolean값 변수 Ai 로 나타내도록 한다.

그러면 문제의 요구조건을 논리식으로 어떻게 나타낼 수 있을까?

우선 각 팀당 두번의 회의 중 하나의 회의만 선택해서 진행해야한다는 조건을 보자.

각 팀은 둘 중 한 회의를 꼭 해야한다.

그러면 i번 팀의 두번의 회의는 2i, 2i+1번 회의이기 때문에 해당 요구 조건을

( A2i || A(2i+1))

이런 논리식으로 나타낼 수 있다.

그리고 시간이 겹치는 두 회의는 동시에 진행할 수 없다는 조건을 보자.

즉, 두 회의 중 최소한 하나는 무조건 진행되지 않아야 한다.

만약 시간이 겹치는 두 회의의 번호를 a, b 라고 할 때 해당 요구 조건을

( !Aa || !Ab)

이런 논리식으로 나타낼 수 있다.

이러한 방식을 통해 각 회의들에 대해 논리식을 만들어 && 연산자로 묶으면 전체 논리식이 된다.

예제가 위와 같이 주어졌을 때 논리식을 위와 같이 만들 수 있다.

위의 논리식은 각 변수들의 참 형태나 거짓 형태가 || 연산자로 연결된 수식들이 모여 구성된다.

이러한 괄호 안에 들어있는 수식들을 절이라고 한다.

각 절들은 모두 && 연산자로 연결되어 있는데, 이러한 형태를 논리곱 정규형이라고 부른다.

논리식을 논리곱 정규형으로 표현했을 때, 각 절에 포함된 변수가 최대 2개인 경우 이 SAT 문제를 특별히 2-SAT 문제라고 부른다.

2-SAT 문제는 그래프를 이용해 다항 시간에 해결할 수 있다.

변수 함의 그래프의 생성

문제를 그래프로 해결하기 위해서 우선 주어진 문제를 그래프로 표현해야 한다.

2-SAT 문제에서 논리식의 각 절은 두개의 변수로 구성되어 있고, 모든 절은 참이어야 한다.

즉, 절을 구성하는 두 변수중 최소 하나는 반드시 참이어야 한다.

예를 들어 논리식에 (A0 || A1) 절이 포함되어 있다고 하자.

그러면 A0가 참이거나 A1이 참이어야 한다.

즉, 0번 회의가 진행되지 않는다면 1번 회의는 반드시 진행되어야 하고, 

반대로 1번 회의가 진행되지 않는다면 0번 회의는 반드시 진행되어야 한다.

이를 'P이면 Q이다' 형태의 필요조건과 충분조건의 형태로 나타내 보자.

0번 회의가 진행되지 않는다.(!A0) => 1번 회의가 진행된다.(A1)

1번 회의가 진행되지 않는다.(!A1) => 0번 회의가 진행된다.(A0)

이렇게 나타낸 조건을 그래프로 그대로 옮길 수 있다.

논리식의 각 변수 Ai 에 대해 Ai 와 !Ai 를 포현하는 두개의 정점을 포함하는 방향 그래프를 만들고, 

각 절마다 위의 조건을 나타낸 것처럼 방향 간선을 추가한다.

즉 위의 조건을 그래프로 나타내면,

!A0 정점에서 A1 정점으로 향하는 간선을 추가하고,

!A1 정점에서 A0 정점으로 향하는 간선을 추가한다.

이 그래프 상에서 정점 P에서 정점 Q로 가는 경로는 P가 표현하는 식이 참일 때 Q가 표현하는 식 또한 무조건 참이어야 한다는 의미를 갖는다.

(P가 표현하는 식이 거짓일 때는 Q가 표현하는 식이 어떤 값을 갖든지 상관없다.)

이렇게 논리식에 포함된 변수들의 값에 대한 요구조건을 표현한 그래프를 함의 그래프(implication graph) 라고 한다.

해당 문제에서 그래프를 만들어 보도록하자.

문제에서 n개의 팀이 있다고 할 때, 회의는 2n개가 존재할 것이고, 각 회의가 열리는지 열리지 않는지를 나타내는 정점은 4n개가 될 것이다.

이 때 회의가 열린다는 것을 표현하는 Ai는 2i번 정점, 회의가 열리지 않는다는 것을 표현하는 !Ai는 2i+1번 정점이 될 것이다.

// 회의 시간으로부터 2-SAT 문제의 함의 그래프 만들기

vector< vector<int> > adj;  // 그래프의 인접리스트

// 두 개의 회의 시간이 서로 겹치지 않는지 확인한다.

bool disjoint(const pair<int, int>& a, const pair<int, int>& b){

return (a.second <= b.first) || (b.second <= a.first);

}

void makeGraph(const vector< pair<int, int> >& meetings){

adj.clear();

adj.resize(meetings.size() * 2);

// 각 팀은 주중회의(i번 회의)나 월말회의(j번 회의) 중 하나의 회의를 무조건 진행해야 한다.

for(int i = 0; i < meetings.size(); i+=2){

int j = i + 1;

adj[i * 2 + 1].push_back(j * 2);  // ~i => j

adj[j * 2 + 1].push_back(i * 2);  // ~j => i

}

// 시간이 겹치는 두 회의가 있다면 둘 중 최소 하나는 진행하면 안된다.

for(int i = 0; i < meetings.size(); i++){

for(int j = i + 1; j < meetings.size(); j++){

if( !disjoint(meetings[i], meetings[j]) ){

adj[i * 2].push_back(j * 2 + 1);  // i => ~j

adj[j * 2].push_back(i * 2 + 1);  // j => ~i

}

}

}

}

함의 그래프를 이용해 2-SAT 문제 풀기

함의 그래프로 문제의 조건을 표현했으면, 이 그래프를 이용해 문제를 해결할 차례이다.

함의 그래프에서 간선 P=>Q 는 요구조건 'P이면 Q이다' 를 나타낸다.

만약 P가 참인데 Q가 거짓이라면 이 요구조건이 만족되지 않았으므로 문제의 답이 될 수 없다는 의미이다.

따라서 다음과 같은 두가지 조건을 만족하도록 그래프의 정점을 분류하는 것이 2-SAT 문제를 해결하는 것과 같다는 것을 알 수 있다.

1. 각 정점 쌍 Ai와 !Ai 중 하나는 참 정점, 하나는 거짓 정점으로 분류된다.

2. 참 정점에서 거짓 정점으로 가는 경로는 없다.

이러한 조건을 만족하는 분류를 찾을 때, 답이 존재하지 않는 대표적인 예가 바로

한 변수를 표현하는 두 정점이 하나의 사이클에 포함되어 있는 경우이다.

어떤 사이클이 A0와 !A0를 모두 포함한다고 했을 때, A0와 !A0는 둘 중 하나는 참, 하나는 거짓이어야 하는데

그러면 참 정점에서 거짓 정점으로 향하는 경로가 생겨버리게 된다.

여기서 우리는 하나의 사이클에 속하는 모든 정점들은 모두 참이거나 모두 거짓이어야 한다는 것을 알 수 있다.

따라서 한 사이클에 존재하는 정점들을 한 묶음으로 처리할 수 있다.

하나의 정점을 참 정점 혹은 거짓 정점으로 분류하고 나면 해당 정점과 같은 사이클에 포함되는 모든 정점들을 같은 분류로 분류할 수 있다.

그러면 그래프의 각 정점을 분류하는 문제에서 사이클 별로 분류하는 문제로 바뀌었다.

그런데 방향 그래프에서 사이클을 분류하는 것은 바로 SCC를 분류하는 것과 같다.

그러면 우리는 그래프를 SCC로 압축하여 만든 DAG의 각 정점을 참 정점 또는 거짓 정점으로 분류하는 작업을 진행하면 된다.

DAG의 각 정점을 분류하는 방법은 간단하다.

들어오는 간선이 하나도 없는 정점을 고르고, 이 정점은 거짓 정점으로 분류한다.

어차피 이 정점으로 들어오는 간선이 하나도 없기 때문에

참 정점에서 거짓 정점으로 향하는 경로가 있으면 안된다는 조건에 위배될 일이 없기 때문이다.

이 정점을 거짓 정점으로 분류한다면, 이 정점 즉 이 SCC에 포함된 정점들의 반대 정점이 모여있는 SCC는 참 정점이 된다.

이러한 과정을 모든 정점이 분류될때까지 반복하면 문제의 정답을 찾아낼 수 있다.

이 때 들어오는 간선이 없는 정점을 선택하면서 과정을 반복하는 것보다 그래프의 위상 정렬 순서대로 처리하는 것이 더 간단하다.

즉, 타잔 알고리즘의 결과를 역순으로 뒤집었을 때의 순서로 정점을 분류할 때, 

A 정점과 !A 정점 중 먼저 발견된 정점이 거짓 정점이 되고, 나중에 발견된 정점이 참 정점이 된다.

// 2-SAT 문제 해결하는 알고리즘

vector<int> solve2SAT(){

int n = adj.size() / 2;

// 함의 그래프의 정점들을 SCC로 묶는다.

vector<int> label = tarjanSCC();

// 만약 한 변수를 나타내는 두 정점이 같은 SCC에 속해있다면 답은 존재하지 않는다.

for(int i = 0; i < 2 * n; i += 2){

if(label[i] == label[i +1]) return vector<int>();

}

vector<int> value(n, -1);

// 타잔 알고리즘의 결과 SCC 번호는 그래프의 위상 정렬의 역순이기 때문에

// SCC 번호의 역순으로 정점을 분류하면 된다.

vector< pair<int, int> > order;

for(int i = 0; i < 2 * n; i++){

order.push_back(make_pair(-label[i], i));

}

sort(order.begin(), order.end());  // SCC번호의 음수값을 기준으로 정렬된다.(위상 정렬 순서로 정렬)

for(int i = 0; i < 2 * n; i++){

int vertex = order[i].second;

int variable = vertex / 2;  // 2i번 정점과 2i+1번 정점은 i번회의에 대한 두가지 상태

int isTrue = vertex % 2;  // 먼저 발견된 것이 2i+1번 정점(~i 정점)이면 ~i가 거짓이므로 i는 참이 된다. ( (2i+1) % 2 = 1)

if(value[variable] != -1) continue;  // 이미 해당 정점을 분류했다면 넘어감

value[variable] = !isTrue;

}

return value;

}