(P||Q||...)&(R||S||...)みたいな連言標準形で書かれた論理式を真にする割り当てはあるかを判定する問題をSATといいます。
2-SATの場合カッコ内のリテラル数が高々2つ、つまり(P||Q)&(R||S)みたいになってます。
2-SATの解き方は蟻本の通り、SCCを使って真のnodeと偽のnodeが同じcycle内に属さないことを確認すればよいです。割り当てはトポロジカル順序を確認すればいいです。
直感的に「ならば」の矢印の記号に沿って有向辺を張っていけばよいことがわかりますが、どうやって証明すればいいのでしょう。
僕は最初SCCした後のグラフを二部グラフっぽい形に変形して二部グラフの片側を真、反対側を偽にすればうまくいくことを証明しようとして失敗しました。なので1978年に出たTarjanの論文を読むことにしました。以下リンク。
https://www.math.ucsd.edu/~sbuss/CourseWeb/Math268_2007WS/2SAT.pdf
これを見ると次の真偽割り当てアルゴリズムを使って証明していることがわかります。
SCC後のグラフのトポロジカルソートを逆順から見て、
Sがマークされていたらなにもしない
Sがマークされていないとき、
S==!S(!SはSの真偽をswapさせた点の集合)ならreturn false
それ以外S=true,S=falseとする
このアルゴリズムでP(T)->Q(F)(P(T)はPの割り当てをTrueにしたということ)のような辺が生じると仮定すると、
!QはQよりもトポロジカル順で後ろで
!PはPよりもトポロジカル順で前になります。
P->Qに辺が張ってあるならば、!Q→!Pにも辺が存在し、!Q->!P->..->P->Q->...!Qのループが生じていることがわかります。
これはSCCした後のグラフがDAGであることに矛盾するので、この割り当てアルゴリズムは正しいと証明されました。
さらにこの証明で真偽の割り当てはSと!Sのトポロジカル順を比べて、Sの方が遅ければ真、!Sが遅ければ偽とすればいいことがわかりました。
蟻本のコードはこれをもとにしているわけですね。
論文にはさらにリテラルについて∃または∀の記号がついている際の真偽値の割り当ての方法に言及していますが、そこまではしなくてよさそう。
同じような問題として、(P&Q...)||(S&T...)||みたいな選言標準形をした論理式たちをさらに&でつないでいるものがあります。
いわれてもわけがわからないと思うので例をあげると、蟻本p85の食物連鎖(POJ1182)です。
Union-Findで同時に起こりうるものを管理していますが、これがうまくいく証明は簡単です。
→はSAT、&はUnionFindという認識くらい持っていると思いつけるようになりそうですね。
