Satisfiability Problem

Satisfiability Problem

만족 가능성 문제(Satisfiability Problem)는 주어진 논리식을 참으로 만들 수 있는지 판별하는 문제이다. 만족 가능성 문제는 컴퓨터 과학에서 중요한 문제이자 어려운 문제로 다뤄지고 있으며, 문제를 풀기 위한 제약 조건 설정 등의 연구가 진행되어왔다.

이 글에서는 다음 용어들을 정의하며 문제 내에서 특별한 설명이나 재정의를 하지 않는 경우 아래 정의를 따른다.

• 논리 변수(Boolean variable): 참 또는 거짓의 값을 가지는 변수.
• 리터럴(Literal): 어떠한 논리 변수 $x$(양의 리터럴), 또는 이의 부정 $\neg x$(음의 리터럴)을 의미한다.
• 절(Clause): 1개 이상의 리터럴을 OR로 연결한 식을 의미한다. 절의 크기는 절 안에 있는 리터럴의 개수이다.
• 항(Term): 절 안에 있는 각각의 리터럴을 의한다.
• CNF(Conjunctive Normal Form): 1개 이상의 절을 AND로 연결한 식이다. 모든 논리식은 다항시간 내에 CNF로 변환 가능하다.

$N$개의 논리 변수 $x_1$부터 $x_N$까지에 참 또는 거짓을 배정하는 방식을 순서대로 간단히 [참, 거짓, 거짓, 참]과 같은 방식으로 표현할 것이다.

예로, $x_1, x_2$를 논리 변수라고 하자. 그러면 리터럴은 $x_1, x_2, \neg x_1, \neg x_2$가 된다. 이 중 $x_1, x_2$를 양의 리터럴, $\neg x_1, \neg x_2$를 음의 리터럴이라 한다. 이러한 리터럴을 OR로 연결한 식 $(x_1 \lor \lnot x_2)$나 $(x_1 \lor x_1 \lor \lnot x_1)$은 절이 되며, 각각의 크기는 2와 3이다. 이제 이러한 절들을 AND로 연결한 식 $(x_1 \lor \lnot x_2) \land (x_1 \lor x_1 \lor \lnot x_1)$는 CNF가 된다. 이러한 CNF 식이 주어질 때, 이의 논리 변수 $x_1, x_2$에 참 또는 거짓을 적절히 배정하여 식을 참으로 만드는 것이 목적이다.

이 글에선 CNF 식의 만족 가능성 문제를 다항 시간에 풀 수 있는 제약들에 대해 다뤄볼 것이다.

Positive

이 문제에서는 식에 사용되는 모든 리터럴이 양의 리터럴이다.

ex1: $(x_1 \lor x_2) \land (x_1 \lor x_3 \lor x_4) \land (x_2 \lor x_2 \lor x_1) \to$ [참, 거짓, 참, 거짓]
ex2: $(x_1 \lor x_1 \lor x_1 \lor x_1) \to$ [참]

모든 리터럴이 양의 리터럴이기 때문에 매우 간단하다. 풀이는 모든 리터럴이 양의 리터럴이기 때문에, 모든 논리 변수를 참으로 설정하면 된다. 반대로 Negative문제는 모든 리터럴이 음의 리터럴 이므로 모든 논리 변수를 거짓으로 설정하면 된다.

1-SAT

이 문제에서는 모든 절의 크기가 1이다.

ex1: $(x_1) \land (\lnot x_2) \land (\lnot x_5) \land (x_4) \to$ [참, 거짓, 참, 참, 거짓]
ex2: $(x_1) \land (x_2) \land (\lnot x_1) \to$ 불가능

주어진 식은 리터럴들의 AND로 이루어진 식으로 볼 수 있다. 만약 어떤 논리 변수 $x$에 대해, $x$와 $\lnot x$가 식에 같이 존재한다면 답은 불가능이다. 그렇지 않다면 음의 리터럴은 거짓으로, 양의 리터럴은 참으로 만들면 된다.

DNF-SAT

이 문제에서는 식에 제약 조건을 걸지 않는다. 대신 조금 다른 찾는데, CNF 식을 참으로 만드는 것이 아니라 거짓으로 만드는 논리 변수의 배정 방식을 찾는다.

ex1: $(x_1 \lor x_3) \land (x_2 \lor \lnot x_3 \lor \lnot x_2) \to$ [거짓, 참, 거짓]
ex2: $(x_1 \lor \lnot x_1) \to$ 불가능

여러 개의 절을 AND로 연결한 식을 거짓으로 만들기 위해서는 절 하나만 거짓으로 만들면 된다. 어떠한 절은 여러 개의 리터럴을 OR로 연결한 형태이므로, 이를 거짓으로 만들기 위해서는 모든 리터럴을 거짓으로 만들어야 한다.

이를 다르게 생각해보면, 모든 리터럴을 참으로 만들어야 하는 1-SAT와 비슷한 문제이다. (드모르간 법칙)

따라서 주어진 절 중 1-SAT로 풀 수 있는 절이 있다면, 해당 절을 1-SAT처럼 풀어서 거짓으로 만들어주면 된다. 만약 그러한 절이 존재하지 않다면, 답은 불가능이다.

CNF 식은 OR을 AND로 묶은 형태이다. 여기에 NOT을 취하면 드모르간 법칙에의해 AND를 OR로 묶은 형태가 되며 이를 DNF라고 부른다. 이 문제에서 볼 수 있듯, DNF 식은 선형 시간에 풀 수 있다.

2-Affine

이 문제에서는 절을 조금 다르게 정의할 것이다.

• 절: 1개 이상의 리터럴을 XOR로 연결한 식을 의미한다.

또한 이 문제에서는 모든 절의 크기가 2이다.

ex1: $(x_1 ⊕ \lnot x_2) \land (x_3 ⊕ \lnot x_3) \land (x_1 ⊕ x_3) \to$ [참, 참, 거짓]
ex2: $(x_1 ⊕ x_2) \land (x_1 ⊕ \lnot x_2) \to$ 불가능

어떤 절을 참으로 만들기 위해서는 $(a ⊕ b)$ 두 변수 중 정확히 하나만 참이어야 한다. 또한 모든 논리 변수 $x$에 대해 이의 양의 리터럴 $x$과 음의 리터럴 $\lnot x$ 중 정확히 하나만 참이다.

따라서 주어진 문제는 아래 조건을 만족하도록 $2N$개의 리터럴 중 일부를 적절히 선택하는 문제가 된다.

1. $(a ⊕ b)$: 리터럴 a와 리터럴 b 중 정확히 한 개만 선택되어야 한다.
2. 논리 변수 $x$에 대해 이의 양의 리터럴 $x$과 음의 리터럴 $\lnot x$ 중 정확히 하나만 선택되야 한다.

“선택된다”를 “참으로 만든다”라고 생각하면 된다.

이러한 문제는 이분 그래프(Bipartite Graph)로 풀 수 있다. $2N$개의 리터럴을 각각 정점으로 하는 무방향 그래프를 만든다.

변수 $N$개: $x_1, x_2, \cdots, x_N$ $\to$ 노드 $2N$개 : $x_1, \lnot x_1, x_2, \lnot x_2, \cdots, x_N, \lnot x_N$

1. 각각의 $(a ⊕ b)$에 대해, $a$와 $b$를 간선으로 연결한다. 이분 그래프이므로 둘의 값이 달라야 한다는 의미이다.
2. 그리고 각 논리 변수 $x$에 대해, $x$와 $\lnot x$를 간선으로 연결한다. 마찬가지로 이 둘 역시 달라야 한다.

이렇게 해서 만들어진 그래프를 이분 그래프에 따라 인접한 정점끼리 서로 다른 색이 되도록 2개의 색으로 칠한다.

만약 제대로 된 색칠을 찾을 수 있다면, 해당 색칠이 그대로 답이 된다. 색칠된 리터럴을 참으로 만들고, 그렇지 않은 리터럴을 거짓으로 만든다.

그러한 색칠이 만약 존재하지 않다면, 해당 그래프는 이분 그래프가 아니기 때문에 홀수 사이클이 존재한다. 이러한 홀수 사이클을 $C[0] \to C[1] \to C[2] \to \cdots \to C[k]=C[0]$라고 하자. 정의상 $k$는 홀수이다. 각각의 간선은 XOR을 의미하기 때문에 아래가 성립한다.

\[\begin{align} C[0]&=C[0] \\ C[1]&=\lnot C[0] \\ C[2]&=C[0] \\ C[3]&=\lnot C[0] \\ &\vdots \\ C[k]&=\lnot C[0]=C[0]..? \end{align}\]

따라서 식에 모순이 있다는 의미가 되고 답은 불가능이 된다. ex2를 예시로 Bipartite Graph를 그려보면 $x_1 \to x_2 \to \lnot x_2 \to x_1$ 사이클이 존재하여 불가능이 됨을 확인할 수 있다.

Weakly Positive

이 문제에서는 모든 절에 대해 절 안에 있는 음의 리터럴의 개수가 최대 1개이다.

ex1: $(x_1 \lor x_2) \land (\lnot x_1 \lor x_3 \lor x_4) \land (x_1 \lor \lnot x_3 \lor x_3 \lor x_4) \to$ [거짓, 참, 참, 참]
ex2: $(\lnot x_1) \land (x_1 \lor x_2) \land (\lnot x_2 \lor x_1) \to$ 불가능

문제의 특성상 대부분의 리터럴이 양의 리터럴이므로 다음과 같은 생각을 할 수 있다.

모든 논리 변수를 참으로 놓고 시작한다. 어떠한 절이 거짓이 된다면, 해당 절의 음의 리터럴에 해당하는 변수를 거짓으로 만든다. 만약 이러한 음의 리터럴이 없다면, 식을 참으로 만드는 배정이 불가능하다.

과정을 좀 더 엄밀히 적으면 다음과 같다.

1. 모든 논리 변수 $x_1, x_2, \cdots, x_N$을 참으로 놓고 시작한다.