백준 11280 (2-SAT _3) C++

문제

11280번: 2-SAT - 3

n개의 변수와 m개의 절(x ∨ y)이 주어집니다.

다음과 같은 식이 주어지면 변수에 true나 false를 넣어서 전체식이 true가 될 수 있는지 구하는 문제입니다.

∧ : AND 연산

∨ : OR 연산

ㄱ : NOT 연산

예를 들어

위의 식은 x(1) = false, x(2) = false , x(3) =true 로 전체식을 true로 만들 수 있습니다.

반면에

위의 식은 x(1)어 어떤 값을 넣어도 전체식을 true로 만들 수 없습니다.

 

특정한 clause (x or y)는 다음 두 조건을 치환 될 수 있습니다.

(~x -> y) , (~y -> x) 즉 x가 아니라면 y이어야 하고, y가 아니라면 x이어야 합니다.

clause (x or y)는 항상 true이어야 하기 때문입니다. (둘 중 하나는 무조건 true)

즉, x =true라면 y = false 이고

x = false라면 , y = true입니다.

이런 관계를 근거로 그래프 간선을 이어줄 수 있습니다.

그렇다면 전체 2-sat 문제에서 모순이 생길 때는 언제?

x이면서 ~x일 때 모순이 생깁니다.

 

방향 그래프 모델링으로 해결하면 , 각 변수 i 마다 x(i)와 ~x(i) 총 2개씩 만들어 줍니다.

방향 간선을 잇고 scc를 판정 해 주자. scc의 정의를 다시 떠올리면 같은 scc내의 원소들은 직/간 접적으로 서로

도달이 가능합니다.

만약 x(i)와 ~x(i)가 같은 scc안에 속한다면 모순이 생깁니다.

모든 i에 대해 x(i)와 ~x(i)가 같은 scc안에 속해 있지 않다면 항상 모순이 없습니다.

---

while (m--) {
        cin >> a >> b;
        if (a < 0)a = abs(a) + n;
        if (b < 0)b = abs(b) + n;
        v[rev(a)].push_back(b);
        v[rev(b)].push_back(a);
    }

x(a)와 x(b)의 정보를 저장하는 과정입니다.

3, 4 번째 줄을 보면 만약 a와 b가 음수로 입력이 들어오면 not a, not b 가 들어왔다는 의미이므로

양수로 not을 표현해주어야하는 과정이 필요합니다.

절댓값을 취하고 노드의 범위 n을 더해주면 됩니다.   

이제 위에서 봤던 것 처럼 x, y가 들어오면 (x or y)가 항상 참이 되기 위해서는 

(~x or y) 이거나 (x or ~y)로 간선을 이어줘야 합니다.

우리는 x에 true, false 어떤것이 들어올지 모르므로 x, ~x 두개를 만들어 준다고 했습니다.

그러한 코드가 5 -6 번째 줄입니다.

ll rev(ll x) {
	if (x <= n)return x + n;
	return x - n;
}

 rev 함수는 not으로 바꿔주는 함수 입니다.

---

for (int i = 1; i <= 2 * n; i++) {
    if (dfsn[i])continue;
    dfs(i);
}
for (int i = 1; i <= n; i++) {
    if (sn[i] == sn[i + n]) {
        cout << "0";
        return 0;
    }
}
cout << "1" << '\n';
    

이제 scc를 찾아줄것입니다. 

1번째 줄의 for문을 i가 1부터 시작해서 2*n 까지 반복하면서 dfs를 실행합니다.

우리는 임의의 변수 x(i)에 대해서 x(i)와 ~x(i) 두개를 만들어 줬기 때문에 노드의 총 갯수는 2*n개가 됩니다.

 

5번째 줄 for문을 보면 이제 scc내부에서 모순을 찾아낼 것입니다.

6번째 줄 sn[x(i)] == sn[~x(i)] 의미는 x(i)와 ~x(i)가 같은 scc안에 있다는 의미이므로 모순입니다.

따라서 0을 출력하고 종료합니다.

 

scc를 구하는 코드는 이전에 구했기 때문에 생략하겠습니다.

---

#include<iostream>
#include<algorithm>
#include<climits>
#include<string>
#include<vector>
#include<queue>
#include<stack>
#include<deque>
#include<cmath>
#include<time.h>
#include<cstring>
#include<cmath>
#include<cstring>
#include<limits>
#define inf INT_MAX
using namespace std;
using ll = long long;
using ull = unsigned long long;
vector<ll>v[100001]; //주어진 그래프 정보 저장
ll dfsn[100001];//방문 순서를 저장할 배열
ll scc_count; //scc의 갯수를 세는 변수
ll sn[100001]; //x번 정점이 몇번째 scc에 포함되어 있는지 알려주는 배열
vector<vector<ll>>SCC; //SCC를 벡터로 저장한 벡터의 벡터
stack<ll>st;
bool fin[100001];//x번쨰 정점이 scc추출이 끝났는지 확인
ll n, m, a, b,cnt;
ll dfs(ll x);
ll rev(ll x);
int main() {
    ios_base::sync_with_stdio(false), cin.tie(NULL), cout.tie(NULL);
    cin >> n >> m;
    while (m--) {
        cin >> a >> b;
        if (a < 0)a = abs(a) + n;
        if (b < 0)b = abs(b) + n;
        v[rev(a)].push_back(b);
        v[rev(b)].push_back(a);
    }
    for (int i = 1; i <= 2 * n; i++) {
        if (dfsn[i])continue;
        dfs(i);
    }
    for (int i = 1; i <= n; i++) {
        if (sn[i] == sn[i + n]) {
            cout << "0";
            return 0;
        }
    }
    cout << "1" << '\n';
    
    return 0;
}
ll dfs(ll x) { //x와 x의 자손들 중 올라갈 수 있는 최소의 dfsn값을 return(제일 위로 어디까지 갈 수 있는지)
    dfsn[x] = ++cnt; //방문순서를 계속해서 저장
    st.push(x);
    ll ret = dfsn[x];
    for (ll nxt : v[x]) {
        if (!dfsn[nxt])ret = min(ret, dfs(nxt));
        else if (!fin[nxt])ret = min(ret, dfsn[nxt]);
    }
    if (ret == dfsn[x]) { //자신과 자신의 자손들 중 자신의 조상으로 가는 간선이 없을 경우
        vector<ll>curSCC;
        while (1) { //scc를 stack에서 빼주는 작업
            ll a = st.top();
            st.pop();
            curSCC.push_back(a);
            fin[a] = true;
            sn[a] = scc_count;
            if (a == x)break;
        }
        SCC.push_back(curSCC);
        scc_count++;
    }
    return ret;
}
ll rev(ll x) {
    if (x <= n)return x + n;
    return x - n;
}