[백준 11280] 2-SAT - 3

문제 링크 => 11280번: 2-SAT - 3 (acmicpc.net)

11280번: 2-SAT - 3

---

SCC 를 활용하는 문제이다.

 

여기서 기본으로 알아야 할 상식은 다음과 같다.

 

1. ~a v b 는 a -> b 또는 ~b -> ~a (대우) 로 표현이 가능하다.

 

2. SCC로 묶인 xi, ~xi (i = 1, 2, 3, ... , n) 에 대하여 i가 동일할 경우 xi, ~xi 가 동시에 있는 경우 무조건 False 이다.

 

따라서 1번을 통해서 정점들을 연결해주고 SCC 를 만들어주고 각 SCC 마다 xi, ~xi 가 동시에 있는 경우만을 확인하면 된다.

 

SCC를 만드는 알고리즘은 Kosaraju's Algorithm 을 활용하여 만들었다.

 

풀이 code

#define _CRT_SECURE_NO_WARNINGS
#include <string>
#include <stdio.h>
#include <math.h>
#include <iostream>
#include <vector>
#include <algorithm>
#include <map>
#include <queue>
#include <stack>
#include <time.h>
#define INF 100000000
#define endl '\n'
#define ll long long

using namespace std;

int N, M;
vector<int> go[20001], back[20001];
int inDegree[20001];
bool visited[20001];
stack<int> s;
vector<vector<int>> SCC;

int notX(int x) {
	if (x > N) return x - N;
	return x + N;
}

void dfs1(int x) {
	if (visited[x]) return;
	visited[x] = true;
	for (int i = 0; i < go[x].size(); i++) {
		int next = go[x][i];
		dfs1(next);
	}
	s.push(x);
}

void dfs2(int x, vector<int> &v) {
	if (visited[x]) return;
	visited[x] = true;
	for (int i = 0; i < back[x].size(); i++) {
		int next = back[x][i];
		dfs2(next, v);
	}
	v.push_back(x);
}

void initialize() {
	for (int i = 1; i <= N; i++) {
		visited[i] = visited[i + N] = false;
	}
}

void solve() {
	cin >> N >> M;

	for (int i = 0; i < M; i++) {
		int x, y;
		cin >> x >> y;
		if (x < 0) x = abs(x) + N;
		if (y < 0) y = abs(y) + N;
		
		// ~x -> y
		go[notX(x)].push_back(y);
		back[y].push_back(notX(x));
		
		// ~y -> x
		go[notX(y)].push_back(x);
		back[x].push_back(notX(y));
	}

	for (int i = 1; i <= N; i++) {
		if (!visited[i]) dfs1(i);
		if (!visited[i + N]) dfs1(i + N);
	}

	initialize();

	while (!s.empty()) {
		int x = s.top();
		s.pop();
		if (!visited[x]) {
			vector<int> v;
			dfs2(x, v);
			SCC.push_back(v);
		}
	}

	initialize();

	for (int i = 0; i < SCC.size(); i++) {
		for (int j = 0; j < SCC[i].size(); j++) {
			int x = SCC[i][j];
			if (x > N) {
				if (visited[x] || visited[x - N]) {
					cout << 0;
					return;
				}
			}
			else {
				if (visited[x] || visited[x + N]) {
					cout << 0;
					return;
				}
			}
			visited[x] = true;
		}
		for (int j = 0; j < SCC[i].size(); j++) {
			visited[SCC[i][j]] = false;
		}
	}

	cout << 1;
}

int main()
{
	ios_base::sync_with_stdio(false); cin.tie(0); cout.tie(0);

	solve();

	return 0;
}