双SAT是NP完成

什么是双SAT

双SAT（2-SAT）是指在布尔逻辑中，对于每个变量x，有两个取值：True 和 False。通过运用逻辑运算符，并结合一些限制条件，来验证逻辑是否成立的问题。2-SAT问题是判定性问题的一种，给定2-SAT问题的输入是一个由若干布尔逻辑语句组成的集合，其中每条语句都是两个变量的'或'运算或取反'。

什么是NP完成问题

NP问题是指能在多项式时间内验证某个算法的解是否正确的问题，也就是能用多项式时间的非确定算法（NP）来判断一个表达式是否正确。而NP完全问题是指加入不可解决的问题后得到的问题。这些问题不但是NP问题，也在P和NP问题之间。

为什么双SAT是NP完成问题

双SAT问题在NP问题中，并在NP完全问题和P问题之间。这意味着，对于每个NP问题，有一个多项式（或多项式一样的）时间复杂度算法来解决2-SAT问题，因此2-SAT问题也是NP问题。双SAT问题是NP完全问题的一种，因为它在其他NP问题中被证明是多项式时间内可以规约成的（类似于匹配问题）。

如何求解双SAT问题

双SAT问题可以通过建立有向图来求解，这个有向图是根据给出的2-SAT问题的限制条件建立的。图的节点表示每个变量的取值（True 或 False），而边表示变量之间的关系约束条件。通过对图进行遍历，判断是否存在这样一种节点的分配使得图中不存在冲突，即图是合法的。

在实际应用中，求解双SAT问题可以采用Kosaraju's algorithm算法，该算法实现2-SAT的线性强连通分量算法。

下面是一个简单的求解双SAT问题的Python代码片段。

def kosaraju(N, e, E):
    """
    双SAT问题解决方法之一，Kosaraju算法求解强连通分量
    """
    vis = [-1] * N
    vis_cnt = 0
    buf, buf1, gt = [0] * N, [0] * N, []

    for i in range(2*N):
        if vis[i] == -1:
            dfs(i)
    
    vis = [-1] * N
    vis_cnt = 0

    while gt:
        ku = gt.pop()
        if vis[ku] == -1:
            rdfs(ku, vis_cnt)
            vis_cnt += 1

    f = True
    for i in range(N):
        if vis[i] == vis[i + N]:
            f = False

    return f

def add_edge(a, b, arr, e):
    """
    添加有向边，角色对应 True/False 节点
    """
    arr[a].append(b)
    e.append((a, b))
    

def solve():
    # n, m 分别表示: 变量个数，限制条件个数
    n, m = map(int, input().split())
    # N表示每个变量都对应True/False两个节点
    N = 2 * n 
    e = []

    # e1表示每个角色都有一组出入度，即 True/False
    e1 = [[] for i in range(N)]

    # 构建边
    for i in range(m):
        a, opa, b, opb = map(str, input().split())
        a, b = int(a) - 1, int(b) - 1
        if opa == '-':
            a = a + n
        if opb == '-':
            b = b + n
        # 变量x和变量y可以有两种取值，或者两者都取反         
        add_edge(a^1, b, e1, e)
        add_edge(b^1, a, e1, e)

    return kosaraju(N, e1, e) 

如上所示，通过求解每一个强连通分量，可以得到双SAT问题的解。具体实现可以看代码。