2-SAT

작성일 | In |

2-SAT(2-Satisfiability)

지난 글에서 예고한대로 2-SAT 문제에 대해 정리합니다.

먼저 이를 이해하려면 몇 가지 짚고 넘어가야 할 게 있어요.

  • CNF(Conjunctive Normal Form) : 논리합(∨)으로 이뤄진 절(clause)을 논리곱(∧)으로 나타난 식.

  • k-SAT 문제 : 최대 k개의 불리언 값을 가지는 변수가 존재하는 절로 CNF 구조를 형성한 논리식을 충족하는 경우를 찾는 것.

따라서 2-SAT 문제는 아래와 같은 식의 결과를 true로 만들 수 있는지 여부와, 만약 가능하다면 이를 충족하는 경우를 구하는 것이라고 생각하면 되겠습니다.

f = (a ∨ b) ∧ (c ∨ d) ∧ (e ∨ f)


True / False?

그런데 전체 식이 참이려면 어떤 조건이 충족되어야 하나요? 우선 전체 식이 참이 되려면 각각의 절이 모두 참이면 됩니다. 그리고 각각의 절, 그러니까 OR 연산자(∨)로 묶인 (a ∨ b) 절이 참이 되려면 a와 b 변수 중 적어도 하나가 참이면 됩니다.

결국 2-SAT 문제에서 식을 만족시키는 값을 찾으려면 조건문을 만들어 봐야 합니다. 아래와 같은 식을 예로 들겠습니다.
(x ∨ y) ∧ (¬y ∨ ¬z) ∧ (¬x ∨ ¬z) ∧ (z ∨ y)

첫 번째 절이 참이 되려면 x 또는 y가 반드시 참이여야만 합니다. 다시 말하자면 x가 거짓이라면 y는 참이고, y가 거짓이라면 x가 참입니다. 이를 명제로 나타내면 ¬x -> y, ¬y -> x인데요, 이처럼 우리는 각 절마다 두 개의 명제를 이끌어낼 수 있습니다.

위의 식에서는 8개의 명제를 얻을 수 있어요.

  • ¬x -> y
  • ¬y -> x
  • y -> ¬z
  • z -> ¬y
  • x -> ¬z
  • z -> ¬x
  • ¬z -> y
  • ¬y -> z

그리고 명제를 이루는 각각의 값을 정점으로 삼는다면 그래프를 만들 수 있습니다.

각 노드의 왼쪽 상단의 숫자는 DFS 방문 순서입니다. 물론 이는 그래프 제작 코드에 따라 달라질 수 있습니다만, 아무튼 이처럼 유향 그래프를 그려보면 강한 연결 요소 개념이 왜 필요한지 알 수 있을 거예요.


우선, 우리는 명제를 기반으로 그래프를 그렸기 때문에 간선으로 서로 이어진 양쪽 노드는 모두 같은 값(참 또는 거짓)을 가질 것입니다. 또한 이러한 논리 흐름에 따라서 같은 SCC(Strongly Connected Component), 그러니까 사이클 내에 속해 있는 노드들은 모두 똑같은 값을 가져야 합니다. 그리고 당연하게도 만약 a와 ¬a가 같은 사이클 내에 있다면 이는 모순입니다. 둘 다 동시에 참이거나 거짓일 수는 없을테니까요. 이제 왜 강한 연결 요소 알고리즘이 필요한지 아시겠나요? SCC 내부에 모순되는 상황이 발생한다면 전체 식 f 의 결과를 true로 만들 수 없다는 뜻입니다. 우리는 SCC 개념을 이용해서 2-SAT 문제를 풀 수 있습니다.

정리 1.
같은 SCC 안에 있는 정점들은 모두 똑같은 값을 가진다.


식 f 를 true로 만드는 변수값은 어떻게 구하는데?

변수값을 구하는 과정을 이해하려면 먼저 명제 논리 조건문에 대한 이해가 필요합니다.

정리 2.
만약 P -> Q 라는 명제에서 P가 거짓이라면 Q가 어떤 값을 가지든 해당 명제는 참이지만, P가 참이라면 Q도 참이어야 전체 명제가 참이 된다.
P가 참이고 Q가 거짓인 경우에만 명제가 거짓이다.

그렇다면 정리 1과 정리 2에 따라 다음과 같은 결론을 내릴 수 있습니다.

  1. SCC P와 Q가 있을 때, 각각의 SCC 내부에 있는 정점들은 참이든 거짓이든 모두 똑같은 값을 가질 것이다.
  2. SCC P에서 Q로 가는 간선이 존재해서 P -> Q가 성립한다면, P를 참이라고 두었을 때 Q도 반드시 참이어야 한다.
  3. 다시 말해서 SCC 단위로 그래프를 탐색할 때, 어떤 정점 x를 처음 만났다면 그 값은 일단 false로 설정하는 게 좋다. 그래야 명제를 해치지 않는다.

무슨 말인지 안 와닿는다구요? 아마 그림을 다시 보면 이해가 잘 될 거예요.

예를 들어 x를 먼저 방문한다면 SCC 2의 x를 false로 둡니다. 다음으로 만약 SCC 1의 y와 ¬z를 방문한다고 가정하면 이 아이들도 false로 설정합니다. 그렇다면 SCC 2 -> SCC 1은 false -> false라서 문제가 없습니다. 그리고 SCC 4 -> SCC 3도 true -> true이라서 문제가 없습니다. 오…이게 되네

근데 그거 앎? 강한 연결 요소 알고리즘을 곰곰이 생각해보면 SCC를 발견하는 순서대로 번호를 매겼으니 당연히 SCC 번호가 큰 것에서 작은 것으로 탐색한다면 이는 DFS 방문순서랑 일치합니다. 그러니까 위에서 설명할 때 말한 SCC 단위로 세운 명제 P -> Q에서 SCC P의 번호가 Q보다 큽니다. 따라서 새로운 결론을 내릴 수 있는데요.

정리 3.
정점 1부터 끝까지 차례로 방문하면서 어떤 정점이 속한 SCC의 번호가 그 정점의 not형이 속한 SCC 번호보다 크다면 해당 정점의 값을 false로 설정한다. 반대의 경우에는 true로 설정한다.


마치며

개인적으로 대부분의 2-SAT 문제가 정체를 알기 어렵다는 생각이 듭니다. 아마 문제 태그를 보지 않았다면 2-SAT 문제라는 것을 알아차리지 못했을 거예요. 그래프의 정점으로 만들 수 있는 대상마다 두 가지의 선택지가 있고, 그 중 하나는 만족해야 하는 상황이라면 2-SAT 문제라고 보면 될 것 같습니다. 어떤 문제는 그래프를 구성하는 과정을 더 까다롭게 만들어 놓은 경우도 있습니다. 앞서 언급한 것처럼 일반적으로 2-SAT 식은 OR로 결합된 절들을 AND로 묶은 구조입니다. 그런데 이와 달리 구조가 반대로 된 케이스로 조건이 주어지는 문제도 있었습니다. 그래서 해당 문제를 풀 때 저는 논리식을 익숙한 구조로 재구성 해야 했습니다.


2-SAT 문제를 공부하다보니 글을 두 개나 쓰게 됐네요. 미래의 제가 다시 읽었을 때 이해가 잘 되면 좋겠습니다.


예시 코드

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

# n은 불리언 값을 가질 변수의 개수, m은 절의 개수
n, m = map(int, input().split())

edge = [[] for i in range(2*n+1)]
for i in range(m):
    a, b = map(int, input().split())
    edge[-a].append(b)
    edge[-b].append(a)
    
    
stack = []
num = [0] * (2*n+1)
check = [0] * (2*n+1)
group = [0] * (2*n+1) # 소속된 SCC 그룹 기록.

count = 1
scc_num = 1 # SCC 번호


# 강한 연결 요소 함수
def sol(x):
    global count, scc_num
    
    num[x] = count
    stack.append(x)
    
    count += 1
    head = num[x]
    
    for i in edge[x]:
        if not num[i]:
            head = min(head, sol(i))
            
        elif not check[i]:
            head = min(head, num[i])
            

    if head == num[x]:
        while True:
            t = stack.pop()
            check[t] = 1
            group[t] = scc_num
            
            if t == x:
                break
            
        scc_num += 1
        
    
    return head
        
        
for i in range(1, 2*n+1):
    if not num[i]:
        sol(i)
        
flag = 1
value = [0] * (n+1) # 식 f를 true로 만드는 x 논리값 기록.

for i in range(1, n+1):
    if group[i] == group[-i]:
        flag = 0
        break # 같은 사이클(SCC) 내에 a와 ¬a가 함께 있다면 모순이니 불가하다.
        
    elif group[i] < group[-i]:
        value[i] = 1
    # 정점이 속한 SCC 번호가 그 정점의 not형이 속한 SCC 번호보다 작다면 명제 P -> Q 구조에서 Q에 해당한다.
    # 명제 논리에 따라 명제가 참이 되려면 P쪽을 false로 두는 게 편하기에 Q에 해당하는 현재 value[i]의 값은 자연스럽게 1이 된다.
        
        
print(1 if flag else 0)
if flag: print(*value[1:])