[그래프] [2-SAT] [시도 x] MEETINGROOM 회의실 배정

1. 회의실 배정 문제

 

이 문제는 

 

n개의 팀이 회의를 할 수 있는 두 시간 범위가 주어지고

 

두 시간중 한 타임을 선택하여

 

모든 팀이 회의를 할 수 있게하는 문제이다.

 

2. 그래프 만들기?

 

그래프의 정점들은 각 시간의 첫부분과 끝부분이어야 할 것 같다.

 

그러면 간선은 회의를 하는 시간을 표현해야할 꺼 같다.

 

 

각 회의 구간은 겹칠수 있다.

A     ->    B 

A->a->b->B

   C -> D

 

위와 같은 다양한 경우가 존재할 수 있다.

 

어떻게 그래프를 표현해야할까

 

인접행렬로 표현할 시 시간의 범위가 43200이므로 

 

메모리가 432000*432000로 1억이 넘어가므로 이건 아닌거 같다.

 

 

인접리스트로 각 시간을 담는것도 조금 무리인것 같지만 행렬보다는 아니다.

 

 

 

시간을 겹치는 것끼리 같은 그룹으로 묶어서 압축을 시키면 어떨까?

 

그러면 겹치는 것중에서 하나를 선택한 뒤 뒤에 이어지는 시간대의 그룹에서 선택하며 

 

나아가며 될것 같다.

 

하지만 이것 또한 문제인게 A와 C, A와 B는 겹치지만 C와 B가 겹치지 않는 경우가 있다.

 

 

책은 어떻게 풀었을까??

 

마음과 같아선 그냥 2^100 조합탐색을 하고 싶어지는 문제이다.

 

 

3. 책의 풀이: SAT문제

 

이런 선택을 여러번 해야하는 문제들을 불린 값 만족성 문제(Boolean satisfiability problem, SAT) 라고 부른다,

 

SAT문제는 불린값 변수의 참 형태와 거짓 형태들로 구성된 식이 주어질 때,

 

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

 

ex) a&&(!b||!a)&&(c&&(!a||b)) 같은 식을 참으로 만드는 a b c를 구하는 것 = > 조합은 없다....(c||(a!||b)) 이면 참

 

 

 

SAT문제는 엄청나게 일반적이고 강력한 문제이다.

 

다항 시간에 풀 수 있는 모든 문제들은 SAT문제로 바꿔서 풀 수 있을 정도이다.

 

하지만 SAT문제를 빠르게 푸는 방법이 아직은 없다.

 

가장 빠른 풀이는 입력 크기의 지수에 비례하는 시간이 걸린다.

 

 

 

4. 논리곱 정규형(conjunctive normalform) => 2-SAT

 

우선 입력에 주어지는 모든 회의에 0 부터 2n-1까지의 번호를 매긴 뒤

 

i번회의를 할 것인지의 여부를 불린 값 변수 Ai로 나타내보자

 

그러면 문제를 다음과 같이 나타낼 수 있다.

 

 

- 각 팀의 주간 회의 와 월간 회의 중 하나는 꼭해야한다. 주간: 2t 월간 2t+1

  모든 t에 대해 (A2t | | A2t+1) 이 참이여야한다.

 

- 서로 겹치는 두 회의 a, b 최소한 하나는 개최되지 않아야한다.

  (!Aa || !Ab) 이 참이여아한다

 

 

 

이들을 모두 && 연산자로 묶으면 문제를 풀 논리식을 얻을 수 있다.

 

3 2 5 6 9 1 3 8 10 4 7 11 12

예제 입력데이터가 위와 같을 때 논리식은 다음과 같다

 

(A0 || A1) && (A2|| A3) && (A4 || A5) 

&& (!A0 || !A2) && (!A1 || !A3) && (!A0 || !A4) && (!A1 || !A4)

 

이 식은 특수한 구조를 띠고 있다.

 

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

 

괄호 안에 들어있는 이 수식들을 절(clause)이라고 부르며

 

각 절들은 모두 && 연산자로 연결되어 있다.

 

이런 형태를 논리곱 정규형이라고 부른다.

 

어떤 논리식도 적절한 전개 과정을 거치면 이형태로 표현할 수 있다.

 

 

논리식을 논리곱 정규형으로 표현했을 때 

 

각 절에 최대 두 개의 변수만이 존재하는 경우의 SAT문제를

 

2-SAT라고 부른다.

 

 

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

 

 

 

5. 변수 함의 그래프의 생성(implication graph)

 

두개의 변수로 구성되어 있다는 점을 이용한다.

 

논리식이 참이 되기 위해서는 모든 절이 참이어야한다.

 

이때 한 절이 참이되려면 절을 구성하는 두 변수 중 반드시 하나는 참이어야 한다.

 

이는 수학의 논리학 에서 필요조건과 충분조건이라 부른다

 

 

!A0 -> A1

!A1 -> A0

 

==

 

~i => j

~j => i

 

i => ~j

j => ~i

 

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

 

각 절마다 위의 표기에 따라 방향 간선을 추가하면 그래프가 완성된다

 

이와 같이 논리식에 포함된 변수들의 값에 대한 요구 조건을 표현한 그래프를 함의 그래프라고 한다.

 

 

이 그래프는

 

2n개의 변수에 각각 ! 이 붙은개 있으므로 총 4n개의 정점을 가지게 된다

 

번호는 다음 순서와 같이 매겨진다

 

A0 !A0 A1 !A1 A2 !A2.....

 

 

 

코드는 다음과 같다.

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)
{
    int vars = meetings.size();
    adj.clear(); 
    adj.resize(vars * 2);
    for(int i = 0 ; i < vars; i += 2) 
    {
        int j = i + 1;
        adj[i*2 + 1].push_back(j*2);
        adj[j*2 + 1].push_back(i*2);
    }
    for(int i = 0 ; i < vars; i++)
    {
        for(int j = 0 ; j < i; j++)
        {
            if(!disjoint(meetings[i], meetings[j]))
            {
                adj[i*2].push_back(j*2 + 1);
                adj[j*2].push_back(i*2 + 1);
            }
        }
    }
}

 

 

6. 함의 그래프를 이용해 2-SAT 풀기

 

A0 A3 A4 는 거짓 A1 A2 A5는 참

 

위에서 생성한 함의 그래프에서

 

2-SAT 문제의 답이 어떻게 표현되는지 봐보자

 

 

각 불린 값 변수의 값을 알고 있을 경우. 

 

그래프의 정점을 참 정점과 거짓정점으로 분류할 수 있다.

 

 

어떤 논리식 (X || Y) 가 거짓이라면 어떻게 될까?

 

일단 이 논리식은 두개의 간선으로 표현된다

 

!X => Y

!Y => X

 

두 변수가 모두 거짓이므로

 

이 간선들은 모두 참 정점에서 거짓 정점으로 가는 것이다.

 

 

 

p=>q  는 p이면 q이다 형태의 요구 조건을 나타낸다.

 

따라서

 

p가 참인데 q가 거짓이라면 이 요구 조건이 만족되지 않은 것이다.

 

 

 

그러므로 다음과 같은 두 가지 조건을 만족하도록 그래프의 정점을 분류하는 것은 답을 찾는것과 동일하다

 

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

 

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

 

 

 

모든 함의 그래프가 이 조건들을 만족하는 분류가 존재하는 것은 아니다.

 

답이 존재하지 않는 함의 그래프의 간단한 예로,

 

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

 

어떤 함의 그래프에 다음과 같은 간선들로 구성된 사이클이 존재한다고하자

 

A0 => !A1 => A2 => !A0 => A1 => !A2 => A0

 

이 사이클은 A0 에서 !A0으로 가는 경로와 !A0에서 A0로 가는 경로를 모두 포함한다.

 

이 두 정점 중 하나는 참. 나머지는 거짓이어야하는데,

 

어느 쪽이 참이든 간에 결과적으로는 참에서 거짓으로 가는 간선이 생기게된다.

 

따라서 이 논리식을 만족하는 변수 조합은 존재하지 않는다.

 

 

 

반대로 어떤 변수에 대해서도 그를 표현하는 두 정점이 한 사이클에 속해 있지 않은 경우는 

 

항상 답을 찾아낼 수 있는 알고리즘을 설계함으로써 이 경우 답의 존재성을 증명할 수 있다.

 

 

 

 

7. 강결합 컴포넌트 이용하기

 

 

 

 

 

앞에서 답이 존재하지 않는 궁극적인 이유는 항상 한 사이클에 참 정점과 거짓 정점이 모두 포함되기 때문이다.

 

한 사이클에 속하는 정점들은 모두 참 정점이거나, 모두 거짓정점이어야 함을 깨달을 수 있다.

 

그렇지 않으면 항상 참 정점에서 거짓 정점으로 가는 간선이 생기기 때문이다.

 

 

 

따라서 한 사이클에 속해 있는 정점들을 한 묶음으로 처리해야한다.

 

한 정점을 참 정점 혹은 거짓 정점으로 분류하고 나면,

 

해당 정점과 같은 사이클에 들어 있는 정점들은 바로 같은 분류에 넣는다.

 

참과 거짓을 결정하는 최소 단위를 정점 대신 사이클로 바꾸는 것이다.

 

 

 

문제는 한 정점이 둘 이상의 사이클에 속해 있을 수도 있다는 것이다.

 

정점을 공유하는 사이클 들을 모두 묶으면 하나의 scc가 된다.

 

두 사이클이 한 정점 x를 공유한다면 두사이클은 정점 x를 통해 오갈 수 있기 때문에 상관이 없다,

 

 

 

이제 scc단위로 문제를 풀 수 있다.

 

scc를 이루는 정점들의 반대 정점들을 모아 보면 이들도 하나의 scc를 이루고 있다.

 

이것은 함의 그래프를 만들 때 각 절을 두 개의 간선으로 표현했기 때문에 나타나는 현상이다.

(X | | Y) 을 다음과 같이간선 두개로 표현했다.   1. !X => Y 2. !Y => X   여기서 1번 간선이 연결하는 두 정점의 반대 정점을 찾으면 이들은 2번 간선에 의해 반대 방향으로 연결되어 있는것을 볼수 있다.

 

이와 같은 속성 때문에 X=>Y=>Z=>X 형태의 사이클이 존재한다면

!X => !Z => !Y => !X 형태의 사이클 또한 반드시 존재하게 된다.

그러므로 SCC들 간에도 원래의 함의 그래프와 같은 1:1대응 관계가 존재하고,

 

한 SCC가 참이라면 그의 반대 SCC는 항상 거짓이어야 함을 알 수 있다.

 

 

 

 

8. 압축된 함의 그래프: DAG

 

결과적으로 이제는 원래 그래프의 정점들을 scc별로 압축한 그래프를 또하나의 함의 그래프를 보고 문제를 풀어도 된다.

 

그리고 이 압축된 함의 그래프는 DAG 이다.

 

 

 

DAG인 함의 그래프에 대해 2-SAT 문제를 푸는 알고리즘은 아주 간단하다.

 

들어오는 간선이 하나도 없는 정점을 하나 고르고

(DAG에는 항상 이런 정점이 존재한다)

 

이 정점을 거짓 정점으로 분류한다

(거짓 정점을 해서 잃는 게 없다.= 참에서 거짓으로 가는 경우가 생기지 않음)

 

이 정점에 대응되는 반대 정점을 참으로 분류하고 그래프에서 거짓 정점을 지워 버린다.

 

그리고 모든 정점이 분류 될때까지 반복한다.

 

들어오는 간선이 없는 정점이 이미 참으로 분류됬으면 그냥 그 정점을 지운다.

 

 

 

위와 같은 과정은 항상 2-SAT 문제의 정답을 찾아낸다.

 

이는 귀류법으로 증명할 수 있다.

 

 

 

 

9. 귀류법: DAG 2-SAT 증명

 

위 알고리즘을 수행했는데. 

 

참 정점 x에서 거짓 정점 y로 가는 간선이 있었다고 가정해보자

 

그래프의 속성에 의해 간선 x=>y 가 있다면 간선 !y => !x 또한 있다.

 

x는 참, y는 거짓이니 !Y는 참. !X는 거짓이 된다.

 

위의 알고리즘은 한쌍의 정점 중 항상 거짓 정점을 먼저 지운다.

 

그러므로 이런 경우는 존재하지 않는다

 

 

X=>Y 간선이 있으니

 

X는 Y보다 먼저 지워져야하지만 X 는 참이다.

 

그래서 !X 가 먼저 거짓 정점으로 분류되어 지어져야 한다.

 

한편 !Y=>!X가 있으므로 !Y는 !X보다 먼저 지워져야 하는데

 

!Y는 참정점이므로 그 전에 Y가 지워져야한다.

 

 

이 조건들을 모두 만족하는 순서란 있을 수 없으므로 애초에 가정이 모순이 되며,

 

이와 같은 그래프가 존재할 수 없음을 알게 된다.

 

 

10. 구현

 

들어오는 간선이 없는 정점을 선택해 반복적으로 삭제하는 대신,

 

압축된 그래프를 위상 정렬한 순서대로 처리하는 것이다.

 

 

여기에 타잔의 강결합 컴포넌트 분리 알고리즘이

 

각 컴포넌트를 위상 정렬의 역순으로 번호를 매긴다는 특성을 이용하면

 

실제 압축을 구현하지 않고도 2-SAT문제의 답을 계산할 수 있다.

(각 정점을 컴포넌트 번호의 역순으로 순회하면서 해당하는 변수에 값을 배정)

 

 

vector<vector<int> > adj;
vector<int> sccId;
vector<int> discovered;
stack<int> st;
 
int sccCounter, vertexCounter;
 
int scc(int here)
{
    int ret = discovered[here] = vertexCounter++;
    st.push(here);
    for(int i = 0; i < adj[here].size(); i++)
    {
        int there = adj[here][i];
        if(discovered[there] == -1)
            ret = min(ret, scc(there));
        else if(sccId[there] == -1)
            ret = min(ret, discovered[there]);
    }
    if(ret == discovered[here]) 
    {
        while(true) 
        {
            int t = st.top();
            st.pop();
            sccId[t] = sccCounter;
            if(t == here) break;
        }
        ++sccCounter;
    }
    return ret;
}
 
vector<int> tarjanSCC()
{
    sccId = discovered = vector<int>(adj.size(), -1);
    sccCounter = vertexCounter = 0;
    for(int i = 0; i < adj.size(); i++) if(discovered[i] == -1) scc(i);
    return sccId;
}
 
vector<int> solve2SAT()
{
    int n = adj.size() / 2;
 
    vector<int> label = tarjanSCC();
 
    for(int i = 0; i < 2 * n ; i += 2)
        if(label[i] == label[i+1])
            return vector<int>();
 
    vector<int> value(2*n, -1);
    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());
    for(int i = 0; i < 2* n; ++i) 
    {
        int vertex = order[i].second;
        int variable = vertex/ 2, isTrue = vertex % 2 == 0;
        if(value[variable] != -1) continue;
 
        value[variable] = !isTrue;
    }
    return value;
}

 

solve2SAT() 과정

 

일단 label 벡터에 scc의 번호를 담는다.

 

만약 !A 와 A가 같은 scc의 번호라는 것은 참->거짓 인 경우가 생기는 것이므로 빈벡터를 반환한다.

 

그 후 번호를 역순으로 정렬해 위상 정렬 형태로 만든다

 

위상정렬은 왼쪽에서 오른쪽으로 가는 간선 밖에 없다.

 

그러므로 만나는 점마다 거짓점이라고 가정해도 상관이 없다.

 

isTrue: A 이면 참 !A 이면 거짓이므로

 

만일 A가 먼저 오면 거짓점으로 만들어줘야하니 !istrue 이다.

만일 !A가 먼저 오면 거짓이되어야하니 A는 참이되어야한다 따라서 !istrue이다.

 

이렇게 처음 만나는 점들은 전부 거짓으로 부여하면 

 

다시 그 점을 만나면 스킵해버려서 참으로 가정한다.

 

이것을 반복하다 보면 문제가 해결된다.

 

 

11. 시간복잡도

 

이 알고리즘의 수행 시간은 

 

그래프의 생성과 강결합 컴포넌트 분리 알고리즘에 의해 지배된다.

 

그래프의 생성 과정에서는 모든 회의의 쌍에 대해 이들이 서로 겹치는지 확인하기 때문에,

 

회의 수 2n에 대해 O(N^2)의 시간이 걸린다.

 

 

타잔의 강결합 컴포넌트 분리 알고리즘은 dfs 한번으로 수행할 수 있으므로

 

함의 그래프에 포함된 정점과 간선의 수에 비례하는 시간이 걸린다.

 

간선의 수는 최대 O(n^2)에 비례하므로, 전체 시간 복잡도는 O(N^2)이다.