読者です 読者をやめる 読者になる 読者になる

2-SATを探索で解く方法とyukicoder No.470 Inverse S+T Problem

問題解説

2-SATを想定解とする問題をyukicoderで出題しました。
No.470 Inverse S+T Problem - yukicoder

想定解通りの2-SAT解法とは別に、計算量のよく分からない探索を結構通されてしまいました。
探索解の中に正当なものがあるのか、調べていたところ2-SATを暗黙的に解いている提出が見つかりました。
たとえばヘクトさんの提出です。

その解き方というのが、Wikipediaの2-SATの解法の一つとして載っているLimited backtrakingです。
2-satisfiability - Wikipedia
http://epubs.siam.org/doi/abs/10.1137/0205048

例を用いて大雑把に説明します。
 (\lnot x_1 \lor x_2) \land (\lnot x_1 \lor \lnot x_2) \land (\lnot x_1 \lor x_5) \land (x_1 \lor x_3) \land (\lnot x_3 \lor x_4) \land (x_5 \lor x_6)
が充足可能か調べましょう。

真であると分かったリテラルの集合を Tで表します。
まず適当な変数を選び( x_1とします)真だと仮定します。( T = \{ x_1 \})
 \lnot x_1は偽になるので、このリテラルを含む節では、もう片方が真になる必要があります。
1つめの節から T x_2を加えます。
2つめの節から T \lnot x_2を加えます。
ここで T = \{ x_1, x_2, \lnot x_2 \}となり、矛盾が見つかりました。

今度は x_1が偽だと仮定します。( T = \{ \lnot x_1 \})
 x_1を含む節に注目します。
4つめの節から T x_3を加えます。
 x_1を含む節は1つだけです。新たに Tに加わった x_3に対して、 \lnot x_3を含み、真であることが確定していない節に注目します。
5つめの節から T x_4を加えます。
これで( T = \{ \lnot x_1, x_3, x_4\})になりました。これ以上 Tに追加することもできませんし、矛盾もみつかりませんでした。

 Tに含まれているリテラルを含むような節は、残りの変数の値によらず真になります。
そうでない節は、 Tに出てくる変数を含みません。この例では、 (x_5 \lor x_6)が余っています。

残った小さな問題についてこの手続を繰り返していきます。最終的に節が無くなれば残りの変数は適当に決めてよいです。
もし部分的な式が充足不能ならば全体も充足不能ですし、部分的な式が充足可能ならばいままでに確定した真偽の割り当てと合わせて全体が充足可能です。


ある程度無駄を省けば計算量は O(nc)になると思います(nが変数の数,cが節の数)。
このアプローチでも工夫すると線形時間で解けるらしいです。