2-SAT は強連結成分分解の典型的な応用例!
問題概要
旗 を数直線上に設置したい。旗 は、座標 または座標 に設置可能である。
ただし、どの 2 つの旗も、その距離が 以上となるようにする必要がある。
本の旗を設置することが可能かどうかを判定し、可能ならば置き方を 1 つ示せ。
制約
考えたこと
各旗は、「座標 に設置する」「座標 に設置しない ( に設置する)」という 2 通りずつの選択肢がある。このようなとき、次のように 0-1 変数を考えるのは典型テクニックだ。
そして、問題文の「距離 以上」という制約条件は次のように解釈できる。
- のとき、「 または 」でなければならない
- のとき、「 または 」でなければならない
- のとき、「 または 」でなければならない
- のとき、「 または 」でなければならない
この条件は 2-SAT で記述できる。1 と True、0 を False と考えることにする。
2-SAT とは
を True または False をとる変数 (リテラルと呼ぶ) とする。 は の否定 (True / False を反転したもの) を表す。
このとき、たとえば、
といった式のように、 (OR) でリテラルを結んだ式 (クロージャと呼ぶ) を、 (AND) で繋げたものを考える。
この式の最終的な値が True となるように、各リテラル の値 (True or False) を決めることができるかどうかを問う問題を SAT と呼ぶ。また、最終的な値が True になるようにすることが可能であるとき、充足できると呼ぶ。たとえば上の式は、
- = False
- = True
- = False
- = False
と各リテラル値を定めることで充足できる!
SAT のうち、特にクロージャが 2 個のリテラルから成るものを 2-SAT と呼ぶ。上の式も 2-SAT になっている。また、今回の旗の問題も 2-SAT で表せることがわかる。
2-SAT をグラフで表す
上の 2-SAT の式は、実は下図のようなグラフで表せる。なお、下図で と書かれた頂点はリテラル を表していて、 と書かれた頂点はリテラル を表している。
たとえば、クロージャ は
- = True のとき、 = True でなければならない
- = False のとき、 = False でなければならない
という制約を表している。これを、グラフ上で次のように表現する。
- 頂点 から頂点 へと辺を張る
- 頂点 から頂点 へと辺を張る
同様に他のクロージャも表現すると、上に示したグラフになる。一般の場合の手続きは、最後の「まとめ」で示します。
2-SAT は強連結成分分解で解ける
上に例示したグラフからは、たとえば次のことが読み取れる。
- 辺 がある:つまり、仮に = True ならば = True である
- 辺 がある:つまり、仮に = True ならば = True である
- 辺 がある:つまり、仮に = True ならば = False である
つまり、もし仮に = True だとすると = False でなければならなくなり、矛盾するのだ。よって、 = False でなければならない。
一般に、次のことが言える:
- 頂点 から頂点 へのパスがあるとき: = False でなければならない
- 頂点 から頂点 へのパスがあるとき: = True でなければならない
ここで強連結成分分解を思い出そう。2-SAT を表すグラフを強連結成分する。上で示したグラフの場合、下図のようになる。
頂点 を含む強連結成分のトポロジカルソート順が末尾にあることから、
- = True
- = False
- = False
でなければならないと分かる。頂点 , の間には順序関係がないため、実は の値は True でも False でもどちらでもいい。実際、 の値を True, False, False にした時点で、
の値は True になっている。
2-SAT を充足できない場合
もし仮にある が存在して、頂点 と頂点 が同じ強連結成分に属してしまった場合、2-SAT の答えを True にすることは不可能であると言える。
なぜならば、もし = True だとしたら、頂点 から頂点 へのパスがあることから、 = False となって矛盾するし、 = False だとしても、頂点 から頂点 へのパスがあることから、 = True となって矛盾するのだ。
逆に、どの に対しても、頂点 と頂点 が異なる強連結成分に属している場合は、充足できる。上で定めたルールで の値を決めればよいのだ。
まとめ
2-SAT の解法をまとめる。
まず、各リテラル に対して、2 つの頂点 , を用意する。そして、各クロージャに対して、次のように辺を張る。
- クロージャ に対しては、辺 と辺 を張る
- クロージャ に対しては、辺 と辺 を張る
- クロージャ に対しては、辺 と辺 を張る
- クロージャ に対しては、辺 と辺 を張る
こうしてできる有向グラフを強連結成分分解する。このとき、次のようになる。
- ある に対して、頂点 , が同じ強連結成分に属するならば、充足できない
- そうでないならば、次のように各リテラルの値を定めることで充足できる
- 頂点 から頂点 へのパスがあるとき: = False
- 頂点 から頂点 へのパスがあるとき: = True
- どちらでもないとき: の値は任意
全体として計算量は となる ( はリテラルの個数、 はクロージャの個数)。
AC コード
2-SAT を解く汎用的なライブラリを作った。旗の問題を 2-SAT に帰着して解いている。
#include <bits/stdc++.h> using namespace std; struct SCC { using Edge = int; using SGraph = vector<vector<Edge>>; // input SGraph G, rG; // result vector<vector<int>> scc; vector<int> cmp; SGraph dag; // constructor SCC(int N = 0) : G(N), rG(N) {} // add edge void addedge(int u, int v) { G[u].push_back(v); rG[v].push_back(u); } // decomp vector<bool> seen; vector<int> vs, rvs; void dfs(int v) { seen[v] = true; for (auto e : G[v]) if (!seen[e]) dfs(e); vs.push_back(v); } void rdfs(int v, int k) { seen[v] = true; cmp[v] = k; for (auto e : rG[v]) if (!seen[e]) rdfs(e, k); rvs.push_back(v); } // reconstruct set<pair<int,int>> newEdges; void reconstruct() { int N = (int)G.size(); int dV = (int)scc.size(); dag.assign(dV, vector<Edge>()); newEdges.clear(); for (int i = 0; i < N; ++i) { int u = cmp[i]; for (auto e : G[i]) { int v = cmp[e]; if (u == v) continue; if (!newEdges.count({u, v})) { dag[u].push_back(v); newEdges.insert({u, v}); } } } } // main solver vector<vector<int>> find_scc(bool to_reconstruct = true) { // first dfs int N = (int)G.size(); seen.assign(N, false); vs.clear(); for (int v = 0; v < N; ++v) if (!seen[v]) dfs(v); // back dfs int k = 0; scc.clear(); cmp.assign(N, -1); seen.assign(N, false); for (int i = N - 1; i >= 0; --i) { if (!seen[vs[i]]) { rvs.clear(); rdfs(vs[i], k++); scc.push_back(rvs); } } // reconstruct DAG if (to_reconstruct) reconstruct(); return scc; } }; // 2-SAT Solver struct TwoSATSolver : SCC { // input int num_variables; // result vector<int> solution; // constructor TwoSATSolver(int N = 0) : SCC(N * 2), num_variables(N), solution(N) {} // リテラルの否定をとる inline int take_not(int x) { if (x < num_variables) return x + num_variables; else return x - num_variables; } // closure の追加 void add_constraint(bool is_x_true, int x, bool is_y_true, int y) { assert(x >= 0 && x < num_variables); assert(y >= 0 && y < num_variables); if (!is_x_true) x = take_not(x); if (!is_y_true) y = take_not(y); addedge(take_not(x), y); addedge(take_not(y), x); } // main solver vector<int> solve() { find_scc(); for (int i = 0; i < num_variables; ++i) { // no solution if (cmp[i] == cmp[take_not(i)]) { return vector<int>(); } solution[i] = (cmp[i] > cmp[take_not(i)]); } return solution; } }; int main() { int N, D; cin >> N >> D; vector<int> X(N), Y(N); for (int i = 0; i < N; ++i) cin >> X[i] >> Y[i]; // 2-SAT Solver TwoSATSolver twosat(N); for (int i = 0; i < N; ++i) { for (int j = i+1; j < N; ++j) { if (abs(X[i] - X[j]) < D) twosat.add_constraint(false, i, false, j); if (abs(X[i] - Y[j]) < D) twosat.add_constraint(false, i, true, j); if (abs(Y[i] - X[j]) < D) twosat.add_constraint(true, i, false, j); if (abs(Y[i] - Y[j]) < D) twosat.add_constraint(true, i, true, j); } } const auto &res = twosat.solve(); if (res.empty()) cout << "No" << endl; else { cout << "Yes" << endl; for (int i = 0; i < N; ++i) { cout << (res[i] ? X[i] : Y[i]) << endl; } } }