Day 074-Q4 — 2-SAT（含意グラフ・Kosaraju SCC・論理制約解構築）

問題

$N$ 個のブール変数 $x_1, x_2, \ldots, x_N$（各々 True/False）と $M$ 個のクローズ（節）が与えられる。各クローズは $(\ell_i \lor \ell_j)$ の形（リテラル $\ell$ は $x_k$ または $\neg x_k$）。

全クローズを満たす変数の割り当てが存在するかを判定し、存在する場合は 1 つ構築して出力せよ。さらに $x_1 = \text{True}$ が強制された場合の解も存在するか判定せよ。

入出力例

3 4
1 -2
-1 3
2 -3
-2 -3

SAT
x1=T x2=F x3=T

2 2
1 2
-1 -2

UNSAT

概念図: 含意グラフと SCC

ヒント

def lit(x):
    return x - 1 if x > 0 else N + (-x - 1)

def neg_lit(x):
    return x + N if x < N else x - N

for u, v in clauses:
    a, b = lit(u), lit(v)
    na, nb = neg_lit(a), neg_lit(b)
    graph[na].append(b)   # ¬a => b
    graph[nb].append(a)   # ¬b => a

模範解答

import sys
input = sys.stdin.readline

def solve():
    N, M = map(int, input().split())
    clauses = [tuple(map(int, input().split())) for _ in range(M)]

    size = 2 * N
    graph = [[] for _ in range(size)]
    rgraph = [[] for _ in range(size)]

    def lit(x):
        return x - 1 if x > 0 else N + (-x - 1)

    def neg_lit(x):
        return x + N if x < N else x - N

    for u, v in clauses:
        a, b = lit(u), lit(v)
        na, nb = neg_lit(a), neg_lit(b)
        graph[na].append(b)
        graph[nb].append(a)
        rgraph[b].append(na)
        rgraph[a].append(nb)

    # Kosaraju Step 1: 後順 DFS
    visited = [False] * size
    order = []

    def dfs1(start):
        stack = [(start, 0)]
        while stack:
            node, state = stack.pop()
            if state == 0:
                if visited[node]:
                    continue
                visited[node] = True
                stack.append((node, 1))
                for nxt in graph[node]:
                    if not visited[nxt]:
                        stack.append((nxt, 0))
            else:
                order.append(node)

    for i in range(size):
        if not visited[i]:
            dfs1(i)

    # Kosaraju Step 2: 逆グラフで SCC
    comp = [-1] * size
    c = 0

    def dfs2(start, label):
        stack = [start]
        while stack:
            node = stack.pop()
            if comp[node] != -1:
                continue
            comp[node] = label
            for nxt in rgraph[node]:
                if comp[nxt] == -1:
                    stack.append(nxt)

    for v in reversed(order):
        if comp[v] == -1:
            dfs2(v, c)
            c += 1

    # SAT 判定と解構築
    assignment = []
    for k in range(N):
        if comp[k] == comp[k + N]:
            print("UNSAT")
            return
        assignment.append(comp[k] > comp[k + N])

    print("SAT")
    print(" ".join(f"x{k+1}={'T' if v else 'F'}" for k, v in enumerate(assignment)))

    # x1=True 固定での判定
    if assignment[0]:
        print("x1=True を強制: SAT（既に True）")
    else:
        print("x1=True を強制: 既存の割り当てと矛盾（再計算要）")

solve()

Step-by-Step 解説

Step 1: 含意グラフの構築

クローズ $(a \lor b)$ は「$a$ が False なら $b$ は True でなければならない」= $\lnot a \Rightarrow b$ を意味する。対称に $\lnot b \Rightarrow a$ も成り立つ。この 2 辺をグラフに追加する。

変数 $x_k$ には 2 つのノード: k-1（True を表す）と k-1+N（¬x_k を表す）。

Step 2: Kosaraju SCC

2 段階 DFS：1) 元グラフで後順 (post-order) に頂点を積む、2) 逆グラフで積んだ逆順に DFS → 同一 SCC にコンポーネント番号を割り当て。

Step 3: 解の判定と構築

$x_k$ と $\lnot x_k$ が同じ SCC → UNSAT（矛盾）。そうでなければ、逆トポロジカル順（Kosaraju では comp 番号が大きいほど後）で後に来る方が True に割り当てられる。

Step 4: 計算量

• グラフ構築: $O(M)$
• Kosaraju SCC: $O(N + M)$（2回 iterative DFS）
• 全体: $O(N + M)$

よくあるミス

次のステップ

• 発展問題: 変数に「どちらを選んでも同じ結果」な変数（必須 True/False）の列挙
• 類題: AtCoder 「回路設計」「スケジュール制約」系の 2-SAT 応用問題
• さらに: Tarjan SCC を使った同様の実装（1回の DFS で完結）

自己評価