
2-SAT은 N개의 불리언 변수 (x_1, x_2, ..., x_n)가 있을 때, 2-CNF 식을 true로 만들기위해 (x_i)를 어떤 값으로 정해야하는지를 구하는 문제이다. 이번 문제는 변수의 개수 N과 절의 개수 M, 그리고 식 (f)가 주어졌을 때, 식 (f)를 true로 만들 수 있는지 없는지를 구하는 프로그램을 작성하는 문제이다.
타잔 알고리즘
모든 정점에 대해 DFS를 수행하여 SCC를 찾는 알고리즘으로, 코사라주 알고리즘에 비해 적용이 더 쉽다.
1) 인접 정점에 방문하여 자기 자신을 스택에 넣고, 재귀적으로 DFS를 수행한다.
2) 인접 정점에 방문했지만, 아직 처리중인 상태일 경우, 작은 값으로 부모값을 갱신한다.
3) 부모 노드의 DFS가 끝난 경우에는, 자신의 id값이 스택에서 나올 때까지 스택에 있는 노드들을 pop하고 scc 배열에 추가한다.
4) 만들어진 하나의 scc를 전체 scc 배열에 추가한다. (구현이 어렵지만, 활용도는 더 높다고 한다.)
코사라주 알고리즘
주어진 방향 그래프의 역방향 그래프와 스택을 사용하여 SCC를 구하는 알고리즘이다. 방향, 역방향 그래프가 동일한 SCC를 구성한다는 것을 이용한 방법이다.
1) 주어지는 방향 그래프와 그 그래프의 역방향 그래프를 만든다.
2) 정점을 담을 스택을 만들고 임의의 정점부터 DFS를 수행한다.
3) DFS가 끝나는 순서대로 스택에 삽입하고, 아직 방문하지 않은 정점에 대해 DFS를 수행한다.
4) 모든 정점이 스택에 담긴 후에는 스택을 pop하여 나오는 정점부터 역방향 그래프에서 DFS를 수행한다. 이미 방문한 정점은 pop만 시행한다.
5) 이때 탐색되는 모든 정점을 SCC로 묶는다.
이것을 스택이 빌 때까지 진행한다.