[알고리즘/파이썬] 2-sat 알고리즘

https://www.acmicpc.net/problem/11280

11280번: 2-SAT - 3

 
위와 같은 문제가 2-sat 알고리즘이며 알고리즘 자체가 문제화되어있다.
2-sat이 무엇인지부터 설명하면 글이 매우 길어질 것이므로(나는 시간이 없다..)
해법에 대해 간략히 설명해보겠다.(기록을 위한 요약 설명이므로 부족하다면 다른 글을 같이 참고하자) 
 
2-SAT은 함수의 각 절이 AND조건으로 연결되어있기 때문에 모든 절이 True여야만 전체 함수가 True가 될 수 있다.
그리고 각 절은 OR조건으로만 연결되어있기 때문에 절 내의 항목 중 최소 하나는 True이어야 한다.
 
(x1 ^ x2) 라는 절을 생각해보자. 여기서 유의미한 명제를 이끌어 내야 하는데 아까 말했듯이 최소 하나가 참이어야 한다는 것에 초점을 맞추면 된다.
 
x1이 거짓이라면 x2는 참이어야만 한다. ---- (1)
x2가 거짓이라면 x1은 참이어야만 한다. ---- (2)
 
위의 두 명제가 반드시 성립하는 명제다. 참고로 x1이 참이라면 x2는 참, 거짓 상관이 없게 되므로 'x1이 참이라면'이라는 가정으로부터는 유의미한 명제를 도출할 수 없다. 
 
위의 두 명제를  -x1 → x2, -x2 → x1 으로 각각 표현하자. 여기서  -x1, x2, -x2, x1 을 각각 노드로 상정하고 화살표에 맞춰 간선을 그리면 하나의 그래프를 그려낼 수 있다. 
 
 
예시

 
참고로 그래프는 대칭형으로 나올 수밖에 없다. c -> a 는 즉슨 -a -> -c 이기 때문이다(대우 법칙),
 
그래프를 그린후 강한연결요소(SCC) 알고리즘을 사용하여 SCC끼리 묶어보자.
이때 위의 그림과 같이 하나의 SCC 안에 x, -x가 동시에 있지 않다면 이 그래프는 전체 함수 f를 참으로 만들 방법이 있다는 뜻이다. 하지만 하나의 SCC 안에 x, -x 가 동시에 있다면 x -> -x, -x -> x가 동시에 성립해야 한다는 의미가 되므로 이 자체는 모순이 되어 함수 f를 참으로 만들 방법이 존재할 수 없게 된다.
(참고로 x->-x라는 명제 하나만으로는 모순이 아니라고 한다.  참고: https://sevity.tistory.com/152 https://namu.wiki/w/%EB%AA%85%EC%A0%9C%20%EB%85%BC%EB%A6%AC#s-3.4)
 
 
 
https://www.acmicpc.net/problem/11281

11281번: 2-SAT - 4

 
여기서 더 나아가, 각 변수가 참/거짓 중 어떤 값을 가져야 하는 지 알 수 있다.
 
1. a -> b 명제가 있다고 할 때, a가 거짓이면 b는 참/거짓 상관없이 a -> b 명제는 참이다. 그래서 먼저 만나는 노드를 거짓으로 놓자.
2. 같은 SCC에 속하면 같은 참/거짓 값을 가진다.
3. SCC 알고리즘을 써서 구한 SCC 그룹은 이 그룹들을 담는 SCCS에 순차적으로 저장이 되는데, SCC 알고리즘은 기본적으로 dfs를 사용하는 알고리즘이라 늦게 저장된 SCC 그룹일수록 사실 위상정렬 순서 상 더 높은 위상 순번을 가진다. 그래서 SCCS를 역으로 순회하며 각 SCC를 조사하여 만나는 노드들을 우선적으로 거짓으로 놓으면 된다.
먼저 만난 -a를 거짓으로 놓았으면 나중에 만나게 될 a는 이미 값이 참으로 정해졌으므로 건너뛰고.. 대략 이런 방식이다.
 

import collections
import sys
sys.setrecursionlimit(10**5)

n, m = map(int, input().split())
graph = collections.defaultdict(list)
for _ in range(m):
    a, b = map(int, input().split())
    graph[-a].append(b)
    graph[-b].append(a)
sccs=[]
id = 0
stack = []
degree = [-1 for _ in range(2*n+1)]

def set_id():
    global id
    id += 1
    return id

def dfs(node):
    degree[node] = set_id()
    stack.append(node)
    parent = degree[node]
    for next in graph[node]:
        if degree[next] == -1:
            parent = min(parent, dfs(next))
        elif next in stack:
            parent = min(parent, degree[next])
    if parent == degree[node]:
        scc = []
        while True:
            e = stack.pop()
            scc.append(e)
            if e == node: break
        sccs.append(scc)
    return parent

for i in range(-n, n+1):
    if i == 0: continue
    if degree[i] == -1:
        dfs(i)

possible = True
for scc in sccs:
    for i in scc:
        for j in scc:
            if i + j == 0:
                possible = False
if possible: print(1)
else: print(0)

if possible:
    result = [-1 for i in range(2*n+1)]
    for scc in sccs[::-1]:
        for e in scc:
            if result[e] != -1:
                continue
            result[e] = 0
            result[-e] = 1
    print(*result[1:n+1])

 
위처럼 코드를 작성해 구현은 일단 했는데 음수 인덱스에 대한 테크닉도 아직 좀 부족하고 마지막에 possible 판별하는 알고리즘도 저게 최선인가..? 싶다. 최적화된 해법은 나중에 좀 더 알아보는걸로!!