2-SAT

What · 是什么

2-SAT(Satisfiability)问题是判定n个布尔变量能否满足m个'两个变量的析取式'约束的问题，如(x1∨x3)、(¬x2∨x3)等。k-SAT在k>2时是NP完全问题，而2-SAT有多项式算法。解法核心是建蕴含图：每个变量x拆成真、假两个节点，每个约束(a∨b)等价于蕴含对(¬a→b)和(¬b→a)，然后求强连通分量(SCC)：若某变量的真节点与假节点在同一SCC则无解；否则有解，且取'所在SCC编号更小(反拓扑序更靠后)'的节点为真即为一组解。由于每条蕴含边同时建一条逆否边，蕴含图满足对称性，保证该取法正确。复杂度O(V+E)。

Why · 为什么

How · 实现

伪代码

# 建图: 变量i(0-based)节点 i 表示x_i为真, i+n 表示x_i为假
# 约束 (a OR b): a,b为带符号文字, 正=var节点, 负=var+n节点
def add_clause(a, b):
  add_edge(neg(a), b)   # ¬a -> b
  add_edge(neg(b), a)   # ¬b -> a
# 判解: Tarjan SCC
# 无解 iff scc[id(x)] == scc[id(not x)]
# 赋值: val[x] = scc[id(x)] > scc[id(not x)]  (取SCC编号小者/反拓扑序靠后)
#   等价于 若 id(x)的scc编号 < id(not x)的scc编号 则 x=true

Python 实现

import sys

sys.setrecursionlimit(1 << 25)


def solve_two_sat(n, clauses):
    """求解2-SAT.
    n: 变量个数(0..n-1)
    clauses: list[(a, b)], a/b为文字: 正数表示变量i, 负数表示¬i (i为1..n)
    return: (bool, list[int]|None) 是否可行 + 每组变量赋值(True/False)
    """
    # 节点: var i(1..n) -> 真节点 2*i, 假节点 2*i+1
    def node(x):  # 文字x(带符号)到节点编号
        v = abs(x)
        return 2 * v + (0 if x > 0 else 1)

    def neg(x):  # 文字取反
        return -x

    N = 2 * n + 2
    g = [[] for _ in range(N)]
    rg = [[] for _ in range(N)]

    def add_edge(u, v):
        g[u].append(v)
        rg[v].append(u)

    for a, b in clauses:
        add_edge(node(neg(a)), node(b))   # ¬a -> b
        add_edge(node(neg(b)), node(a))   # ¬b -> a

    # Kosaraju SCC
    visited = [False] * N
    order = []

    def dfs(u):
        visited[u] = True
        for v in g[u]:
            if not visited[v]:
                dfs(v)
        order.append(u)

    for i in range(N):
        if not visited[i]:
            dfs(i)

    comp = [-1] * N

    def rdfs(u, cid):
        comp[u] = cid
        for v in rg[u]:
            if comp[v] == -1:
                rdfs(v, cid)

    cid = 0
    for u in reversed(order):
        if comp[u] == -1:
            rdfs(u, cid)
            cid += 1

    for i in range(1, n + 1):
        if comp[2 * i] == comp[2 * i + 1]:
            return False, None  # x与其否定同SCC, 无解

    # 赋值: 取SCC编号更大者为真 (Kosaraju cid与Tarjan同语义: 大cid=反拓扑序靠前)
    # 更通用的做法: 取拓扑序在后者为真, 此处用 comp 编号比较
    val = [False] * (n + 1)
    for i in range(1, n + 1):
        val[i] = comp[2 * i] > comp[2 * i + 1]
    return True, val[1:]


if __name__ == "__main__":
    # 测试1: (x1∨x2), (¬x1∨x3), (¬x2∨¬x3): 有解
    clauses1 = [(1, 2), (-1, 3), (-2, -3)]
    ok, val = solve_two_sat(3, clauses1)
    assert ok, "should be satisfiable"
    # 验证约束
    def check(val, clauses):
        for a, b in clauses:
            fa = val[abs(a) - 1] if a > 0 else not val[abs(a) - 1]
            fb = val[abs(b) - 1] if b > 0 else not val[abs(b) - 1]
            if not (fa or fb):
                return False
        return True

    assert check(val, clauses1), f"assignment {val} violates"

    # 测试2: (x1∨x1) 且 (¬x1∨¬x1): 无解
    clauses2 = [(1, 1), (-1, -1)]
    ok2, val2 = solve_two_sat(1, clauses2)
    assert not ok2, "should be unsatisfiable"

    # 测试3: (x1∨x2), (¬x1∨¬x2): 有解(x1=true,x2=false 或反之)
    clauses3 = [(1, 2), (-1, -2)]
    ok3, val3 = solve_two_sat(2, clauses3)
    assert ok3 and check(val3, clauses3), (val3, clauses3)

    print("two-sat: ALL TESTS PASSED")

易错点

• 每条约束必须建两条对称蕴含边，只建一条会导致对称性破坏、贪心赋解出错
• 变量节点与否定节点下标映射错误(如1-based/0-based混用)是最常见bug
• 判定无解条件：x与¬x在同一SCC，注意是'所在SCC编号相同'而非'有边可达'
• 取解用SCC编号比较方向需与所用SCC算法的编号语义匹配(Kosaraju与Tarjan相反)
• 自环约束如(a∨a)退化为强制a=true, (¬a∨¬a)退化为强制a=false，建图时同样处理

例题

信源

• OI Wiki✓ https://oi-wiki.org/graph/2-sat/
• CP-Algorithms✓ https://cp-algorithms.com/graph/2SAT.html
• 书籍✓ CPH ch20 pp191-204