2-SATを解いた時のメモ - TopCoderとJ言語と時々F#2-SATとは SATとはsatisfiability(充足性)の略で、与えられた論理式を満たす真偽値の組合せが存在することをいう。 特に2-SATとは、変数がx_1からx_nまであるとして以下の形の論理式について変数の真偽値の組合せを考える問題である。 ここで 論理積でつながれたひとつひとつの部分(節)に変数が二つある(節の長さが2である)ので2-SATという。 2-SATの解法について 2-SATに対しては、節の数と変数の数に対する線形時間のアルゴリズムが存在する。ちなみに節の長さが3以上の場合この問題はNP完全に属する。 2-SATを解くにはImplication graphというグラフを構築する必要がある。次節でこのグラフについて述べる。 Implication graphの構築 Implication Implicationとは「包含」という意味であり、論理で言えば論理包含がこれ
