2-SAT (2-Satisfiability Problem)

2-SAT 문제는 다음과 같다.

 

(a or b) 꼴의 식 여러 개를 and 연산으로 연립한 것이다. 이때 각 a, b, c 변수는 true, false 를 값으로 하는 변수이다. 각 변수에는 not 을 붙일 수 있다.

 

이 문제는 변수들 간의 방향 그래프로 모델링 한 후, SCC를 사용하여 해를 구할 수 있다.

 

첫 번째로, 각 항의 (a or b)는 모두 true 가 되어야 한다.

이제 하나의 항만 생각해 보자.

(a or b) 가 성립하기 위해서는 a가 false이면 b가 true / b가 false이면 a가 true 여야 한다.

이를 명제로 표현하면 !a -> b , !b -> a 이다. 이 명제들이 모두 성립한다면 (a or b) 가 성립한다.

 

이제, 모든 항들을 2개의 명제로 바꾸었다. 항의 개수가 m 개라면, 주어진 2-SAT 문제는 2*m 개의 모든 명제들을 모두 만족시키는 변수 x1, x2, x3, x4, x5, ... 들의 값을 찾으면 된다.

 

다음 단계는 변수 x1, !x1, x2, !x2, x3, !x3, x4, !x4, x5, !x5, ... 의 상태를 하나의 노드로 모델링하는 것이다.

명제 !a -> b가 있다면 말 그대로 !a 와 b 사이를 간선으로 연결해 준다. 이제 이를 통해 완성된 그래프를 통하여 원래의 2-SAT 문제에 대한 답을 찾아주면 된다.

 

만약 명제 a -> b 가 성립하고, b -> c 가 성립한다면 a -> c 가 성립하는 것도 자명하다. 따라서, 만약 완성된 함의 그래프에서 u에서 v가 도달 가능하다면 u -> v 라는 명제가 성립한다고 생각해도 좋다.

 

이러한 도달 가능성의 느낌으로 생각해보면 2-SAT 문제를 푸는데 함의 그래프에서의 SCC를 생각해 볼 수 있다.

만약 하나의 SCC안에 x와 !x가 모두 들어 있다고 생각해 보자. SCC의 정의에 따라 x -> !x, !x -> x 의 두 명제가 모두 성립해야 한다. 이는 모순이고, 이러할 경우에 답이 존재하지 않음을 알 수 있다.

 

이제 SCC를 구해서, x와 !x의 위치를 생각해 보자. 

만약 x -> !x 의 경로가 존재한다 생각하자. 이때는 x가 false 면 명제가 성립한다.

같은 논리로 !x -> x 의 경로가 존재하면 x가 true 일때 명제가 성립한다.

만약 x와 !x 사이에 간선이 없다면 ? x가 뭐가 됐던 성립한다.

이를 간단하게 구현하는 방법은 위상정렬된 SCC에서의 번호를 생각하는 것이다. (코사라주는 순서대로, 타잔은 역순)

 

시간 복잡도 : $O(N+M)$

#include <bits/stdc++.h>
using namespace std;

typedef long long ll;
typedef pair<int, int> pii;
typedef pair<ll, ll> pll;

const int MAXN = 2e4;

int n, m;
vector<int> adj[MAXN+10], revadj[MAXN+10];

bool vis1[MAXN+10];
vector<int> order;
void dfs1(int now)
{
    vis1[now]=true;
    for(int nxt : adj[now]) if(!vis1[nxt]) dfs1(nxt);
    order.push_back(now);
}

int scc[MAXN+10], scnt=1;
void dfs2(int now)
{
    scc[now]=scnt;
    for(int nxt : revadj[now]) if(scc[nxt]==0) dfs2(nxt);
}

int ans[MAXN+10];

int main()
{
    int i, j;

    scanf("%d%d", &n, &m);
    for(i=1; i<=m; i++)
    {
        int a, b, na, nb;
        scanf("%d%d", &a, &b);

        if(a<0) a=n-a, na=a-n;
        else a=a, na=a+n;

        if(b<0) b=n-b, nb=b-n;
        else b=b, nb=b+n;

        adj[na].push_back(b); revadj[b].push_back(na);
        adj[nb].push_back(a); revadj[a].push_back(nb);
        //printf("%d %d / %d %d\n", na, b, nb, a);
    }

    for(i=1; i<=2*n; i++) if(!vis1[i]) dfs1(i);
    reverse(order.begin(), order.end());

    for(i=0; i<2*n; i++)
    {
        if(scc[order[i]]==0)
        {
            dfs2(order[i]);
            scnt++;
        }
    }
    for(i=1; i<=n; i++)
    {
        if(scc[i]==scc[i+n])
        {
            return !printf("0");
        }
    }

    //for(i=1; i<=n; i++) printf("!%d %d\n", scc[i], scc[n+i]);

    for(i=1; i<=n; i++)
    {
        if(scc[i]<scc[n+i]) ans[i]=0;
        else ans[i]=1;
    }

    printf("1\n");
    for(i=1; i<=n; i++) printf("%d ", ans[i]);
}