2-SAT（2充足可能性）問題とは？C/C++での判定アルゴリズムを解説

2-SAT問題とは

2-SAT（2充足可能性）問題は、各節がちょうど2つのリテラルからなる論理式に対して、すべての節を真にするような変数の割り当て（充足割り当て）が存在するかどうかを判定する問題です。

対象となる論理式は次の形で表されます。

f = (x₁ ∨ y₁) ∧ (x₂ ∨ y₂) ∧ … ∧ (x_n ∨ y_n)

ここで各 x_i、y_i はブール変数またはその否定です。問題は「f は充足可能か？」という問いに帰着します。

含意への書き換え

鍵となるのは、選言（OR）を含意（→）で書き換えられるという同値関係です。次の3つの式はすべて同値です。

• x_i ∨ y_i
• ¬x_i → y_i
• ¬y_i → x_i

そこで、各節 (x_i ∨ y_i) を上記の2つの含意文に変換します。

含意グラフの構築

次に、2n個の頂点を持つ有向グラフ（含意グラフ）を考えます。各節 (x_i ∨ y_i) に対して、次の2本の有向辺を追加します。

• ¬x_i から y_i への辺
• ¬y_i から x_i への辺

このグラフでは、「あるリテラルが偽なら、もう一方のリテラルは真でなければならない」という制約が辺として表現されています。

充足可能性の判定：SCCを利用

¬x_i と x_i が同じ強連結成分（SCC: Strongly Connected Component）に属する場合、f は充足不能と判定されます。これは「x_i が真であると同時に偽でもある」という矛盾が生じることを意味します。

逆に、すべての変数について x_i と ¬x_i が異なるSCCに属していれば、f は充足可能です。

変数への値の割り当て

f が充足可能な場合、構築したグラフの縮約グラフ（SCCを頂点とするDAG）のトポロジカルソートを用いて、各変数に値を割り当てることができます。

• トポロジカル順序で ¬x_i が x_i より後ろにある場合 → x_i は FALSE とみなす
• それ以外の場合 → x_i は TRUE とみなす

この割り当てにより、すべての節が真になることが保証されます。

擬似コード

以下は、コサラジュ（Kosaraju）法でSCCを求め、2-SATの充足可能性を判定する擬似コードです。

func dfsFirst(vertex v):
    marked[v] = true
    for each vertex u adjacent to v do:
        if not marked[u]:
            dfsFirst(u)
    stack.push(v)

func dfsSecond(vertex v):
    marked[v] = true
    for each vertex u adjacent to v do:
        if not marked[u]:
            dfsSecond(u)
    component[v] = counter

// グラフの構築
for i = 1 to n do:
    addEdge(not x[i], y[i])
    addEdge(not y[i], x[i])

// 1回目のDFS（探索終了順をスタックに記録）
for i = 1 to n do:
    if not marked[x[i]]:
        dfsFirst(x[i])
    if not marked[y[i]]:
        dfsFirst(y[i])
    if not marked[not x[i]]:
        dfsFirst(not x[i])
    if not marked[not y[i]]:
        dfsFirst(not y[i])

set all marked values false
counter = 0
flip directions of edges // 辺 v -> u を u -> v に反転

// 逆グラフで2回目のDFS（SCCを検出）
while stack is not empty do:
    v = stack.pop
    if not marked[v]:
        counter = counter + 1
        dfsSecond(v)

// 充足可能性の判定
for i = 1 to n do:
    if component[x[i]] == component[not x[i]]:
        it is unsatisfiable
        exit
    if component[y[i]] == component[not y[i]]:
        it is unsatisfiable
        exit
it is satisfiable
exit

計算量

このアルゴリズムの計算量は、頂点数 V = 2n、辺数 E（節の数を m とすると E = 2m）として O(V + E)、すなわち変数の個数と節の個数に対して線形時間 O(n + m) となります。2-SATは多項式時間で解けることが知られている一方、節に3つ以上のリテラルを含む一般のSAT（3-SAT以上）はNP完全です。そのため、この線形時間アルゴリズムは競技プログラミングや実務の制約充足問題において非常に有用です。