Day 091-Q5 — 2-SAT（含意グラフ + Kosaraju SCC・充足可能性判定と解構築）

問題

$N$ 個のブール変数と $M$ 個の節 $(\ell_a\lor\ell_b)$ が与えられる。リテラルは正の $i$ が $x_i$、負の $-i$ が $\lnot x_i$。全節を真にする割り当てが存在するか判定し、存在すれば1つ出力する。

入出力例

2 3
1 2
-1 2
-1 -2

POSSIBLE
0 1

前2節から $x_2$ 真、第3節から $x_1$ 偽。解は $x_1=0, x_2=1$。

1 2
1 1
-1 -1

IMPOSSIBLE

$(x_1)\land(\lnot x_1)$ は矛盾。

概念図

ヒント

neg(node) = node ^ 1
# 節 (a ∨ b):  add_edge(neg(a), b);  add_edge(neg(b), a)
# 解: x_i = 真  ⇔  comp[2i] > comp[2i+1]   (トポロジ後ろ側)

模範解答

import sys

def main():
    data = sys.stdin.buffer.read().split()
    idx = 0
    n = int(data[idx]); m = int(data[idx + 1]); idx += 2
    V = 2 * n
    G = [[] for _ in range(V)]
    GR = [[] for _ in range(V)]

    def lit(a):
        # a>0: x_{a} 真 = 2*(a-1) / a<0: x_{|a|} 偽 = 2*(|a|-1)+1
        var = abs(a) - 1
        return 2 * var if a > 0 else 2 * var + 1

    for _ in range(m):
        a = int(data[idx]); b = int(data[idx + 1]); idx += 2
        la = lit(a); lb = lit(b)
        # ¬la -> lb, ¬lb -> la
        G[la ^ 1].append(lb); GR[lb].append(la ^ 1)
        G[lb ^ 1].append(la); GR[la].append(lb ^ 1)

    # --- Kosaraju 第1パス: 帰りがけ順（反復DFS） ---
    visited = [False] * V
    order = []
    for s in range(V):
        if visited[s]:
            continue
        stack = [(s, 0)]
        visited[s] = True
        while stack:
            node, pi = stack[-1]
            if pi < len(G[node]):
                stack[-1] = (node, pi + 1)
                nxt = G[node][pi]
                if not visited[nxt]:
                    visited[nxt] = True
                    stack.append((nxt, 0))
            else:
                order.append(node)
                stack.pop()

    # --- 第2パス: 逆グラフを finish 逆順に走査し SCC 番号付け ---
    comp = [-1] * V
    c = 0
    for s in reversed(order):
        if comp[s] != -1:
            continue
        stack = [s]
        comp[s] = c
        while stack:
            node = stack.pop()
            for nxt in GR[node]:
                if comp[nxt] == -1:
                    comp[nxt] = c
                    stack.append(nxt)
        c += 1

    # --- 判定と解構築 ---
    res = []
    for v in range(n):
        if comp[2 * v] == comp[2 * v + 1]:
            print("IMPOSSIBLE")
            return
        # トポロジカル順で後ろ（comp が大きい方 = 葉側）を真にする
        res.append('1' if comp[2 * v] > comp[2 * v + 1] else '0')

    print("POSSIBLE")
    print(' '.join(res))

main()

Step-by-Step 解説

Step 1: リテラルを頂点に符号化

変数 $x_i$（0-indexed）で真リテラル $=2i$、偽リテラル $=2i+1$。否定は node ^ 1。

Step 2: 含意グラフを構築

節 $(\ell_a\lor\ell_b)$ を $\lnot\ell_a\to\ell_b$, $\lnot\ell_b\to\ell_a$ に変換し、順・逆グラフ両方に張る。

Step 3: Kosaraju で SCC 分解（反復DFS）

第1パスで帰りがけ順 order、第2パスで逆順に逆グラフを走査し SCC 番号を昇順付与。番号はトポロジ順（0=ソース側、大=シンク側）。

Step 4: 判定と割り当て

真頂点と偽頂点が同一SCCなら IMPOSSIBLE。そうでなければトポロジ順で後ろ（comp が大きい方）を真とする。

よくあるミス

次のステップ

• 発展: Tarjan の SCC（1回DFS）に置換し定数倍改善
• 発展: 「少なくとも1つ真」「高々1つ真」等の制約を符号化
• 次回予告: 新テーマ（Master ローテーション継続）

自己評価