2-SAT

References

• Algorithms (Sanjoy Dasgupta)

Contents

• Backtracking
• 2-SAT를 그래프 문제로 변환
• 백준 11277번, 11278번, 11280번, 11281번

---

이번 포스팅에서는 아래의 포스팅에서 언급했었던 2-SAT 문제에 대해서 살펴볼 예정입니다.

NP-Complete Problems (1)

NP-Complete Problems (2)

포스팅에서 2-SAT를 그래프로 변환한 다음 SCC를 찾음으로써 다항 시간에 해결할 수 있다고 했습니다. 하지만, 그 전에 먼저 백트래킹 기법을 이용하여 SAT 문제를 푸는 방법에 대해서 살펴보겠습니다.

 

Backtracking

백트래킹은 해의 일부분만을 보고 이 해가 답이 될 수 없다는 것을 판단할 수 있는 경우가 많다는 관찰에 근거를 둡니다. 예를 들어, SAT 문제에서 \(x_1 \vee x_2\)라는 절을 포함한다고 가정해봅시다. 그러면 \(x_1 = x_2 = 0\)을 배정하는 것은 답이 될 수 없다는 것을 바로 알 수 있습니다. 즉, 이러한 부분적인 해를 통해 전체 탐색 공간을 가지치기할 수 있습니다. 문제는 이러한 전략을 체계적으로 적용하기가 쉽지는 않습니다.

 

백트래킹을 사용하는 방법을 예를 통해 살펴볼텐데, 다음과 같은 절(clause)들의 집합인 부울식 \(\Phi(w, x, y, z)\)으로 살펴보겠습니다.

이러한 부울식이 있는 경우에 우리는 부분해의 트리를 확장해나가면서 답을 찾아낼 수 있습니다. 즉, 임의의 변수, 예를 들어, \(w\)를 선택하여 초기 트리를 다음과 같이 둡니다.

\(w = 0\)과 \(w = 1\)을 \(\Phi\)에 대입해서 살펴보면, false가 되는 절은 없기 때문에 이 두 가지 경우에서 제거될 수 있는 가지는 없다는 것을 알 수 있습니다. 따라서, 다음 임의의 변수를 선택하여 트리를 확장합니다.

예를 들어, 다음과 같이 \(x\)를 선택해서 트리를 확장해봅시다.

이번에는 \(w = 0, x = 1\)로 대입하는 것이 절 \((w \vee \bar{x})\)를 false로 만들기 때문에 이 가지는 더 이상 살펴볼 필요가 없게 되며, 따라서 탐색 공간의 상당 부분을 가지치기할 수 있습니다. 이 막다른 루트에서 백트래킹하여 나머지 두 가지 중 임의의 하나를 선택해서 탐색을 계속 진행합니다.

 

이러한 방법으로 백트래킹은 현 상태(부분해)에서 결과를 알 수 없는 노드만 계속 확장해나가고, 주어진 식을 만족시키는 truth assignment가 발견되면 종료합니다.

 

SAT 문제에서는 탐색 트리의 각 노드는 임의의 변수를 대입했을 때 남아있는 절들로 표현될 수 있습니다. 예를 들어, \(w = 0, x = 0\)을 대입한 경우 \(\bar{w}\)나 \(\bar{x}\)를 포함한 절은 무조건 만족하며, \(w\)나 \(x\)는 만족되지 않음으로서 제거될 수 있습니다. 따라서 남는 절들은 다음과 같습니다.

비슷한 이유로, \(w = 0, x = 1\)은 아래의 절들을 남깁니다.

다만, 위의 빈 절 '()'는 만족시키는 것이 불가능하다는 것을 나타냅니다. 따라서 부분적으로 값을 대입하여 나타내는 탐색 트리의 노드는 그 자체가 SAT의 subproblem이 됩니다.

 

이러한 방법으로 위에 예시 문제에서는 다음과 같은 탐색 트리로 답을 찾아나갑니다.

즉, 위 문제에서는 부울식을 만족하는 해가 존재하지 않습니다.

 

---

백준 11277번, 11278번

https://www.acmicpc.net/problem/11277

11277번: 2-SAT - 1

https://www.acmicpc.net/problem/11278

11278번: 2-SAT - 2

백준 11277번과 11278번 문제는 위의 백트래킹 방법을 통해 해결할 수 있습니다. 이 문제는 주어진 입력의 개수가 적기 때문에 백트래킹으로 해결 가능하며, 11277번 문제는 단순히 주어진 부울식의 해가 존재하는지만 찾으면 되고, 11278번 문제는 부울식의 해가 존재한다면 각 변수에 어떤 값을 대입해야 하는지도 찾아야 합니다.

 

두 문제가 거의 동일하기 때문에 11278번 문제의 풀이만 남겨두도록 하겠습니다. 저의 풀이는 아래와 같습니다.

#include <iostream>
#include <vector>

using namespace std;

void dfs(int cnt, vector<bool>& sel, bool& pass, const int N, const vector<pair<int, int>>& clauses)
{
    if (pass)
        return;

    if (cnt == N + 1) {
        pass = true;
        printf("1\n");
        for (int i = 0; i < cnt - 1; i++) {
            printf("%d ", sel[i] ? 1 : 0);
        }
        return;
    }

    for (auto& clause : clauses) {
        int a = clause.first;
        int b = clause.second;
        if (abs(a) <= cnt && abs(b) <= cnt) {
            bool ret = false;

            ret |= (a > 0 ? sel[abs(a) - 1] : !sel[abs(a) - 1]);
            ret |= (b > 0 ? sel[abs(b) - 1] : !sel[abs(b) - 1]);

            if (!ret)
                return;
        }
    }

    sel.push_back(true);
    dfs(cnt + 1, sel, pass, N, clauses);
    sel.pop_back();

    sel.push_back(false);
    dfs(cnt + 1, sel, pass, N, clauses);
    sel.pop_back();
}

int main(int argc, char** argv)
{
    int N, M;
    scanf("%d %d", &N, &M);

    vector<pair<int, int>> clauses(M);

    int a, b;
    for (int i = 0; i < M; i++) {
        scanf("%d %d", &a, &b);
        clauses[i].first = a;
        clauses[i].second = b;
    }

    vector<bool> sel;
    bool pass = false;
    dfs(0, sel, pass, N, clauses);

    if (!pass)
        printf("0\n");

    return 0;
}

 

---

2-SAT를 그래프 문제로 변환

위의 풀이 방법은 입력의 개수가 많지 않을 때만 가능합니다. 따라서, 입력의 크기가 크다면 위의 방법으로는 쉽게 풀리지 않습니다. 예를 들어, 11277번과 동일한 문제이지만 11280번 문제의 입력 크기는 매우 커서, 위의 코드를 그대로 사용하면 시간 초과가 발생합니다.

https://www.acmicpc.net/problem/11280

11280번: 2-SAT - 3

따라서, 더 빠른 알고리즘이 필요합니다.

 

이전 포스팅에서 언급했지만, 2-SAT 문제는 SAT의 특수한 케이스이고 이 경우에는 다항 시간 알고리즘이 존재한다고 언급했습니다. 이는 2-SAT 문제를 그래프 문제로 변환하고 SCC를 찾아서 해결할 수 있습니다.

 

그럼 먼저 2-SAT 문제를 어떻게 그래프로 변경하는지부터 살펴보겠습니다.

일단 \((x_1, x_2)\)라는 절이 있다고 가정해봅시다. 그렇다면, 이 절은 \(x_1\)이나 \(x_2\) 둘 중 하나는 반드시 true가 되어야 합니다. 반대로 말하면, \(x_1\)이 false라면 \(x_2\)는 반드시 true이어야 하고, \(x_2\)가 false라면 \(x_1\)은 반드시 true이어야 합니다.

여기서 우리는 후자의 경우, 두 변수 중 하나가 false라면 다른 변수는 true이어야 한다는 것을 그래프로 나타냅니다. 따라서 \((x_1, x_2)\)는 다음의 2가지 간선으로 나타낼 수 있습니다.

\[\bar{x}_1 \rightarrow x_2 \text{,  } \bar{x}_2 \rightarrow x_1\]

 

예를 들어, 아래와 같은 부울식이 있다면,

\[f = (\bar{x}_1 \vee x_2) \wedge (\bar{x}_2 \vee x_3) \wedge (x_1 \vee x_3) \wedge (x_3 \vee x_2) \]

이는 각 변수 \(x\)와 \(\bar{x}\)가 정점이면서, 아래의 간선들을 갖는 그래프가 됩니다.

\[(x_1 \rightarrow x_2), (\bar{x}_2 \rightarrow \bar{x}_1), (x_2 \rightarrow x_3), (\bar{x}_3 \rightarrow \bar{x}_2), (\bar{x}_1 \rightarrow x_3), (\bar{x}_3 \rightarrow x_1), (\bar{x}_3 \rightarrow x_2), (\bar{x}_2 \rightarrow x_3)\]

 

이제 한 가지 문제가 남았는데, 바로 SCC를 추출하는 것까진 좋은데 이를 어떻게 사용해야 위 식을 true로 하는 답이 존재한다고 판단할 수 있을까요?

이는 어느 한 변수에서 자기 자신의 not 변수로 가는 경로를 조사하면 알 수 있습니다. 즉, 어떤 변수로부터 자기 자신의 not 변수로 가는 경로가 존재한다면, 주어진 부울식을 true로 만드는 해가 없다는 것을 의미합니다. 변수의 개수가 적다면 다른 방법도 가능하겠지만, 변수의 개수가 많다면 SCC 내에 이러한 조건을 만족하는 변수가 존재하는지 확인함으로써 해가 존재하는지 여부를 알 수 있습니다.

 

저의 경우, 변수 1의 경우에는 정점 0(\(x_1\)), 1(\(\bar{x}_1\))을 부여하는 방식으로 그래프를 구성하여 문제를 해결하였습니다. 전체 코드는 아래와 같습니다. SCC를 추출하는 방법은 코사라주 알고리즘을 사용했으며, 이에 관한 내용은 이전 포스팅(강한 연결 요소 (Strongly Connected Component))을 참조하시길 바랍니다 !

#include <iostream>
#include <vector>
#include <stack>
#include <algorithm>

int get_vertex_num(int v)
{
    return (v > 0) ? (v - 1) * 2 : -(v + 1) * 2 + 1;
}

int get_not_vertex_num(int v)
{
    return (v > 0) ? (v - 1) * 2 + 1 : -(v + 1) * 2;
}

void set_graph(std::vector<std::vector<int>>& graph, int u, int v)
{
    graph[u].push_back(v);
}

std::vector<std::vector<int>> get_reversed_graph(std::vector<std::vector<int>>& graph)
{
    const int V = graph.size();
    std::vector<std::vector<int>> reversed_graph(V);
    for (int u = 0; u < V; u++) {
        for (auto v : graph[u]) {
            reversed_graph[v].push_back(u);
        }
    }
    return reversed_graph;
}

void post_visit(std::vector<int>& post, const int v)
{
    static int clock = 0;
    post[v] = clock++;
}

// dfs to get post number
void dfs(const int cur, std::vector<bool>& visited, std::stack<int>& st, const std::vector<std::vector<int>>& graph)
{
    visited[cur] = true;
    for (auto next : graph[cur]) {
        if (!visited[next]) {
            dfs(next, visited, st, graph);
        }
    }
    st.push(cur);
}

// dfs to get SCC
void dfs(const int cur, std::vector<int>& scc, std::vector<bool>& visited, const std::vector<std::vector<int>>& graph)
{
    visited[cur] = true;
    scc.push_back(cur);
    for (auto next : graph[cur]) {
        if (!visited[next]) {
            dfs(next, scc, visited, graph);
        }
    }
}

int main(int argc, char* argv[])
{
    int N, M;
    scanf("%d %d", &N, &M);
    std::vector<std::vector<int>> graph(2 * N);
    int u{}, v{};
    for (int i = 0; i < M; i++) {
        scanf("%d %d", &u, &v);
        set_graph(graph, get_not_vertex_num(u), get_vertex_num(v));
        set_graph(graph, get_not_vertex_num(v), get_vertex_num(u));
    }
    // get reversed graph
    auto reversed_graph = get_reversed_graph(graph);

    // set init variables
    std::vector<bool> visited(2 * N, false);
    std::stack<int> st;

    // 1. run dfs on reversed_graph
    for (int u = 0; u < 2 * N; u++) {
        if (!visited[u]) {
            dfs(u, visited, st, reversed_graph);
        }
    }
    std::fill(visited.begin(), visited.end(), false);

    // 2. run dfs on graph
    std::vector<std::vector<int>> SCC;
    while (!st.empty()) {
        int cur = st.top();
        st.pop();
        std::vector<int> curSCC;
        if (!visited[cur]) {
            dfs(cur, curSCC, visited, graph);
            sort(curSCC.begin(), curSCC.end());
            SCC.push_back(curSCC);
        }
    }

    // set num to SCC group
    std::vector<int> scc_idx(2 * N);
    int idx = 0;
    for (auto& curSCC : SCC) {
        for (int cur : curSCC) {
            scc_idx[cur] = idx;
        }
        ++idx;
    }

    // check valid
    for (int i = 0; i < N; i++) {
        if (scc_idx[i * 2] == scc_idx[i * 2 + 1]) {
            printf("0\n");
            return 0;
        }
    }

    printf("1\n");

    return 0;
}

다행히 적당히 풀리는 것 같습니다... !

 

 

---

백준 12281번

https://www.acmicpc.net/problem/11281

11281번: 2-SAT - 4

11281번 문제는 11280번과 동일하지만, 주어진 부울식을 true로 만드는 각 변수의 값을 찾아야 합니다. 물론 해가 여러개 존재할 수 있으므로, 문제는 스페셜 저지로 표기되어 있네요.

 

위의 풀이에서 해가 존재할 때, 변수들의 값을 찾는 부분을 추가하면 될 것 같습니다.

12280번 문제 코드에서 SCC를 구한 뒤, 각 SCC에 인덱스를 부여했습니다. 그런데 사실 인덱스를 부여할 때 SCC는 이미 위상이 정렬되어 있습니다. DFS에서 방문한 순서대로 SCC를 찾았고, 그 순서대로 오름차순으로 인덱스를 부여했습니다. 따라서 인덱스의 역순으로 방문하면 SCC 단위로 위상정렬을 한 것과 같습니다.

 

그리고, \((x_1 \rightarrow x_2)\)는 \(x_1\)이 false라면 \(x_2\)는 true라는 것을 의미한다고 했습니다. 따라서 먼저 방문하는 것을 false라고 한 뒤에, 나머지를 살펴보는 것이 유리합니다.

예를 들어, \(x_1\)가 먼저 나온다면 \(x_1\)은 false가 되며, 만약 not \(x_1\)이 먼저 나온다면 \(x_1\)은 true가 됩니다.

 

풀이는 다음과 같습니다.

#include <iostream>
#include <vector>
#include <stack>
#include <algorithm>

int get_vertex_num(int v)
{
    return (v > 0) ? (v - 1) * 2 : -(v + 1) * 2 + 1;
}

int get_not_vertex_num(int v)
{
    return (v > 0) ? (v - 1) * 2 + 1 : -(v + 1) * 2;
}

void set_graph(std::vector<std::vector<int>>& graph, int u, int v)
{
    graph[u].push_back(v);
}

std::vector<std::vector<int>> get_reversed_graph(std::vector<std::vector<int>>& graph)
{
    const int V = graph.size();
    std::vector<std::vector<int>> reversed_graph(V);
    for (int u = 0; u < V; u++) {
        for (auto v : graph[u]) {
            reversed_graph[v].push_back(u);
        }
    }
    return reversed_graph;
}

void post_visit(std::vector<int>& post, const int v)
{
    static int clock = 0;
    post[v] = clock++;
}

// dfs to get post number
void dfs(const int cur, std::vector<bool>& visited, std::stack<int>& st, const std::vector<std::vector<int>>& graph)
{
    visited[cur] = true;
    for (auto next : graph[cur]) {
        if (!visited[next]) {
            dfs(next, visited, st, graph);
        }
    }
    st.push(cur);
}

// dfs to get SCC
void dfs(const int cur, std::vector<int>& scc, std::vector<bool>& visited, const std::vector<std::vector<int>>& graph)
{
    visited[cur] = true;
    scc.push_back(cur);
    for (auto next : graph[cur]) {
        if (!visited[next]) {
            dfs(next, scc, visited, graph);
        }
    }
}

int main(int argc, char* argv[])
{
    int N, M;
    scanf("%d %d", &N, &M);
    std::vector<std::vector<int>> graph(2 * N);
    int u{}, v{};
    for (int i = 0; i < M; i++) {
        scanf("%d %d", &u, &v);
        set_graph(graph, get_not_vertex_num(u), get_vertex_num(v));
        set_graph(graph, get_not_vertex_num(v), get_vertex_num(u));
    }
    // get reversed graph
    auto reversed_graph = get_reversed_graph(graph);

    // set init variables
    std::vector<bool> visited(2 * N, false);
    std::stack<int> st;

    // 1. run dfs on reversed_graph
    for (int u = 0; u < 2 * N; u++) {
        if (!visited[u]) {
            dfs(u, visited, st, reversed_graph);
        }
    }
    std::fill(visited.begin(), visited.end(), false);

    // 2. run dfs on graph
    std::vector<std::vector<int>> SCC;
    while (!st.empty()) {
        int cur = st.top();
        st.pop();
        std::vector<int> curSCC;
        if (!visited[cur]) {
            dfs(cur, curSCC, visited, graph);
            sort(curSCC.begin(), curSCC.end());
            SCC.push_back(curSCC);
        }
    }

    // set num to SCC group
    std::vector<int> scc_idx(2 * N);
    //sort(SCC.begin(), SCC.end());
    int idx = 0;
    for (auto& curSCC : SCC) {
        for (int cur : curSCC) {
            scc_idx[cur] = idx;
        }
        ++idx;
    }

    // check valid
    for (int i = 0; i < N; i++) {
        if (scc_idx[i * 2] == scc_idx[i * 2 + 1]) {
            printf("0\n");
            return 0;
        }
    }

    printf("1\n");

    // get truth assignments
    std::vector<int> results(N, -1);
    std::vector<std::pair<int, int>> vertex_info(2 * N);
    for (int i = 0; i < 2 * N; i++) {
        vertex_info[i] = { scc_idx[i], i };
    }
    // sort by scc number
    sort(vertex_info.begin(), vertex_info.end());

    for (int i = 2 * N - 1; i >= 0; i--) {
        int var = vertex_info[i].second; // variable(vertex) number
        if (results[var / 2] == -1)
            results[var / 2] = (var % 2);
    }

    for (int i = 0; i < N; i++) {
        printf("%d ", results[i]);
    }

    return 0;
}