133. 2-SAT

충족 가능성 문제(SAT, Satisfiability Problem)는 Boolean 변수들(True 또는 False 중 한 가지 값을 가질 수 있음)로 이루어진 식의 값이 True가 되게 하는 변수들의 값 조합이 존재하는지를 알아내는 문제이다. 이러한 식은 불 연산식(Boolean Expression)이라고 부르며 다음과 같은 두 가지의 형태로 나타낼 수 있다. 식에서 $\neg$, $\wedge$, $\vee$ 기호는 각각 NOT, AND, OR 연산자와 같은 의미를 가지며 $\neg$ 연산자의 우선순위가 가장 높다.

• CNF(Conjunctive Normal Form): $f = (x_1 \vee x_2) \wedge (\neg x_3 \vee x_1 \vee x_4) \wedge (\neg x_2 \vee x_3)$; $\vee$로 묶인 절이 $\wedge$로 연결된 형태
• DNF(Disjunctive Normal Form): $f = (x_1 \wedge \neg x_3) \vee (x_1 \wedge x_2) \vee (x_2 \wedge x_3 \wedge \neg x_4)$; $\wedge$로 묶인 절이 $\vee$로 연결된 형태

식에서 괄호로 묶인 각각의 부분은 절(Clause)이라고 부르며 CNF에서는 각 절의 값이 전부 True일 때만 전체 식의 결과값이 True가 되고 DNF에서는 각 절의 값 중 True가 하나라도 존재하면 전체 식의 결과값이 True가 된다. 충족 가능성 문제에서는 CNF를 주로 다루며, CNF의 각 절에 최대 $k$개의 변수가 존재하는 경우를 $k$-SAT이라고 부른다. 위의 예시에 나온 CNF의 경우 두 번째 절에 있는 변수가 $3$개로 가장 많으므로 3-SAT이라고 부르면 된다.

 

일반적으로 충족 가능성 문제는 $k$의 값에 따라 세 가지로 분류한다. 첫 번째로 $1$-SAT은 $x_1$과 $\neg x_1$ 꼴이 동시에 나오는 경우가 없으면 전체 식을 True로 만들 수 있다. 두 번째로 $2$-SAT은 다항 시간에 풀 수 있는데 이 풀이에서 SCC가 등장한다. 세 번째로 $k$가 $3$ 이상인 모든 SAT은 $3$-SAT으로 변형할 수 있으며, NP-Hard 문제이다.

---

여기서부터는 $2$-SAT을 SCC를 이용하여 푸는 방법을 소개한다. 먼저 명제와 관련된 정의를 몇 가지 짚고 넘어가자면,

• 두 Boolean 변수 $p$와 $q$가 존재할 때 $p$가 참이면 $q$도 참이라는 명제를 $p \to q$로 나타낸다.
• 명제 $p \to q$는 $p$가 거짓이거나 $q$가 참일 경우 참이다. 즉, $p \to q$와 $\neg p \vee q$는 동치이다.
• 만약 $p$와 $q$ 외에 다른 변수 $r$이 존재하고 $p \to r$, $r \to q$가 성립할 때 $p$가 참이면 $q$도 참이 되는데, 이렇게 간접적으로 참이 되는 관계를 $p \Rightarrow q$로 나타낸다.

$2$-SAT의 각 절은 변수 $2$개가 $\vee$ 연산자로 결합된 구조로 되어 있다. 이때 절은 다음과 같이 변형할 수 있다.

$$x_1 \vee x_2 \equiv (\neg x_1 \to x_2) \wedge (\neg x_2 \to x_1)$$

여기서 각 변수의 값이 True인 상태와 False인 상태를 정점으로 두면 $x_1 \to x_2$는 $x_1$이 참인 상태를 나타내는 정점에서 $x_2$가 참인 상태를 나타내는 정점으로 가는 방향 간선이 존재한다는 의미로 해석할 수 있다. 따라서 위에서 변형한 내용에 맞게 그래프에 간선을 추가할 수 있다. 그렇게 해서 만들어진 그래프에서 $x_1$과 $\neg x_1$이 같은 SCC에 속하는 경우가 없으면 전체 식을 True로 만들 수 있다.

 

그렇다면 각 변수에 어떤 값을 대입해야 전체 식이 True가 되는지를 구해야 하는데, 현재 SCC끼리 묶은 그래프는 DAG의 형태이므로 위상 정렬이 가능하고, 만약 위상 정렬을 했을 경우 먼저 나오는 컴포넌트에 속한 변수들의 값을 False로 정하는 방법을 생각해 볼 수 있다. 다음과 같은 식을 예로 들면,

$$f = (x_1 \vee \neg x_3) \wedge (\neg x_2 \vee x_1) \wedge (\neg x_1 \vee \neg x_4) \wedge (x_2 \vee x_4) \wedge (x_3 \vee \neg x_4)$$

$4$개의 SCC로 이루어진 그래프가 나온다.

이제 SCC 단위로 위상 정렬을 실행하면 초록색 → 노란색 → 파란색 → 빨간색 또는 초록색 → 파란색 → 노란색 → 빨간색 순서가 된다. 여기서 가장 먼저 나오는 초록색 컴포넌트에 속한 변수들의 값을 False로 설정할 경우 이와 반대되는 속성을 가진 빨간색 컴포넌트에 속한 변수들의 값이 True가 된다. 다음으로 노란색 또는 파란색 컴포넌트가 나오는데, 둘 중 먼저 나온 컴포넌트에 속한 변수들의 값을 False로 설정하면 나머지 하나에 속한 변수들의 값은 True가 된다. 다음으로 나오는 컴포넌트들은 이미 변수들의 값이 할당된 상태이므로 그냥 넘어간다. 따라서 $x_1 =$ True, $x_2 =$ True, $x_3 =$ True, $x_4 =$ False 또는 $x_1 =$ True, $x_2 =$ True, $x_3 =$ False, $x_4 =$ False의 두 가지가 전체 식의 값을 True로 만드는 경우가 된다.

시간복잡도를 계산하면, 변수의 수가 $n$이고 절의 수가 $m$일 때 $2n$개의 정점과 $2m$개의 간선이 있는 그래프에서 SCC를 구하는 시간이 $\Theta(n + m)$이고, 변수들의 값을 설정하는 시간이 $\Theta(n)$이므로 전체 시간복잡도는 $\Theta(n + m)$이다.

 

구현은 다음과 같다. $1$ ~ $n$번 정점이 변수의 값이 True인 경우, $(n + 1)$ ~ $2n$번 정점이 변수의 값이 False인 경우를 각각 나타낸다. $\text{var}[i]$는 $i$번째 변수의 값을 나타낸다. DFS를 실행하면서 각 변수들의 값을 동시에 구하는 것에 주목하자.

#import<bits/stdc++.h>
using namespace std;
int c, n, v1[200004], v2[200004], var[100005];
vector<int>e[200004];
stack<int>S;
int dfs(int u)
{
    int minc = v1[u] = ++c;
    S.push(u);
    for(auto &v: e[u])
    {
        if(!v1[v])minc = min(minc, dfs(v));
        else if(!v2[v])minc = min(minc, v1[v]);
    }
    if(minc == v1[u])
    {
        for(;;)
        {
            int x = S.top();
            S.pop();
            v2[x] = minc;
            int p = x > n ? x - n : x;
            if(var[p] < 0)var[p] = x <= n; // 변수에 값 대입
            if(x == u)break;
        }
    }
    return minc;
}
int main()
{
    int m, x, y;
    cin >> n >> m;
    for(int i = 1; i <= m; i++)
    {
        cin >> x >> y;
        e[x > 0 ? n + x : - x].push_back(y > 0 ? y : n - y);
        e[y > 0 ? n + y : - y].push_back(x > 0 ? x : n - x);
    }
    fill(var + 1, var + n + 1, -1);
    for(int i = 1; i <= n << 1; i++)
    {
        if(!v1[i])dfs(i);
    }
    for(int i = 1; i <= n << 1; i++)
    {
        if(v2[i] == v2[i + n])
        {
            // 전체 식을 True로 만드는 방법이 존재하지 않는 경우
        }
    }
}

 

[연습문제]

 

BOJ 11280. 2-SAT - 3 (Platinum IV)

$2$-SAT으로 식 $f$의 값을 True로 만들 수 있는지의 여부를 구한다.

 

BOJ 11281. 2-SAT - 4 (Platinum III) [샘플 코드]

식 $f$의 값을 True로 만들 수 있는 경우 각 변수의 값까지 구한다.

 

BOJ 3648. 아이돌 (Platinum III)

상근이가 항상 다음 라운드에 진출해야 한다는 조건이 있으므로 $(x_1 \vee x_1)$ 절을 CNF에 추가하고 $2$-SAT을 적용하면 된다. $n$과 $m$의 제한이 작아서 코사라주 알고리즘이나 타잔 알고리즘은 안 써도 되고, DFS $2n$번으로 $\Theta(n^2 + nm)$ 시간에 답을 구해도 된다.

 

→ solved.ac tag: 2_sat