Computer >> 컴퓨터 >  >> 프로그래밍 >> C++

C/C++로 이해하는 2-SAT(2-만족도) 문제: 개념부터 의사코드까지

2-SAT 문제란?

2-SAT(2-만족도, 2-Satisfiability) 문제는 각 절(clause)이 정확히 두 개의 리터럴로 구성된 부울 논리식이 참(true)이 되도록 변수에 값을 배정할 수 있는지를 판단하는 고전적인 알고리즘 문제입니다. 다음 형태의 논리식 f를 생각해 보겠습니다.

f = (x1 ∨ y1) ∧ (x2 ∨ y2) ∧ ... ∧ (xn ∨ yn)

문제는 단순합니다. "f를 만족시키는 변수 값의 조합이 존재하는가?"

절을 함축 명제로 바꾸기

핵심 아이디어는 논리학의 동치 관계를 활용하는 것입니다. 절 xi ∨ yi는 다음 두 명제와 서로 동치입니다.

  • ¬xi → yi : "xi가 거짓이라면 yi는 반드시 참이다"
  • ¬yi → xi : "yi가 거짓이라면 xi는 반드시 참이다"

즉, 각 절 (xi ∨ yi)을 이 두 함축 명제로 변환하는 것입니다.

함의 그래프(Implication Graph) 구성

이제 2n개의 정점을 갖는 방향 그래프를 만듭니다. 각 변수 xi에 대해 xi와 ¬xi, 즉 참과 거짓 두 상태를 정점으로 두는 방식입니다. 그리고 각 절 (xi ∨ yi)마다 다음 두 개의 방향 간선을 추가합니다.

  • ¬xi → yi
  • ¬yi → xi

판정 조건: 강연결요소(SCC)

그래프가 준비되면 만족 여부 판정은 간단해집니다. 어떤 변수 xi에 대해 xi와 ¬xi가 같은 강연결요소(Strongly Connected Component, SCC)에 속한다면, "xi = 참"과 "xi = 거짓"이 서로를 함의하게 되어 모순이 발생합니다. 따라서 이 경우 f는 만족 불가능(unsatisfiable)입니다.

값 배정: 위상 정렬 활용

f가 만족 가능하다고 판정되었다면, 이번에는 실제로 각 변수에 값을 배정해야 합니다. 이때는 앞서 구성한 그래프의 정점들을 위상 정렬(topological sort)하면 됩니다. 규칙은 다음과 같습니다.

  • 위상 정렬 순서에서 ¬xi가 xi보다 뒤에 위치하면 → xi = FALSE
  • 그렇지 않으면 → xi = TRUE

의사코드(Pseudo Code)

아래는 코사라주(Kosaraju) 알고리즘 방식으로 SCC를 구한 뒤, 이를 바탕으로 2-SAT을 판정하는 전체 흐름입니다.

func dfsFirst1(vertex v1):
    marked1[v1] = true
    for each vertex u1 adjacent to v1 do:
        if not marked1[u1]:
            dfsFirst1(u1)
    stack.push(v1)

func dfsSecond1(vertex v1):
    marked1[v1] = true
    for each vertex u1 adjacent to v1 do:
        if not marked1[u1]:
            dfsSecond1(u1)
    component1[v1] = counter

// 그래프 구성: 각 절을 두 개의 함축 간선으로 변환
for i = 1 to n1 do:
    addEdge1(not x[i], y[i])
    addEdge1(not y[i], x[i])

// 첫 번째 DFS로 정점들의 종료 순서 기록
for i = 1 to n1 do:
    if not marked1[x[i]]:
        dfsFirst1(x[i])
    if not marked1[y[i]]:
        dfsFirst1(y[i])
    if not marked1[not x[i]]:
        dfsFirst1(not x[i])
    if not marked1[not y[i]]:
        dfsFirst1(not y[i])

set all marked values false
counter = 0
flip directions of edges // v1 -> u1 간선을 u1 -> v1으로 변경

// 스택 순서대로 역방향 그래프에서 DFS 수행하여 SCC 번호 부여
while stack is not empty do:
    v1 = stack.pop
    if not marked1[v1]:
        counter = counter + 1
        dfsSecond1(v1)

// 변수와 그 부정이 같은 SCC에 있으면 만족 불가능
for i = 1 to n1 do:
    if component1[x[i]] == component1[not x[i]]:
        it is unsatisfiable
        exit
    if component1[y[i]] == component1[not y[i]]:
        it is unsatisfiable
        exit

it is satisfiable
exit

마무리: 시간 복잡도

이 방법은 DFS를 두 번 수행하는 구조이므로, 정점 V개와 간선 E개를 기준으로 O(V + E)의 시간 복잡도로 동작합니다. 일반적인 SAT 문제가 NP-완전인 것과 달리, 절의 크기가 2로 제한된 2-SAT은 그래프 탐색만으로 선형 시간 안에 해결할 수 있다는 점이 가장 큰 특징입니다.