线性 SAT 求解器

bcdmwSjy · 2026-10-05 10:38:01 · 休闲·娱乐

这个算法过于超前，以至于只有放在休闲娱乐里才会有人能看懂。

众所周知，SAT（布尔可满足性问题）是一个著名的 NP 完全问题。而在今天，我发明了一个可以在线性时间复杂度内求出任意 SAT 问题的解的算法，我们来详细讲解一下。

为了完成这个惊人的目标，我们采用万能的正则表达式来处理。

首先，整个算法的核心是这样的一条语句：

(?(group)yes|no)

这是条件匹配的语法，它表示如果 group 曾经成功参与匹配，那就匹配 yes，否则匹配 no。

然后，我们可以把一个布尔变量表示成一个捕获组是否存在。比如 x_1 就可以写成 (?:(?P<x1>)|)，其中 (?P<x1>) 为一个匹配空字符的命名的捕获组。它自然就有两种选择，(?P<x1>) 就代表 x1=True，另一半空串就代表 x1=False。

接下来考虑怎么检查一个子句是否合法，以 x_1 为例，就可以用 (?(x1)|(?!))，其中 (?!) 的匹配一定会失败。这样，整个表达式就表示为如果 x1=True，那么就匹配空串，然后成功；否则就匹配 (?!)，然后失败。

若检查 \neg x_1，即可用 (?(x1)(?!)|)，道理与上面的相同。

只检查一个变量当然没有用，我们考虑怎么实现或运算。

比如检查 x_1\lor\neg x_2，这就相当于先检查 x_1 是否为真，如果为真就成功，否则继续检查 \neg x_2 是否为真，如果为真就成功，否则失败。正好，正则表达式也可以嵌套，于是可以直接写成 (?(x1)| (?(x2)(?!)|) )。

接下来把所有写好的子句直接拼起来就是与操作，跑一次正则表达式匹配即可。

参考实现：

import re

def var(i):
    return r"(?:(?P<x%d>)|)"%i

def compile_clause(c,pos):
    if pos==len(c):
        return r"(?!)"

    x=c[pos]
    v=abs(x)
    r=compile_clause(c,pos+1)

    if x>0:
        return r"(?(x%d)|%s)"%(v,r)
    else:
        return r"(?(x%d)%s|)"%(v,r)

def compile_sat(cnf):
    n=max(max(abs(y) for y in x) for x in cnf)
    v="".join(var(i) for i in range(1,n+1))
    c="".join(compile_clause(x,0) for x in cnf)
    return v+c

def solve_sat(cnf):
    pattern=compile_sat(cnf)
    res=re.fullmatch(pattern,"")

    if res is None:
        return None

    n=max(max(abs(y) for y in x) for x in cnf)
    return tuple(res.group("x%d"%i) is not None for i in range(1,n+1))

if __name__=="__main__":
    cnf=[]
    n=int(input("输入子句个数："))
    print("输入子句内容（i 表示 x_i 为真，-i 表示 x_i 为假，下标从 1 开始，用空格分隔）：")
    for i in range(n):
        cnf.append(list(map(int,input().split())))

    res=solve_sat(cnf)

    if res is None:
        print("UNSAT")
    else:
        print("SAT")
        for i in range(len(res)):
            print("x%d=%s"%(i+1,res[i]))

可以发现，整个代码只遍历了一次所有子句内容，可以认为整体复杂度为线性。

这个算法甚至可以求出一个合法的解，若 x_1 为真，则说明其参与了匹配，内容为空串，否则匹配的内容就为空。这样，解也就求出来了。

总结：

我们定义了一个编译器 R:\text{CNF}\to\text{Regex} 使得 F\in\text{SAT}\iff R(F)\text{ matches }\epsilon，其中 \epsilon 为空串。

假设 re.fullmatch 为基础操作，那么 SAT 就可以用 O(1) 次正则表达式匹配来解决。

实验数据：