BOJ)15675 괴도 강산

문제 :icpc.me/15675

모든 보석을 집고, 위치 추적기를 하나도 안 가진 상태가 가능하다면 1을 아니면 0을 출력하는 문제이다.

문제의 조건을 잘 읽어보면 2NF로 모델링이 가능하여 2-SAT을 이용한 풀이가 가능하다.

우선 보석을 고르는 조건은, 보석이 존재하는 행을 a 열을 b라고 하였을 때, a b 중에 하나밖에 선택되지 않으므로

(a&&!b)||(!a&&b) 라는 식이 세워진다. 하지만 이는 CNF가 아니므로 식을 잘 풀어내어 (a||b)&&(!a||!b)로 변형하여 추가해준다.

다음으로 위치추적기를 밟는 경우 다시 그자리에 돌려놔야 하므로 a b 를 모두 선택하거나 a b를 모두 선택하지 않는 경우 중 한 경우가 이루어져야 한다.

즉(a&&b)||(!a&&!b) 라는 식이 세워지고 이를 CNF로 표현하여 (a||!b)&&(!a||b)를 추가해준다.

이 후 SCC를 확인해주어 valid 한지 여부를 보면 된다.

#include <cstdio>
#include <algorithm>
#include <vector>
#include <cstring>
#include <stack>
using namespace std;
struct TwoSAT{
    int n,c,sccc;
    vector<vector<int>> vt;
    vector<int> disc,scc;
    stack<int> st;
    TwoSAT(int n):n(n){
        vt.resize(2*n+1);
        disc.assign(2*n+1,0);
        scc.assign(2*n+1,0);
        c=sccc=0;
    }
    int dfs(int here){
        int ret=disc[here]=++c;
        st.push(here);
        for(auto next:vt[here]){
            if(!disc[next])
                ret=min(ret,dfs(next));
            else if(!scc[next])
                ret=min(ret,disc[next]);
        }
        if(ret==disc[here]){
            sccc++;
            while(1){
                int h=st.top();
                st.pop();
                scc[h]=sccc;
                if(h==here)break;
            }
        }
        return ret;
    }
    int convert(int h){
        return h<=n?h+n:h-n;
    }
    void add_CNF(int x,int y){
        vt[convert(x)].push_back(y);
        vt[convert(y)].push_back(x);
    }
    bool is_satisfied(){
        for(int i=1;i<=2*n;i++)
            if(!disc[i])dfs(i);
        for(int i=1;i<=n;i++)
            if(scc[i]==scc[convert(i)])return false;
        return true;
    }
};
int n,m;
char a[1001][1001];
int main(){
    scanf("%d%d",&n,&m);
    TwoSAT ts(n+m);
    for(int i=0;i<n;i++)scanf("%s",a[i]);
    for(int i=0;i<n;i++){
        for(int j=0;j<m;j++){
            if(a[i][j]=='*'){
                ts.add_CNF(i+1,j+1+n);
                ts.add_CNF(ts.convert(i+1),ts.convert(j+1+n));
            }
            else if(a[i][j]=='#'){
                ts.add_CNF(i+1,ts.convert(j+1+n));
                ts.add_CNF(ts.convert(i+1),j+1+n);
            }
        }
    }
    printf("%d\n",ts.is_satisfied());
    return 0;
}