2-SAT¶
SAT(불리언 충족 가능성 문제, Boolean satisfiability problem)는 주어진 불리언 논리식을 만족하도록 변수에 불리언 값을 할당하는 문제입니다. 불리언 논리식은 보통 CNF(논리곱 정규형, conjunctive normal form)로 주어집니다. CNF는 여러 절(clause)의 논리곱이며, 각 절은 리터럴(변수 또는 변수의 부정)의 논리합입니다. 2-SAT(2-충족 가능성, 2-satisfiability)는 SAT 문제에 제한을 둔 것으로, 2-SAT에서는 모든 절이 정확히 두 개의 리터럴을 가집니다. 다음은 이러한 2-SAT 문제의 예시입니다. 다음 논리식이 참이 되도록 하는 $a, b, c$의 할당을 구하십시오:
SAT는 NP-완전 문제이며, 이에 대해 알려진 효율적인 해법은 없습니다. 그러나 2-SAT는 $O(n + m)$에 효율적으로 풀 수 있습니다. 여기서 $n$은 변수의 개수이고 $m$은 절의 개수입니다.
알고리즘:¶
먼저 문제를 다른 형태, 이른바 함의 정규형(implicative normal form)으로 변환해야 합니다. 식 $a \lor b$는 $\lnot a \Rightarrow b \land \lnot b \Rightarrow a$와 동치라는 점에 주목하십시오(두 변수 중 하나가 거짓이면 다른 하나는 반드시 참이어야 합니다).
이제 이러한 함의들로 방향 그래프를 구성합니다: 각 변수 $x$마다 두 정점 $v_x$와 $v_{\lnot x}$가 있습니다. 간선은 함의에 대응합니다.
2-CNF 형태의 예시를 살펴봅시다:
방향 그래프는 다음과 같은 정점과 간선을 포함합니다:
다음 그림에서 함의 그래프를 볼 수 있습니다:
함의 그래프의 다음 성질에 주목할 필요가 있습니다: 간선 $a \Rightarrow b$가 있으면 간선 $\lnot b \Rightarrow \lnot a$도 있습니다.
또한 $\lnot x$에서 $x$에 도달할 수 있고 $x$에서 $\lnot x$에 도달할 수 있다면, 문제의 해가 존재하지 않는다는 점에 주목하십시오. 변수 $x$에 어떤 값을 선택하든 항상 모순으로 끝납니다 - $x$에 $\text{true}$를 할당하면 함의에 의해 $\lnot x$도 $\text{true}$여야 하며, 그 반대도 마찬가지입니다. 사실 이 조건은 필요조건일 뿐만 아니라 충분조건이기도 합니다. 이는 몇 문단 아래에서 증명하겠습니다. 먼저 한 정점에서 두 번째 정점에 도달할 수 있고 두 번째 정점에서 첫 번째 정점에 도달할 수 있다면, 이 두 정점은 같은 강한 연결 요소에 속한다는 사실을 떠올려 보십시오. 따라서 해가 존재하기 위한 조건을 다음과 같이 정식화할 수 있습니다:
이 2-SAT 문제가 해를 가지기 위한 필요충분조건은 모든 변수 $x$에 대해 정점 $x$와 $\lnot x$가 함의 그래프의 서로 다른 강한 연결 요소에 속하는 것입니다.
이 조건은 모든 강한 연결 요소를 찾아 $O(n + m)$ 시간에 확인할 수 있습니다.
다음 그림은 예시의 모든 강한 연결 요소를 보여 줍니다. 쉽게 확인할 수 있듯이, 네 요소 중 어느 것도 정점 $x$와 그 부정 $\lnot x$를 함께 포함하지 않으므로, 이 예시는 해를 가집니다. 올바른 할당을 계산하는 방법은 다음 문단들에서 배우겠지만, 설명을 위해 우선 해 $a = \text{false}$, $b = \text{false}$, $c = \text{false}$를 제시합니다.
이제 해가 존재한다는 가정하에 2-SAT 문제의 해를 구하는 알고리즘을 구성합니다.
해가 존재하더라도 함의 그래프에서 $x$로부터 $\lnot x$에 도달할 수 있거나, (동시에는 아니지만) $\lnot x$로부터 $x$에 도달할 수 있는 경우가 있다는 점에 주목하십시오. 그러한 경우 $x$에 $\text{true}$와 $\text{false}$ 중 하나를 선택하면 모순이 생기지만, 다른 하나를 선택하면 모순이 생기지 않습니다. 모순이 생기지 않도록 값을 선택하는 방법을 알아봅시다.
강한 연결 요소들을 위상 순서로 정렬하고(즉, $v$에서 $u$로 가는 경로가 있으면 $\text{comp}[v] \le \text{comp}[u]$), $\text{comp}[v]$가 정점 $v$가 속한 강한 연결 요소의 인덱스를 나타낸다고 합시다. 그러면 $\text{comp}[x] < \text{comp}[\lnot x]$이면 $x$에 $\text{false}$를 할당하고, 그렇지 않으면 $\text{true}$를 할당합니다.
이렇게 변수를 할당하면 모순에 이르지 않는다는 것을 증명해 봅시다. $x$에 $\text{true}$가 할당되었다고 가정합니다. 다른 경우도 비슷한 방법으로 증명할 수 있습니다.
먼저 정점 $x$에서 정점 $\lnot x$에 도달할 수 없음을 증명합니다. $\text{true}$를 할당했으므로 $x$의 강한 연결 요소의 인덱스는 $\lnot x$의 요소의 인덱스보다 커야 합니다. 이는 $\lnot x$가 $x$를 포함하는 요소의 왼쪽에 위치한다는 뜻이며, 후자의 정점은 전자에 도달할 수 없습니다.
둘째로, 함의 그래프에서 $x$로부터 정점 $y$와 $\lnot y$ 모두에 도달할 수 있는 변수 $y$가 존재하지 않음을 증명합니다. 그러한 변수가 있다면 $x = \text{true}$가 $y = \text{true}$와 $\lnot y = \text{true}$를 함의하므로 모순이 발생합니다. 이를 귀류법으로 증명해 봅시다. $x$로부터 $y$와 $\lnot y$ 모두에 도달할 수 있다고 가정하면, 함의 그래프의 성질에 의해 $y$와 $\lnot y$ 모두로부터 $\lnot x$에 도달할 수 있습니다. 추이성에 의해 $x$로부터 $\lnot x$에 도달할 수 있다는 결과가 나오며, 이는 가정에 모순됩니다.
이로써 임의의 변수 $x$에 대해 정점 $x$와 $\lnot x$가 서로 다른 강한 연결 요소에 속한다는 가정 하에서 변수들의 요구되는 값을 찾는 알고리즘을 구성했습니다. 위에서 이 알고리즘의 정확성을 보였습니다. 결과적으로 위에서 제시한 해의 존재 조건도 동시에 증명했습니다.
구현:¶
이제 전체 알고리즘을 구현할 수 있습니다. 먼저 함의 그래프를 구성하고 모든 강한 연결 요소를 찾습니다. 이는 Kosaraju 알고리즘으로 $O(n + m)$ 시간에 수행할 수 있습니다. 그래프의 두 번째 순회에서 Kosaraju 알고리즘은 강한 연결 요소들을 위상 순서로 방문하므로, 각 정점 $v$에 대해 $\text{comp}[v]$를 쉽게 계산할 수 있습니다.
그런 다음 $\text{comp}[x]$와 $\text{comp}[\lnot x]$를 비교하여 $x$의 할당을 선택할 수 있습니다. $\text{comp}[x] = \text{comp}[\lnot x]$이면 2-SAT 문제를 만족하는 유효한 할당이 존재하지 않음을 나타내기 위해 $\text{false}$를 반환합니다.
아래는 이미 구성된 함의 그래프 $adj$와 전치 그래프 $adj^{\intercal}$(각 간선의 방향이 뒤집힌 그래프)에 대한 2-SAT 문제의 해법 구현입니다. 그래프에서 인덱스가 $2k$와 $2k+1$인 정점은 변수 $k$에 대응하는 두 정점이며, $2k+1$이 부정된 변수에 대응합니다.
struct TwoSatSolver {
int n_vars;
int n_vertices;
vector<vector<int>> adj, adj_t;
vector<bool> used;
vector<int> order, comp;
vector<bool> assignment;
TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) {
order.reserve(n_vertices);
}
void dfs1(int v) {
used[v] = true;
for (int u : adj[v]) {
if (!used[u])
dfs1(u);
}
order.push_back(v);
}
void dfs2(int v, int cl) {
comp[v] = cl;
for (int u : adj_t[v]) {
if (comp[u] == -1)
dfs2(u, cl);
}
}
bool solve_2SAT() {
order.clear();
used.assign(n_vertices, false);
for (int i = 0; i < n_vertices; ++i) {
if (!used[i])
dfs1(i);
}
comp.assign(n_vertices, -1);
for (int i = 0, j = 0; i < n_vertices; ++i) {
int v = order[n_vertices - i - 1];
if (comp[v] == -1)
dfs2(v, j++);
}
assignment.assign(n_vars, false);
for (int i = 0; i < n_vertices; i += 2) {
if (comp[i] == comp[i + 1])
return false;
assignment[i / 2] = comp[i] > comp[i + 1];
}
return true;
}
void add_disjunction(int a, bool na, int b, bool nb) {
// na and nb signify whether a and b are to be negated
a = 2 * a ^ na;
b = 2 * b ^ nb;
int neg_a = a ^ 1;
int neg_b = b ^ 1;
adj[neg_a].push_back(b);
adj[neg_b].push_back(a);
adj_t[b].push_back(neg_a);
adj_t[a].push_back(neg_b);
}
static void example_usage() {
TwoSatSolver solver(3); // a, b, c
solver.add_disjunction(0, false, 1, true); // a v not b
solver.add_disjunction(0, true, 1, true); // not a v not b
solver.add_disjunction(1, false, 2, false); // b v c
solver.add_disjunction(0, false, 0, false); // a v a
assert(solver.solve_2SAT() == true);
auto expected = vector<bool>(True, False, True);
assert(solver.assignment == expected);
}
};