ふと2-SATの事が気になって、復習がてらPractice RoomでSRM464のDiv1 Medium問題を開いてみた。(ちなみにSRM464には出場している) SAT (充足可能性問題, SATisfiability problem) についてはここの読者の皆さんはご存知とは思います。NP完全問題でおなじみのあれです (x_0 ∨ ¬x_1) ∧ (¬x_0 ∨ ¬x_3) ∧ ... みたいな論理式(乗法標準形)を満たす真偽値 x_0, x_1, ... の組み合わせが存在するか否か。(存在する場合、その組み合わせを知りたかったりする) 上の例ではすべての節が(高々)2変数なので2-SATと呼ばれる。 (2-SATは線形時間で解けるらしい)。 論理和 x ∨ y が論理包含 ¬x⇒y (または ¬y⇒x)に書き換え可能なことを利用して、論理式を有向グラフに変換してみたり 出来上がっ