(11280) 2-SAT - 3

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

단계별로 풀어보기

48단계(강한 연결 요소) 5번째

 

 

 

2N개의 정점을 만든다. 어떤 불리언 변수 x_i에 대해 2i번 정점은 x_i를, 2i-1번 정점은 ￢x_i를 나타낸다고 하자.

(x_i∨x_j)가 true가 되기 위해서는 둘 중 하나는 true여야 하므로 "x_i가 아니라면 x_j이다"와 "x_j가 아니라면 x_i이다"가 성립한다.

따라서 ￢x_i→x_j에서 2i-1번 정점에서 2j번 정점으로 이어지는 간선을 만들고,

￢x_j→x_i에서 2j-1번 정점에서 2i번 정점으로 이어지는 간선을 만든다. 절 내부의 변수가 NOT 형태여도 같은 방식으로 간선을 이으면 된다.

모든 절에 대해 두개씩 간선을 만든 뒤 SCC를 만들었을 때 어떤 x_i와 ￢x_i가 같은 SCC에 속한다면, x_i→ ￢ x_i이고 ￢x_i→x_i이므로 x_i는 true일 때 false여야 하고 false일 때 true여야 한다. 이는 불가능하므로 주어진 2_CNF를 true로 만들 수 없다.

 

 

 

#include <iostream>
#include <vector>
#include <stack>
using namespace std;

int main(){
  ios_base::sync_with_stdio(false);
  cin.tie(NULL);
  cout.tie(NULL);
  
  int n, m, cnt= 1, idx= 1;
  
  cin >> n >> m;
  
  vector<int> check(2*n+1), scc(2*n+1);
  vector adj(2*n+1, vector<int> ());
  stack<int> st;
  
  while(m--){
    int i, j;
    
    cin >> i >> j;
    
    if(i>0&&j>0){
      adj[2*i-1].push_back(2*j);
      adj[2*j-1].push_back(2*i);
    }else if(i>0){
      adj[2*i-1].push_back(-2*j-1);
      adj[-2*j].push_back(2*i);
    }else if(j>0){
      adj[-2*i].push_back(2*j);
      adj[2*j-1].push_back(-2*i-1);
    }else{
      adj[-2*i].push_back(-2*j-1);
      adj[-2*j].push_back(-2*i-1);
    }
  }
  
  auto dfs= [&](auto self, int now) -> int {
    st.push(now);
    check[now]= cnt++;
    int low= check[now];
    
    for(int next:adj[now]){
      if(!check[next]){
        low= min(low, self(self, next));
      }else if(!scc[next]){
        low= min(low, check[next]);
      }
    }
    
    if(check[now]==low){
      while(true){
        int here= st.top();
        st.pop();
        scc[here]= idx;
        
        if(here==now)  break;
      }
      
      idx++;
    }
    
    return low;
  };
  
  for(int i=1;i<=2*n;i++){
    if(check[i])  continue;
    
    dfs(dfs, i);
  }
  
  for(int i=1;i<=n;i++){
    if(scc[2*i-1]==scc[2*i]){
      cout << 0;
      
      return 0;
    }
  }
  
  cout << 1;
  
  return 0;
}