如何用Python实现可输出解的O(n)复杂度2-SAT高效求解算法

核心思路 #

2-SAT的线性时间解法依赖**强连通分量（SCC）**分析：

• 将每个变量x拆分为两个节点：x为真对应2*x，x为假对应2*x+1（索引规则保持一致即可）
• 对每个子句a ∨ b，添加两条蕴含边：¬a → b和¬b → a（逻辑等价转换）
• 计算所有节点的强连通分量后，若任意变量的两个节点属于同一SCC，则问题无解；否则，选择变量对应节点中拓扑序更靠后的取值作为解

基于Kosaraju算法的完整实现 #

Kosaraju算法通过两次DFS实现线性时间的SCC求解，同时支持导出具体变量取值：

def two_sat(num_vars, clauses):
    # 构造原图与逆图：每个变量对应2个节点（真/假状态）
    size = 2 * num_vars
    graph = [[] for _ in range(size)]
    reverse_graph = [[] for _ in range(size)]
    
    # 将逻辑文字转换为节点索引：输入文字如1表示x1为真，-2表示x2为假
    def lit_to_node(lit):
        var_idx = abs(lit) - 1  # 转为0基变量索引
        is_negative = lit < 0
        return 2 * var_idx + 1 if is_negative else 2 * var_idx
    
    # 为每个子句添加对应的蕴含边
    for a, b in clauses:
        not_a = lit_to_node(-a)
        b_node = lit_to_node(b)
        graph[not_a].append(b_node)
        reverse_graph[b_node].append(not_a)
        
        not_b = lit_to_node(-b)
        a_node = lit_to_node(a)
        graph[not_b].append(a_node)
        reverse_graph[a_node].append(not_b)
    
    # 第一步：DFS原图，记录节点完成顺序（逆序栈）
    visited = [False] * size
    order = []
    
    def dfs(u):
        stack = [(u, False)]
        while stack:
            node, processed = stack.pop()
            if processed:
                order.append(node)
                continue
            if visited[node]:
                continue
            visited[node] = True
            stack.append((node, True))
            for v in graph[node]:
                if not visited[v]:
                    stack.append((v, False))
    
    for i in range(size):
        if not visited[i]:
            dfs(i)
    
    # 第二步：DFS逆图，分配每个节点的SCC编号
    visited = [False] * size
    scc_id = [0] * size
    current_id = 0
    
    def reverse_dfs(u, current_id):
        stack = [u]
        visited[u] = True
        scc_id[u] = current_id
        while stack:
            node = stack.pop()
            for v in reverse_graph[node]:
                if not visited[v]:
                    visited[v] = True
                    scc_id[v] = current_id
                    stack.append(v)
    
    for u in reversed(order):
        if not visited[u]:
            reverse_dfs(u, current_id)
            current_id += 1
    
    # 判断可行性并构造解
    solution = [False] * num_vars
    possible = True
    for var in range(num_vars):
        if scc_id[2*var] == scc_id[2*var+1]:
            possible = False
            break
        # 拓扑序越靠后的SCC编号越小，选择对应状态作为解
        solution[var] = scc_id[2*var] < scc_id[2*var+1]
    
    return possible, solution if possible else None

使用示例 #

# 示例：变量x1、x2、x3，子句为(x1∨¬x2)、(¬x1∨x3)、(x2∨¬x3)
num_vars = 3
clauses = [(1, -2), (-1, 3), (2, -3)]
possible, sol = two_sat(num_vars, clauses)

if possible:
    print("存在解：")
    for i in range(num_vars):
        print(f"x{i+1} = {sol[i]}")
else:
    print("无解")

输出结果：

存在解：
x1 = True
x2 = True
x3 = True

关键说明 #

• 变量索引：输入变量从1开始（符合常规问题表述），内部转为0基处理
• 时间复杂度：O(n + m)，其中n为变量数，m为子句数，属于线性时间复杂度
• 解的正确性：通过SCC拓扑序判断，确保选择的取值不会产生逻辑矛盾

内容的提问来源于stack exchange，提问作者niico