2-SAT

2-SAT

2-SAT 문제는 여러개의 절(Clause)로 이루어진 논리식이 성립할 수 있는지를 판별하는 문제로, 적어도 두개의 절이 주어졌을 때를 의미합니다.

이 식에서, $a = True, \; b = False, \; c = True$라면 성립합니다. 그러나 이런 식은 어떻게 될까요?

두번째 절에서, b는 False 여야합니다. 그러나, 첫번째 절에서 a 는 True 여야하고, 세번째 절에서 a 는 False여야하기 때문에 모순이 발생합니다. 그렇다면 이런 식이 성립하는지 판단하려면 어떻게 해야할까요? 우리는 OR로 연결된 식을 조건식으로 바꿀 수 있다는 점을 주목해야합니다. 부분집합과 조건문

그리고, $p\rightarrow q$에서, $p=True$라면 $q=True$여야합니다. 그러나 만약, $a\rightarrow\;\sim a$ 에서 $a$가 True 라면, $\sim a$또한 True여야하기 때문에 모순이 발생하는 것입니다. 이는 반대도 똑같습니다(if a = False, ~a must be True). 우리는 이러한 과정에서 $a\rightarrow \;\sim a$, $\sim a \rightarrow a$와 같은 식이 나오면 안된다는 것을 알 수 있습니다.

위의 식을 그래프로 표현하면 다음과 같습니다.

여기서, A노드에서 출발했을 때, ~B를 거쳐 ~A로 도달할 수 있기 때문에 모순이 발생하였습니다. 또한, ~A노드에서 B를 거쳐 A로 갈 수 있기 때문에 모순이 발생한다고 말할 수 있습니다.

그러나 이 그래프에서, ~A에서는 A에 도달할 수 있지만, A에서는 ~A에 도달할 수 없습니다. 그렇기 때문에 이 식은 참입니다.

정리하자면, ~N에서도 N에 도달할 수 있고, N에서도 ~N에 도달할 수 있다면, 그 식은 성립하지 않습니다. 즉, N와 ~N 사이에 사이클이 발생한다면, 그 식은 성립하지 않습니다. 사이클을 판단하는 알고리즘은 SCC를 사용하면 됩니다. 같은 SCC 집합에 ~N과 N이 속해있다면, 그 식은 성립하지 않는다는 것입니다.

Python 코드(BOJ 11280)

import sys

input = sys.stdin.readline
sys.setrecursionlimit(10**6)

# Kosaraju's Algorithm
def dfs(n):
    global num
    for vertex in graph[n]:
        if not visited[vertex]:
            visited[vertex] = True
            dfs(vertex)
    numbers[n][0] = num
    num += 1

def dfs2nd(n):
    group[n] = p
    for vertex in graph_inversed[n]:
        if not visited_inversed[vertex]:
            visited_inversed[vertex] = True
            dfs2nd(vertex)

v, e = map(int, input().split())
graph = {i:[] for i in range(-v, v + 1)}
graph_inversed = {i:[] for i in range(-v, v+1)}
visited = {i:False for i in range(-v, v+1)}
visited_inversed = {i:False for i in range(-v, v+1)}
numbers = {i:[0, i] for i in range(-v, v + 1)}
group = [0] * (2*v + 1)
num = 1
p = 0

for i in range(e):
    a, b = map(int, input().split())
    graph[-a].append(b)
    graph[-b].append(a)
    graph_inversed[b].append(-a)
    graph_inversed[a].append(-b)

for i in range(-v, v + 1):
    if i == 0:
        continue
    if not visited[i]:
        dfs(i)

por = sorted(numbers.values(), key = lambda x:x[0], reverse = True)

for i in por:
    if i[1] == 0: continue
    if not visited_inversed[i[1]]:
        visited_inversed[i[1]] = True
        dfs2nd(i[1])
        p += 1

flag = 1
for i in range(1, v+1):
    if i == 0: continue
    if group[i] == group[-i]:
        flag = 0
        break

print(flag)