[백준/11280/11281] 2-SAT - 3 / 4 (Python)

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

11280번: 2-SAT - 3

 

Problem 2 : https://www.acmicpc.net/problem/11281

11281번: 2-SAT - 4

 

Difficulty : Platinum 4

 

Status : Solved

 

Time : 00:44:47(problem 1)

 

---

 

문제 설명

 

 

2-SAT은 N개의 불리언 변수 x_1, x_2, ..., x_n가 있을 때, 2-CNF 식을 true로 만들기위해 x_i를 어떤 값으로 정해야하는지를 구하는 문제이다.

2-CNF식 (x or y) and ( ~y or z ) and ( x or ~z ) and ( z or y ) 와 같은 형태이다. 여기서 괄호로 묶인 식을 절(clause)라고 하는데, 절은 2개의 변수를 or한 것으로 이루어져 있다. 

변수의 개수 N과 절의 개수 M, 그리고 식 f가 주어졌을 때, 식 f를 true로 만들 수 있는지 없는지를 구하는 프로그램을 작성하시오.

예를 들어, N = 3, M = 4이고, f = ( ~x_1 or x_2 ) and ( ~x_2 or x_3 ) and ( x_1 or x_3 ) and ( x_3 or x_2 ) 인 경우에 x_1을 false, x_2을 false, x_3를 true로 정하면 식 f를 true로 만들 수 있다. 하지만, N = 1, M = 2이고, f =( x_1 or x_1 ) and ( ~x_1 or ~x_1 ) 인 경우에는 x_1에 어떤 값을 넣어도 식 f를 true로 만들 수 없다.

 

 

입력 및 출력

 

입력

 

첫째 줄에 변수의 개수 N (1 ≤ N ≤ 10,000)과 절의 개수 M (1 ≤ M ≤ 100,000)이 주어진다. 둘째 줄부터 M개의 줄에는 절이 주어진다. 절은 두 정수 i와 j (1 ≤ |i|, |j| ≤ N)로 이루어져 있으며, i와 j가 양수인 경우에는 각각 x_i, x_j를 나타내고, 음수인 경우에는 ~x_{-i}, ~x_{-j}를 나타낸다.

 

출력

 

첫째 줄에 식 f를 true로 만들 수 있으면 1을, 없으면 0을 출력한다.

 

입력 예시

 

3 4
-1 2
-2 3
1 3
3 2

 

출력 예시

 

1

 

 

---

 

풀이

 

배우면서 풀었던 문제. SCC가 핵심이었다..!

 

x or y 는 ~x -> y 혹은 ~y -> x의 명제의 형태로 나타낼 수 있다. x or y가 true가 되어야 한다고 가정하자.

 

• 만약 x가 false라면(~x) y는 반드시 true여야 한다.
• 만약 y가 false라면(~y) x는 반드시 true여야 한다.

즉 명제의 형태로 나타낼 수 있으며, 이들 명제는 하나의 그래프로 취급할 수 있다.

그렇다면 그 그래프 내에 강한 연결 요소(SCC)가 있다고 가정하자. 그 요소들을 이루는 임의의 노드 x, y는 x -> y는 y -> x 역시 성립한다. 따라서 둘 모두 참이거나 모두 거짓이어야 한다. 즉 x와 그 부정형 ~x가 모두 강한 연결 요소 안에 포함되어 있다면 모순이 발생하므로, 식 f를 절대 true로 만들 수 없다.

 

그렇다면 모든 N개의 정수와 그 부정형 정수 N개, 즉 2N개에 대해 SCC를 모두 찾고, 각 노드와 부정 노드가 같은 SCC에 속하는지 검사하기만 하면 된다. 본 풀이에는 타잔 알고리즘을 사용하였다.

 

p.s. 이 문제를 한번 보자.

 

2023.09.13 - [알고리즘 문제/백준] - [백준/11266] 단절점 (Python)

[백준/11266] 단절점 (Python)

 

타잔 알고리즘의 핵심은 노드에서 접근 가능한 모든 다음 노드들의 최소 순번을 반환하고, 이 최소 순번이 자신과 동일하다면 SCC가 존재한다는 의미(즉 우회로가 존재)를 이용한다. 즉 연결 요소를 이용하는 알고리즘으로, 바로 위에 소개하는 문제와 유사한 알고리즘으로 풀 수 있다.

 

풀이 코드

from collections import defaultdict
import sys
sys.setrecursionlimit(100000)
input = sys.stdin.readline
MAX = float('inf')

N, M = map(int, input().split())
edge_dict = defaultdict(list)

def cvt(a) :
  if a < 0 :
    return -a-1+N
  else :
    return a-1

def neg(a) :
  return (a + N) % (2*N)

for _ in range(M) :
  a, b = map(int, input().split())
  a = cvt(a)
  b = cvt(b)
  edge_dict[neg(a)].append(b)
  edge_dict[neg(b)].append(a)

visited = [MAX]*(2*N)
finished = [False]*(2*N)
stk = list()
scc_result = [-1]*(2*N)
idx, scc_idx = 0, 0

def dfs(node) :
  global idx, scc_idx
  visited[node] = result = idx
  idx += 1
  stk.append(node)

  for nxt in edge_dict[node] :
    if finished[nxt] :
      continue
    if visited[nxt] < MAX :
      result = min(result, visited[nxt])
      continue
    result = min(result, dfs(nxt))

  if result == visited[node] :
    while stk :
      n = stk.pop()
      finished[n] = True
      scc_result[n] = scc_idx
      if n == node :
        break
    scc_idx += 1
  return result

for i in range(2*N) :
  if not finished[i] :
    dfs(i)

for i in range(N) :
  if scc_result[i] == scc_result[neg(i)] :
    print(0)
    exit()
print(1)

풀이 완료!

 

 

---

 

2-SAT-4 문제 역시 핵심은 동일하므로 이 글에 같이 기술하도록 한다. 여기서는 추가로, 만약 가능할 경우 그 조합 중 하나를 같이 표기해야 한다는 전제조건을 꼽았다. 즉 이에 대한 추가적인 구현이 필요하다.

 

scc 알고리즘은 스택을 이용하므로, 스택의 특성상(LIFO) 넘버링이 클수록 더 초기에 방문한 SCC 요소가 된다. 즉 SCC의 순서는 위상 정렬 결과의 역순과 동일하다.

 

그 다음은 명제를 매핑할 차례이다. ~x OR y라는 명제가 존재한다고 가정하자. 이는 x -> y의 꼴로 나타낼 수 있다.

 

우리는 식 f가 참임을 알고 있으므로 위 명제를 참으로 만드는 x, y값을 찾아야 한다. 여기서 (~x, y) = (F, F)인 경우, 즉 T -> F 인 경우가 유일하게 거짓이 됨을 알 수 있다. 또한 앞선 값이 F인 경우 어떤 경우에서든 참을 만족한다. 즉 그리디하게, 우선적으로 위상이 높은 노드들을 방문하며, 만약 방문하지 않은 점이라면 False를 그리디하게 매핑한다. 여기서 한 가지 당연한 전제를 살펴보자. 어떤 노드 n과 그 부정형인 ~n은 서로 반대의 값을 가진다. 즉 동시에 그 negative 값에는 True를 매핑한다. 즉 위상 정렬 순으로 SCC 노드들을 방문하며 위 전략을 사용하는 게 첫 번째 방법이다.

 

두 번째 방법은 좀 더 쉽다. 각 노드들을 체크하며, 노드와 그 부정값 중 더 SCC 위상 정렬 결과 앞에 오는 값을 0으로, 다른 값을 1로 초기화하면 된다. 이 방법이 어떻게 성립하는지 한번 사고 실험을 진행해보자.

 

x -> y가 성립하는 임의의 x, y를 뽑자. 그렇다면 ~y -> ~x 역시 대우명제로 성립하고, 각 scc 위상 정렬 결과를 나타낸다면 scc(x), scc(y), scc(~x), scc(~y) 가 성립한다. 

 

명제와 대우명제 관계에 있는 두 SCC 그래프는 항상 대칭형을 띄고, 명제의 필요조건은 위상 정렬상 충분조건보다 항상 앞에 온다. 즉 scc(x) <= scc(y)이며 동시에 scc(~y) <= scc(~x)가 성립한다. 또한 대칭되는 두 SCC 그래프의 간선은 존재하지 않고, 우리는 DFS로 SCC 요소들을 검색했으므로,

 

• scc(x) <= scc(y) < scc(~y) <= scc(~x) 혹은
• scc(~y) <=  scc(~x) < scc(x) <= scc(~y)

 

두 가지 경우만이 존재한다.

 

• 첫 번째 경우는 x = y = F, ~x = ~y = T가 되어 앞선 명제는 F -> F, T -> T 꼴이 된다. 즉 두 명제 모두 참을 만족한다.
• 두 번째 경우는 ~x = ~y = T, x = y = T가 되어 앞선 명제는 T -> T, F -> F 꼴이 된다. 역시 두 명제 모두 참을 만족한다.

즉 부등호 비교만으로도 매핑이 가능하다!

 

풀이 코드

from collections import defaultdict
import sys
sys.setrecursionlimit(100000)
input = sys.stdin.readline
MAX = float('inf')

N, M = map(int, input().split())
edge_dict = defaultdict(list)

def cvt(a) :
  if a < 0 :
    return -a-1+N
  else :
    return a-1

def neg(a) :
  return (a + N) % (2*N)

for _ in range(M) :
  a, b = map(int, input().split())
  a = cvt(a)
  b = cvt(b)
  edge_dict[neg(a)].append(b)
  edge_dict[neg(b)].append(a)

visited = [MAX]*(2*N)
finished = [False]*(2*N)
stk = list()
scc_result = [-1]*(2*N)
idx, scc_idx = 0, 0

def scc(node) :
  global idx, scc_idx
  visited[node] = result = idx
  idx += 1
  stk.append(node)

  for nxt in edge_dict[node] :
    if finished[nxt] :
      continue
    if visited[nxt] < MAX :
      result = min(result, visited[nxt])
      continue
    result = min(result, scc(nxt))

  if result == visited[node] :
    while stk :
      n = stk.pop()
      finished[n] = True
      scc_result[n] = scc_idx
      if n == node :
        break
    scc_idx += 1
  return result

for i in range(2*N) :
  if not finished[i] :
    scc(i)

result = [0]*N
for i in range(N) :
  if scc_result[i] == scc_result[neg(i)] :
    print(0)
    exit()
  if scc_result[i] < scc_result[neg(i)] :
    result[i] = 1
print(1)
print(*result[:N])

풀이 완료!