AtCoder Library を読んでアルゴリズムを勉強：2-SAT

これまでと同じ前書き

競技プログラミング AtCoder では、コンテストでよく使うアルゴリズムをライブラリにした AtCoder Library (ACL) を公開していて、特に C++ ならコンテスト内で利用できます。

私は Ruby を使っているため直接は利用できず、ライブラリを模写する必要がありました。その過程で学んだアルゴリズムを整理してまとめます。

---

今回は 2-SAT (2-satisfiability) です。前回扱った強連結成分 (SCC) を利用して解いています。

• AtCoder Library の two_sat
  • ソースコード
  • ドキュメント

TL;DR

• 「 x_i に false を割り当てたら x_j には true を割り当てないといけない」といった依存関係をグラフ化して考えます
  • 依存関係の結果が矛盾を起こしたら解は無く、無矛盾なら解は少なくともひとつあります（解を実際にひとつ提示します）
  • このグラフ問題は、強連結成分分解およびトポロジカルソートによって簡単に処理できます

充足可能性問題（SAT）について

簡単に言えば、いくつかの変数を使った論理式全体を真にできるかという問題です。if文の条件式が複雑なときに中身が実行され得る（到達不能コードではない）かどうか知りたい、といった状況を考えると良いと思います。

if x1 && !x3 && (!x1 || x2) && (!x2 || x3)
  # 到達不能コード： x1, x2, x3 の真偽にかかわらず実行されない
  system("rm -rf /")
end

考える論理式は任意の形だと大変なので、連言標準形（CNF）だけ扱うことにしています。これは「変数（それ自身か否定）の論理和の論理積」の形です。論理和の各項は「リテラル」、論理和全体＝論理積の各項は「節」（clause）と呼びます。

(x_1 \lor \bar{x}_2) \land (x_2 \lor x_3 \lor \bar{x}_4)

2-SAT は、全ての節でリテラルが高々2つ¹の問題です。3つ以上の節がある場合は高速なアルゴリズムが知られていないものの（NP完全）、2つなら線形時間のアルゴリズムが知られています。

アルゴリズム

以下のようにして強連結成分の問題へ帰着させます。

グラフ化

2-SAT で扱う論理式が真になる条件は全ての節が真になることです。

ひとつの節 $(x_i \lor x_j)$ が真になる条件は、以下のように言い換えられます。

• もし $x_i$ が偽ならば $x_j$ は真
• もし $x_j$ が偽ならば $x_i$ は真

この依存関係を可視化するために、 x_i = true, x_i = false, x_j = true, x_j = false の4頂点を持つ有向グラフを描いてみます。

この作業を全ての節について行うと、各変数の真・偽を頂点とする大きな有向グラフ（implication graph）が完成します。以下に例を示します。

(x_0 \lor x_1) \land (x_0 \lor \bar{x}_2) \land (x_1 \lor x_2) \land (\bar{x}_1 \lor x_3) \land (\bar{x}_2 \lor x_3) \land (\bar{x}_2 \lor \bar{x}_3)

例えば x1 = true と決めると、矢印をたどることで x2 = false, x3 = true も決まることがわかります。

解の存在判定

解が存在しない十分条件は「ある変数で真と偽のどちらも選べない」ことです。依存関係で読み替えると、以下のように矛盾を起こします。

• もし $x_i$ が偽ならば $x_i$ は真
  → なので $x_i$ は偽ではない
• もし $x_i$ が真ならば $x_i$ は偽
  → なので $x_i$ は真ではない
• → したがって $x_i$ は真でも偽でもダメ

これはグラフで言うと、頂点 x_i = true と x_i = false が互いに繋がっている、つまり同じ強連結成分に属するということになります。以下は実際に x2 の両頂点で循環ができています（他にも循環があります）。

そのため、グラフを強連結成分分解して各変数について調べれば、矛盾を起こしているかどうかがわかります。前節の例であれば、どの変数も真と偽の頂点は異なる成分に属しているため、循環は存在しません。

ところで、グラフで見て矛盾を起こしていないなら解が必ず存在するのか？ということにはまだ触れていません。ここは説明が難しいのですが、次節で解の簡単な見つけ方を説明します。

解の作成

解を見つける素朴な方法は、適当な変数の真偽値を仮決めして、依存している変数にも値を当てていくことです。どこかで変数に真と偽の両方を当ててしまったら（矛盾を起こしたら）、仮決めが間違っていたことになるので戻って選び直します。

例えば x1 = false と決めると、矢印をたどることで x1 = true も選んでしまうので、元の決め方が間違っていたことになります。この探索を繰り返していくのは地味に面倒です。

---

しかし、解をひとつだけ作るのはもっと楽な方法があります。強連結成分についてトポロジカルソートしておき、各変数の真偽値はソート後の番号が大きい方（矢印の終端側）²を愚直に選びます。これは必ず成功し、グラフを探索して矛盾を起こさないか確かめる必要はありません。

なぜこの方法で大丈夫なのか考えたのですが、各変数の真偽値の間に有向辺を描き加えてみたら納得しました。トポロジカルソートが済んでいる状態で、その番号付けを守るように有向辺を加えても結果は変化しません。ソートが保たれるため矛盾は起きず、しかし変数内で辺を加えたため真偽値のどちらを選べばいいか明確です。（一方で番号付けに逆らって有向辺を加えると、強連結成分が合体して真偽値を選べなくなる可能性があります）

実装

強連結成分分解とそのトポロジカルソートが必要なので、 ACL では同ライブラリの scc を利用しています。

初期化

変数が n 個とすると、それぞれに真と偽の頂点を用意するので、グラフの頂点は 2n 個となります。頂点の番号付けは自由ですが、例えば「変数の番号を2倍して、偽のほうには1を足す」（真偽値を区別するビットを用意する）とすると扱いやすいです。

節の追加

節 $(x_i \lor x_j)$ の追加は add_clause() で行います。 2-SAT なので節内のリテラルは2つですが、それぞれ否定にするかどうか（ $\bar{x}_i$ など）も指定する必要があるため4引数です。

節を1つ追加するとき、グラフでは辺を2つ追加します。 ACL の実装ではアルゴリズムの説明と逆向きに辺を追加しています。

    # 節 ((x_i == f) || (x_j == g)) を追加する
    def add_clause(i, f, j, g)
      # 各リテラルが単独でtrueになる選び方（の頂点の番号）
      ii = 2 * i + (f ? 0 : 1)
      jj = 2 * j + (g ? 0 : 1)
      # trueになる選び方と相方がfalseになる選び方の間に辺を張る
      @scc.add_edge(ii, jj ^ 1)
      @scc.add_edge(jj, ii ^ 1)
    end

解の存在判定と作成

できあがったグラフを強連結成分分解し、各頂点にその成分のIDを振っておきます（IDはトポロジカルソートされています）。

あとは各変数を表す2つの頂点を比較していきます。

• 成分のIDが同じ場合、真偽値のどちらも選べないため解はありません
• 成分のIDが異なる場合、 ACL の実装方法では番号の小さい方²を真偽値に選びます
  • 全ての変数で選べれば解ありです

    # 解があればそのひとつを真偽値の配列で返す
    # 解が無ければnilを返す
    def satisfiable?
      _, ids = @scc.scc_ids  # 2n 個の頂点の強連結成分のID

      ids.each_slice(2).map do |id1, id2|
        return nil if id1 == id2
        id1 < id2  # 不等号の向きは、辺の張り方やソートの順序付けに依存
      end
    end

1. 節にリテラルがひとつしか無い場合は、 $(x_i \lor x_i)$ のように繰り返せば2つに揃えられます。 ↩

2. 番号の振り方や依存関係の表し方によっては逆になります。 ↩ ↩²