그래프 자료구조 ②:깊이 우선 탐색③

그래프를 이용해서 푸는 심화된 문제인 2-SAT 문제와 그 풀이법을 알아봅시다

Featured image

들어가며

이때까지 이 블로그에 썼던 깊이 우선 탐색을 주제로 한 글들은 이랬습니다.

  1. DFS를 소개
  2. DFS를 활용하여 그래프 관련 문제를 푸는데 도움을 주는 여러가지들 소개(위상정렬, 사이클판별, 절단점 찾기, SCC 찾기…)

그리고 이번 포스팅에서 다룰것은, DFS를 활용해서 찾아낼수 있다고 우리가 배웠던 SCC를 활용하여 어떤 한 문제를 푸는 법을 다루어 볼 것 입니다. 응용의 응용인 셈이군요.

이번 글에서는 단순히 프로그래밍적 지식만이 아니라, 우리가 중학교, 고등학교 수학시간에 배웠던 몇몇 지식과, 이산수학 지식을 약간 써야 합니다. 그래서 좀 읽기 쉬운 글을 지향하는 제 블로그 특성상, 분량이 좀 길어지고, DFS 2번 포스팅의 내용이 여러 주제로 갈라져, 뭔가 읽고 있다보면 머리아픈 글이 될 것 같아, 별도의 글로 분리를 하였습니다.

2-SAT 문제란?

이번 글에서 다룰 문제는 SAT 문제중에 특수한 경우 2-SAT 문제입니다.

SAT문제 라는것이, 좀 생소할 수 있을 것입니다. 이 글에서 다룰 SAT 문제란, 충족 가능성 문제(SATisfiability problem) 라고 불리는 문제이고, 이는 참/거짓만을 가지는 불리언 변수들과 &, | 와 같은 논리 연산들로 이루어진 식이 주어졌을 때, 변수들의 참/거짓을 적절히 선택하면 식 전체가 참이 되게 할 수 있는지, 그리고 가능하다면 차밍 되는 값이 어떤 값인지 알아내는 문제입니다.

예를 들어보자면 a && (!b || !a) && (c && (!a || b)) 와 같이 식이 주어졌을때, a,b,c의 값을 어떻게 해야지 위 식 전체가 참이 될 수 있느냐 입니다. 참고로 8가지 모든 경우의 수를 따져봐도 위 식은 결코 참이 될 수 없습니다.

일반적인 SAT 문제를 다항시간내에 푸는 알고리즘은 지금까지 발견되지 않았다고 합니다. 사실, SAT 문제는 NP-완전 문제로 알려져있는 문제로, SAT 문제를 다항시간 내에 풀 수 있는 알고리즘은 없다고 알려져 있습니다.

하지만 다항 시간내에 풀 수 있는 특수한 형태의 SAT 문제가 있습니다. 바로 이 단락의 제목에도 적어놓은 2-SAT 문제입니다. 논리식이 주어졌을 때에, 식이 항상 괄호로 둘러쌓여 있고, 괄호 안쪽은 변수들이 논리합(OR 연산)으로 연결되어 있고, 괄호 끼리는 논리곱(AND 연산)으로 연결되어 있는 형태를 CNF(Conjunctive Normal Form : 논리곱 정규형)이라고 합니다. CNF에서 괄호로 둘러쌓인 덩어리들을 절(Clause)이라고 하며, 절 안에 변수가 최대 2개인 경우를 2-CNF라고 하고, 2-CNF에 대해서 주어진 SAT 문제를 2-SAT라고 합니다.

뭔가 설명이 되게 길어져서 복잡하게 되었지만, 간단하게 정리하면 이렇습니다.

2-SAT 문제 : SAT 문제에서 주어진 논리식을 CNF라는 형태로 변형했을 때, 괄호안에 변수가 2개까지만 들어있게 변형을 할 수 있는 경우의 문제

2-SAT 문제를 그래프를 활용해 다항시간 내에 푸는 방법을 이제부터 알아봅시다.

SAT 문제와 그래프의 접목

그래프와 별 상관이 없어 보이는 SAT 문제를 어떻게 그래프를 이용해 푸는지 부터 살짝 의아할 수 있을것 같습니다. 우선, 위에서 2-SAT문제를 다룰 때, CNF라는 형태를 잠깐 언급했었습니다. 괄호로 둘러쌓인 ‘절’ 들이 AND 연산으로 연결되어 있는 형태라고 했었지요. 당연한 말이지만, 모든 절이 참이어야만 논리식 전체가 참이 될 것 입니다. (AND연산들 사이에 끼어있는 변수중 하나라도 거짓이면 전체가 거짓이 되는게 AND 연산의 특징이니…)

그리고, OR 연산들로 이루어진 각 절들이 참이 되기 위해서는, 반드시 만족해야 하는 사항이 있습니다. \((A \| B)\)라는 항이 있을 때, A,B 두 변수 중 적어도 하나는 참이어야 한다는 당연한 사실입니다. 즉 A가 거짓이면, B가 참이어야 하고, B가 거짓이면 A는 참이어야 합니다. A가 참이거나, B가 참일 경우에는 다른 변수가 어찌 되든 별 상관이 없으니, 생각을 따로 안해도 되겠네요. A가 거짓이면, B가 참이고, B가 거짓이면 A가 참이다 이 문장을, 우리가 중고등학교 수학시간에 배웠던 화살표를 이용한 명제의 표기법을 활용해서 표기할 수 있겠습니다.

\[!A \rightarrow B\] \[!B \rightarrow A\]

명제를 배울 때, 명제를 이용해 새로운 명제를 이끌어 내는 추론, 그것도 우리가 일상적으로 잘 알고 있는 삼단추론을 생각해 봅시다. \(A \rightarrow B\) 이고, \(B \rightarrow C\)이면 \(A \rightarrow C\) 라는 것이죠? 그리고 그러한 추론이 모순을 일으킬 때도 있습니다. 간단한 예를 들자면, \(!A \rightarrow A\)와 \(A \rightarrow !A\) 두가지 명제를 둘다 충족시키는 경우는 \(A\)가 참이건 거짓이건 존재하지 않음음 쉽게 알 수 있습니다.

처음 이 장을 시작할 때, 둘이 별 상관 없어 보이는 그래프와 SAT를 연결시켜 줄 것 처럼 말해놓고, 왜 갑자기 명제 이야기를 하는지 의아해 하셨을수도 있을것 같은데, 이제 그래프와 SAT 문제를 엮기 위한 명제 이야기는 다 했으므로, 여러분이 궁금해 하시던 본론 이야기를 해보겠습니다.

함의 그래프

SAT 문제를 푸는것은 각 절에서 나오는 두가지 명제들을 각각 적절히 선택해 선택한 명제들이 서로 충돌하지 않게 하는 것입니다. 각 변수와, NOT 형태들을 정점으로 하고, 명제들을 방향 있는 간선을 이용해서 그래프 형태로 표현해 봅시다. 예를 들면 \(A \rightarrow B\)라는 명제는, A라는 정점에서 B라는 정점으로 가는 방향있는 간선으로 표현하는 것이지요. 이 그래프를 함의 그래프라고 합니다.

SAT 문제에 답이 존재한다면, 각 정점에 대해서 참 또는 거짓 값을 할당 할 수 있을 것입니다. 정점이 나타내는 변수가 참인 정점을 참 정점, 아닌것은 거짓 정점 이라고 하겠습니다.

예를들어서 \(A\)와 \(B\) 두 변수만 있는 어떠한 논리식을 푸는 SAT 문제의 가능한 답 중 한개가 \($A\)\(는 참,\)\(B\)\(는 거짓 이라고 합시다. 그렇다면 참 정점은\)A\(,\)!B\(가 될 것이며, 거짓 정점은\)!A\(,\)B$가 될 것입니다.

한 SAT 문제의 답이 존재하지 않는다면, 즉 그 SAT 문제의 논리식에 포함된 적어도 한 절이 거짓이라면, 어떤 일이 생길까요? (\(A || B\))라는 논리식이 거짓이라고 해봅시다. 위 논리식을 명제로 푼것은 위에서도 적었듯이

\[!A \rightarrow B\] \[!B \rightarrow A\]

입니다.

두 명제가 거짓이라고 하였으니, 두 명제가 거짓이려면, 화살표 왼쪽에 있는 조건이 참인데, 오른쪽에 있는것이 거짓이 되게 됩니다. 즉 참 정점에서 거짓 정점으로 가게 됩니다. 둘 중에 하나 골라야 하는 간선들인데, 둘다 그렇게 되지요. 그러므로 SAT 문제에 답이 있으려면 참에서 거짓으로 가는 경로가 없어야 겠군요. 거짓에서 참으로 가는 경로는, 즉 조건 자체가 거짓인 명제는 참인 명제로 생각하므로 상관이 없으니, 굳이 생각을 해도 되지 않아도 됩니다.

이상의 내용과, 당연한 사실 하나를 정리하면 아래와 같습니다.

만일 그래프에 사이클이 있다면, 해당 사이클 내에 있는 정점의 종류는 반드시 같아야 할까요? 달라도 될까요? 약간만 생각해보면 바로 알 수 잇듯이, 전부 참이거나, 전부 거짓이어야 합니다. 사이클 내에 종류가 다른 정점이 혼재해 있으면, 참→거짓→참 이나, 거짓→참→거짓이라는 경로가 생기게 되어서, 참에서 거짓으로 가는 경로가 하나 생기게 되니까요.

음… 방향 그래프에서 사이클과 관련된 것을 배웠던것 같은데… SCC가 생각나지 않나요? 이제 대략적으로 왜 이 논리식을 다루는 문제가 그래프, 그것도 SCC와 연관이 있는지 이해가 조금은 가실겁니다.

SCC 판별 알고리즘을 통해서 얻어낸 한 사이클에서 한 정점의 한 쌍(\(A_i\), \(!A_i\))이 한 SCC에 들어있으면 이건 확실히 위에서 말한 참에서 거짓으로 가는 경로가 생기게 됨을 알 수 있습니다.

그렇다면, 어떤 변수에 대해서도 그 변수를 표현하는 두 정점이 한 사이클 내에 없다면, SCC의 답이 존재하며, 그 답을 찾아낼 수 있을까요? 이것 또한 앞에서 오일러 경로를 찾을 때와 같이 알고리즘을 설계하고, 그 알고리즘의 정당성을 증명하는 방법으로 설명하겠습니다.

알고리즘 설계

앞에서 한 사이클 내에서 참,거짓이 혼재되어 있으면 안되는 이유로, 참에서 거짓으로 가는 경로가 생기기 때문이라고 언급하였습니다. 그러면, 그래프들을 SCC들의 연결관계로 그래프를 압축 할 수 있겠군요.

압축을 할 수 있다고 바로 압축된 그래프를 쓸 수 있는지는 정확히는 모릅니다. 압축된 그래프에서도 원래의 그래프의 성질을 그대로 가지고 있는지 확인해 봅시다. 만약에 \(A\rightarrow B\)라는 명제가 있어, \(A\)와 \(B\)가 한 SCC에 속해있다고 합시다. 그렇다면, \(!A\), \(!B\)도 한 SCC에 속해있을까요? 정답은 당연히 입니다. \(A \rightarrow B\) 명제의 대우 명제는 \(!B\rightarrow !A\) 이므로, 당연히 이 둘도 하나의 SCC에 있음을 알 수 있지요. 이를 일반화 하면, 참 정점들로 구성된 SCC가 있다면, 그 정점들의 부정형들로 구성된 거짓 정점들로만 이루어진 SCC또한 쌍으로 존재함을 확실하게 알 수 있습니다. 그러므로, SCC간에도 원래의 함의 그래프와 같은 1:1 대응 관계가 존재합니다. 한가지 예외가 있긴 한데, 한 정점의 원래 형태와 부정 형태가 동시에 존재하지 않는 경우는 이같은 것이 성립하지 않는데, 그건 앞 챕터에서 다뤘든 그런 경우는 해당 SAT 문제에 답이 존재하지 않음을 우리가 다뤘으니, 그런 경우는 따로 걸러내면 되겠지요.

그럼 이제 SCC들을 참, 거짓으로 분류를 해야하는데, 어떻게 하는것이 쉽고 정확하게 분류를 수행할 수 있을지 생각해봅시다. 사실 정말 놀랍도록 간단한 방법이 있습니다. 들어오는 간선이 하나도 없는 정점에 대해서 생각을 해봅시다. 압축한 그래프는 DAG(사이클 없는 방향 그래프) 임을 지난 포스팅에서 다루었기 때문에 해당 정점이 분명 존재함을 알 수 있습니다. 해당 정점을 참/거짓 중 어느 정점으로 분류를 하는것이 좋을까요? 간선을 받지 않고 주기만 입장에서는 참이건 거짓이건 크게 상관이 없지만, 간선을 받는 입장에서 생각해보면, 참→거짓이 안되니, 이왕이면 나한테 간선을 꽃는 정점이 참인것 보다는 거짓인 쪽이 더 편합니다. 이제 아까 말했던 들어오는 간선이 하나도 없는 정점에서 간선으로 연결된 정점들을 거짓으로 분류하고 그래프에서 이 정점을 날려 버립니다. 그리고, 이를 모든 간선이 분류될 때 까지 반복합니다.

이상이 알고리즘의 끝 입니다. 되게 단순하지요? 이제 이 알고리즘의 당위성을 귀류법을 이용해서 설명 해보겠습니다. 전제인 “이 알고리즘은 정확한 답을 찾아낸다” 를 뒤집어, 이 알고리즘을 수행 하는데, 참 정점 \(X\)에서 거짓 정점 \(Y\)로 가는 경로가 나오는 결과가 나온다면(알고리즘이 정점 \(X\), \(Y\)를 그렇게 분류했다면) 이는 위 알고리즘에서 어떤 순서로 정점 분류가 되었을까요?

\(X\rightarrow Y\)간선이 존재하고, 대우 명제도 위 그래프에 존재하니 \(!Y\rightarrow X\)또한 존재합니다. \(X\)는 참, \(Y\)는 거짓 정점이라고 하였고, 위에서 설명한 알고리즘은 거짓 정점을 먼저 지운다라는 사실에 주목하고 아래의 설명을 읽어보시기 바랍니다.

\(X\)가 참 정점이라고 판별된게 먼저라고 합시다. 그러면 \(!X\)가 거짓정점으로 판별되어 먼저 지워졌을건데, \(!Y\rightarrow !X\)라는 명제가 있으니 \(!Y\)가 먼저 지워져야 하는데, \(!Y\)는 참 정점이므로, \(Y\)가 거짓 정점이라고 먼저 판별되어 지워졌어야 하고… 여기서 모순이 발생하므로, 위에서 설명한 알고리즘이 잘못된 결과를 내는 상황이란 존재하지 않음을 알 수 있습니다.

이제 답을 찾을 수 있음은 알았으니, 실제 코드 구현을 살펴봅시다.

구 현

//adj는 함의 그래프의 인접 리스트 표현이라고 하자
//정점은 순서대로 A0, !A0, A1, !A1 이런 식으로, 한 변수의 긍정형과 부정형이 교대로 온다
vector<int> solve2SAT(){
    int n = adj.size() / 2;
    vector<int> label = tarjanSCC();// 그래프의 요소를 SCC들로 타잔의 알고리즘을 이용해 묶는다
    /*참고 : 타잔의 알고리즘은 SCC들의 번호를 위상정렬의 역순으로 매긴다.
    자세한 사항은 이전 포스팅에서 다루고 있다.*/
    for(int i = 0; i < 2 * n; i += 2)
        if(label[i] == label[i+1]) //한 정점의 긍정, 부정형이 한 SCC에 있으면
            return vector<int>;//걸러내야할 케이스

    vector<int> value(2*n, -1);//답을 저장할 배열 각 정점의 참,거짓 여부를 저장할것
    vector<pair<int,int> > order;//정렬용 보조 vector
    for(int i = 0 ; i < 2 * n; i++)
        order.push_back(make_pair(-label[i], i));//SCC번호의 역순으로 정렬하게 하여
    sort(order.begin(),order.end());//위상 정렬 순서대로 order vector안에 정렬되있게함
    for(int i = 0; i < 2 * n ; ++i){
        int vertex = order[i].second;
        int variable = vertex / 2;
        bool isTrue = vertex % 2 == 0;// 해당 정점이 긍정형인지 부정형인지
        if(value[variable] != -1) continue;//이미 분류된 정점이라면 pass
        //거짓 정점이 먼저 지워지므로, 부정형 변수라면 해당 변수의 긍정형은 참이고
        //긍정형이 거짓이면 해당 변수는 거짓이다.
        value[variable] = !isTrue;
    }
    return value;
}

마무리 하며

2-SAT 문제는 참 쓰일데가 많은 문제입니다. 두가지 중에 적어도 하나를 선택하고, 그 선택들이 서로 모순이 되지 않을 그러한 상황을 묻는 문제라면 응용할 수 있는 문제이기 때문에, 정말 활용될 수 있는 분야가 많습니다.

필자가 이 블로그를 포스팅하며 많은 참고를 했던 종만북에서도, 두가지 회의 중 하나를 반드시 개최하고, 회의들의 시간을 서로 겹치지 않게 회의 시간을 설정하는 문제를 2-SAT 문제로 푸는 예시를 보여주었습니다.

여러 선택을 하는데, 그 선택이 두가지 중 한가지가 적어도 참이다라는 냄새가 나는 문제라면 2-SAT 문제와 관련되어 있는지 한번 확인해 보자. 어렵게만 느껴졌던 문제를 위의 코드를 적당히 손보는것 만으로 간단히 문제를 풀어낼 수 있을지도 모르니까…

참고한 글