[C/C++] 백준 #2207 가위바위보(2-SAT)

#2207 문제는 문제 설명이 조금 어렵습니다.  사실, 모든 경우에 필승전략은 k번째 주먹, k번째 가위를 말하면 반드시 맞으니까, 필승전략이 되겠죠.  문제는 바로 이러한 필승 전략을 요구하는 것으로 보이지만, 실제는 그것이 아니라, 학생들이 말한 내용이 필패전략(즉, 한명이라도 맞추지 못하는)이 될 수 있는지 검사하라는 것입니다.

 

rock paper scissors

 

문제의 링크입니다.

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

2207번: 가위바위보

필패전략이 되지 않으려면, n명의 학생들이 통과할 수 있는 경우가 있는지에 대해서 검사하는 것입니다.  즉, 필승전략인지를 검사하는 것이 아니라는 이야기죠.  필패전략이라는 것은 가위와 바위를 어떤 순서로 내든, 적어도 1명 이상이 맞추지 못한다는 의미입니다.

 

두가지 추측한 것 중에 하나만 맞으면 되기 때문에 논리식으로,

\[ a \lor b \]

이 참인지 검사하면 됩니다.

 

이것을 조금 변형해서 \( a \lor b = ( \lnot a \rightarrow b ) \land ( \lnot b \rightarrow a ) \)로 표현해보도록 하죠.  사실 \( ( \lnot a \rightarrow b ) \) 과 \( ( \lnot b \rightarrow a ) \) 는 대우관계로 동일한 관계입니다.  하지만 여기서는 그래프를 만들어 검증하기 위해서 위와 같이 만듭니다.

 

그러면 조금 복잡한 형태로 2개씩 짝을 지어서 4가지 경우가 모순이 생겨서 적어도 한가지 경우가 거짓이 되지 않는지 알아보고자 합니다.

\[ ( a \lor \lnot b ) \land ( \lnot a \lor b ) \land ( \lnot a \lor \lnot b ) \land ( a \lor \lnot c ) \]

이렇게 된 식을 논리식으로 표현한 후 그것을 그래프로 표현하면 아래와 같습니다.

 

파란색은 a는 \(a\)를 뜻하고 빨간색 a는 \( \lnot a \)를 뜻합니다.  그래프로 표시하면 대칭형의 그래프를 얻을 수 있습니다.  보시면 사이클을 이루는 것을 볼 수 있습니다.  이 사이클은 서로 동치형태로 존재해야함을 의미합니다.  사이클을 이루는 것들을 표시하면 다음과 같습니다.

네모난 박스안에 있는 내용들이 모순이 생기지 않는다면, 우리는 이 논리식이 논리적으로 참이 될 수 있다고 할 수 있습니다.  그 이야기는 같은 박스안에 있는 노드들이 서로 상충되는 논리식을 가지지 않으면 됩니다.  이와 같이 논리합으로 되어 있는 여러개의 쌍들이 논리적으로 참이 될 수 있는지 검사하는 알고리즘이 2-SAT 알고리즘입니다.  3개의 논리합들이 묶인 경우에는 3-SAT이고, k개의 논리합들이 묶인 경우에는 k-SAT이지만 2-SAT 이외에는 NP-Hard 문제입니다.

 

사이클을 찾아내는 방법은 순방향 DFS를 한 후, 반대로 역방향 DFS를 해서 사이클을 찾아냅니다.  그래서 두번의 DFS를 거친 후, 같은 그룹에 대해 같은 번호를 매김으로써, 모순이 생기는 노드가 있는지 검사를 합니다.

 

다음은 제가 작성한 소스입니다.

//------------------------------------------------
//    baekjoon #2207 - rock-paper-scissors
//        - by Aubrey Choi
//        - created at 2019-08-19
//------------------------------------------------
#include <cstdio>
#include <vector>
using namespace std;

#define NODE(a) ((a<0)?(((-a-1)<<1)|1):((a-1)<<1))
#define    NOT(a) (a^1)

vector<int> adj[20000];
vector<int> invadj[20000];
vector<int> order;
char used[20000];
int group[20000];

void dfs(int v)
{
    used[v] = 1;
    for(auto c : adj[v])
        if(!used[c]) dfs(c);
    order.push_back(v);
}

void invdfs(int v, int g)
{
    group[v] = g;
    for(auto c : invadj[v]) if(!group[c]) invdfs(c, g);
}

int solve(int m)
{
    for(int i = 0; i < 2*m; i++) if(!used[i]) dfs(i);
    int g = 0;
    while(!order.empty())
    {
        int v = order.back(); order.pop_back();
        if(!group[v]) invdfs(v, ++g);
    }
    for(int i = 0; i < 2*m; i+=2) if(group[i] == group[i+1]) return 0;
    return 1;
}

int main()
{
    int n, m, a, b, ans;
    scanf("%d%d",&n,&m);
    while(n--)
    {
        scanf("%d%d",&a,&b);
        if(a == -b) continue;
        a = NODE(a); b = NODE(b);
        adj[NOT(a)].push_back(b);
        adj[NOT(b)].push_back(a);
        invadj[a].push_back(NOT(b));
        invadj[b].push_back(NOT(a));
    }
    ans = solve(m);
    puts(ans?"^_^":"OTL");
}