将无限制SAT (USAT)减少为3-SAT

Question

我知道这个过程，只需将每个子句l1∨⋯∨ln转换为n−2子句的连词。

我试图用Z3显示满足原始公式和最终公式的值，以表明它们可以作为SMT文件满足。

为了澄清，你能给出任何关于这个程序的例子吗？谢谢。

Answer 1

等价检查是通过询问求解者是否有一个可以区分两个公式的赋值来完成的。如果没有这样的赋值，那么您可以得出公式是等价的，或者在SAT上下文中，可以满足。

下面是一个简单的例子：

from z3 import *

a, b, c = Bools('a b c')

fml1 = Or(And(a, b), And(a, c))
fml2 = And(a, Or(b, c))

s = Solver()
s.add(Distinct(fml1, fml2))
print(s.check())

现在，如果fml1是一个任意的SAT公式，而fml2是一个3-SAT转换版本(我不是说上面是SAT和3-SAT转换，而是替换这里算法的结果)，那么我们就会认为SAT求解器无法区分它们，即公式Distinct(fml1, fml2)是不可满足的。事实上，我们得到：

unsat

确定他们是一样的。

如果您只使用SMTLib，那么要使用的模板是：

(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)

(assert (distinct (or (and a b) (and a c))
                  (and a (or b c))))
(check-sat)