Day 123-Q5 — 2-SAT（含意グラフ + SCC分解）

2026-08-15 赤色 Master / Phase 8+ ★★★★★★★★★ 論理・グラフ理論・SCC・Tarjan

問題

$N$個の真偽変数 $x_1,\dots,x_N$ に対し、$M$個の節（2リテラルのOR）が与えられる。リテラルは非0整数$v$（$1\le|v|\le N$）で表し、$v>0$なら$x_v$が真、$v<0$なら$x_{-v}$が偽を意味する。すべての節を同時に満たす割り当てが存在するか判定し、存在するならYesとその割り当てを、存在しないならNoを出力せよ。

入力形式

N M
a_1 b_1
...
a_M b_M

制約

$1 \le N \le 100000$
$1 \le M \le 200000$
$a_k, b_k$ は非0整数
$1 \le |a_k|, |b_k| \le N$

入出力例

入力例1

3 3
1 2
-1 3
-2 -3

出力例1

Yes
1 0 1

解は一意とは限らず他の正しい割り当ても正解

入力例2

1 2
1 1
-1 -1

出力例2

No

x1が真であることと偽であることを同時に強制し矛盾

概念図: 含意グラフとSCC

節 (a∨b) → 含意辺 ¬a→b, ¬b→a 節 (x1 ∨ x2) ¬x1 → x2 ¬x2 → x1 「x1が偽ならx2は真」etc. SCC分解: x_i真 と x_i偽 が同一SCCなら矛盾 x1真 SCC A x1偽 SCC B 経路あり comp[x1真] < comp[x1偽] → x1 = 真 を選択 反復Tarjan SCC (O(N+M)) はSCCを逆位相順（シンク側から先）に番号付ける

ヒント（段階的開示）

ヒント1: 方向性
節$(a\lor b)$は「aが偽ならbは真でなければならない」「bが偽ならaは真でなければならない」という含意（implication）に言い換えられる。全節についてこの言い換えを行うと、リテラル同士の含意関係を表す有向グラフができる。
ヒント2: アプローチ
各変数$x_i$に「真」「偽」の2ノードを用意し（全体で2Nノード）、節$(a\lor b)$について$\lnot a\to b$と$\lnot b\to a$の2辺を張る。$x_i$真ノードと$x_i$偽ノードが同じ強連結成分（SCC）に含まれたら矛盾で充足不可能。すべての変数でこれが起きなければ充足可能。
ヒント3: 誘導（コード骨格）
SCC分解には反復版のTarjanを使う（再帰深度制限の回避）。TarjanはSCCを逆位相順に番号付けるため「x_i真のSCC番号 < x_i偽のSCC番号」ならx_iを真に割り当てる。 
# clause (a or b): not(a) -> b,  not(b) -> a
adj[neg(node(a))].append(node(b))
adj[neg(node(b))].append(node(a))

模範解答 (Python)

import sys

def solve():
    data = sys.stdin.buffer.read().split()
    idx = 0
    N = int(data[idx]); idx += 1
    M = int(data[idx]); idx += 1

    def node_id(v):
        if v > 0:
            return 2 * (v - 1)
        else:
            return 2 * (-v - 1) + 1

    def neg_node(node):
        return node ^ 1

    n_nodes = 2 * N
    adj = [[] for _ in range(n_nodes)]

    for _ in range(M):
        a = int(data[idx]); idx += 1
        b = int(data[idx]); idx += 1
        na, nb = node_id(a), node_id(b)
        adj[neg_node(na)].append(nb)
        adj[neg_node(nb)].append(na)

    # --- 反復版 Tarjan SCC ---
    index_counter = 0
    dfs_stack = []
    lowlink = [0] * n_nodes
    index = [-1] * n_nodes
    on_stack = [False] * n_nodes
    comp = [-1] * n_nodes
    comp_count = 0

    for start in range(n_nodes):
        if index[start] != -1:
            continue
        work = [(start, 0)]
        while work:
            v, pi = work[-1]
            if pi == 0:
                index[v] = lowlink[v] = index_counter
                index_counter += 1
                dfs_stack.append(v)
                on_stack[v] = True
            advanced = False
            while pi < len(adj[v]):
                w = adj[v][pi]
                pi += 1
                if index[w] == -1:
                    work[-1] = (v, pi)
                    work.append((w, 0))
                    advanced = True
                    break
                elif on_stack[w]:
                    if index[w] < lowlink[v]:
                        lowlink[v] = index[w]
            if advanced:
                continue
            work[-1] = (v, pi)
            work.pop()
            if work:
                pv = work[-1][0]
                if lowlink[v] < lowlink[pv]:
                    lowlink[pv] = lowlink[v]
            if lowlink[v] == index[v]:
                while True:
                    w = dfs_stack.pop()
                    on_stack[w] = False
                    comp[w] = comp_count
                    if w == v:
                        break
                comp_count += 1

    ok = True
    for i in range(N):
        if comp[2 * i] == comp[2 * i + 1]:
            ok = False
            break

    if not ok:
        print("No")
        return

    assign = [1 if comp[2 * i] < comp[2 * i + 1] else 0 for i in range(N)]
    print("Yes")
    print(' '.join(map(str, assign)))

solve()
計算量: 含意グラフ構築O(N+M)、反復Tarjan SCC O(N+M)。全体O(N+M)。入力例1・2の両方を手動でグラフ構築しSCCを追跡してYes/Noの判定が一致することを確認済み。出力された割り当てをすべての節に代入して実際に真になることも検算した。

Step-by-Step 解説

1節から含意への言い換え
「節を満たすこと ⟺ 含意グラフをたどってすべての含意が矛盾なく成り立つこと」に帰着できる。
2なぜSCCが同じだと矛盾か
x_i真とx_i偽が同じSCCにあると「x_iが真だと仮定すると含意により偽が導かれ、逆も真」という循環矛盾を意味する。
3反復Tarjanの実装ポイント
ノード数最大2×10^5のため再帰DFSではPythonのデフォルト再帰制限にすぐ達する。(頂点,次に見る隣接リストの添字)の組をスタックに積みwhileループで擬似再帰を模倣する。
4SCC番号から割り当てを復元するルール
TarjanはSCCをシンク側から先に番号付ける。x_i真のSCC番号がx_i偽より小さいならx_i=真を選ぶことで矛盾なく含意が成立する（節(x1∨x1)単体での検算で確認済み）。
5正しさの検証
入力例1・2を手動でグラフ構築しYes/Noの判定を確認。出力割り当てをすべての節に代入し真になることも検算した。

よくあるミス

ミス原因正しい書き方
節(a∨b)に対しa→b, b→aのように直接辺を張ってしまう含意の対偶（否定を経由）変換を忘れる正しくは¬a→bと¬b→a
SCC番号の大小関係を逆にして割り当てるTarjanが位相順・逆位相順どちらで番号付けるか記憶が曖昧小さな具体例で検算しルールの向きを確認してから実装する
再帰DFSでSCCを実装しRecursionErrorになるNが大きい場合の再帰深度制限を見落とす反復（スタックベース）のTarjanを使う
出力を唯一の正解だと思い込む2-SATは複数の有効な割り当てを持つのが一般的すべての節を満たすかどうかで自己検証する

次のステップ

  • 発展: 2-SATは区間スケジューリングの排他制約やグラフの2彩色判定など様々な「AかBのどちらか一方」制約に応用できる。一般の3-SATはNP完全になり、この線形時間アルゴリズムは使えないことも押さえておく。
  • 次回予告: 次のマスターレベル・ローテーションへ（データ構造・グラフ理論・数論・文字列・幾何のバランスを継続）

自己評価

自分の回答

気づき・メモ