2 SAT Algorithm
コードについての説明
SAT(充足可能性問題) を CNF 形式で書いたときに各クロージャーに高々 $2$ 個しかリテラルが含まれないような命題論理式($2$ SAT) の充足可能性を判定し、
可能なら実際にその割当を計算するアルゴリズムである.
$3$ SAT については決定性チューリングマシンを用いて多項式時間で解くことが難しいと考えられているが $2$ SAT については驚くことに線形時間で解けることが知られている.
$n$ 個のリテラル $x_i$ が存在するとき $x_i$, $\bar{x}_i$ に対応する $2n$ 頂点のグラフを考える.
各クロージャー $a \lor b$ は $\lnot a \rightarrow b$, $\lnot b \rightarrow a$ と同値であり, グラフに $(\lnot a, b)$, $(\lnot b, a)$ ($(\lnot ψ \rightarrow \lnot φ) \rightarrow (φ \rightarrow ψ)$ の成り立つ世界にする) の $2$ つの有向辺を加える. そしてできあがったグラフで強連結成分分解を行い,
すべてのリテラルについて $x_i$ と $\bar{x}_i$ が異なる強連結成分に属することと論理式を満たす解が存在することとが同値になる.
詳しくは蟻本などに載っている.
(関数)
TwoSAT(リテラルの個数): コンストラクタ
void add_closure : リテラルの個数を $n$ とすると ($x_i \lor \bar{x}_j$) なら add_closure$(i, j + n)$ とする(否定は $+n$)
bool satisfy() : 充足可能性判定を行い, 可能なら $ans$ に結果 $1/0$ (真/偽) が格納される
時間計算量: $\O (n+m)$ ($n$ はリテラルの数, $m$ はクロージャーの数)
コード
class TwoSAT {
private:
const int V;
vector<vector<int> > G, rG;
vector<int> ps, cmp;
void add_edge(int from, int to){
G[from].push_back(to), rG[to].push_back(from);
}
void dfs(int u){
cmp[u] = 0;
for(int v : G[u]){
if(cmp[v] == -1) dfs(v);
}
ps.push_back(u);
}
void rdfs(int u, int k){
cmp[u] = k;
for(int v : rG[u]){
if(cmp[v] == -1) rdfs(v, k);
}
}
int scc(){
for(int i = 0; i < 2 * V; ++i){
if(cmp[i] == -1) dfs(i);
}
fill(cmp.begin(), cmp.end(), -1);
int k = 0;
for(int i = 2 * V - 1; i >= 0; --i){
if(cmp[ps[i]] == -1) rdfs(ps[i], k++);
}
return k;
}
public:
vector<int> ans;
TwoSAT(const int literal_count)
: V(literal_count), G(2 * V), rG(2 * V), cmp(2 * V, -1), ans(V){}
void add_closure(int x, int y){
add_edge((x + V) % (2 * V), y), add_edge((y + V) % (2 * V), x);
}
// 充足可能性判定
// 真のものは 1,偽のものは 0 が ans に格納される(解の構成)
bool satisfy(){
scc();
for(int i = 0; i < V; i++){
if(cmp[i] == cmp[V + i]) return false;
ans[i] = (cmp[i] > cmp[V + i]);
}
return true;
}
};