SAT ‒ 将最大变量数设置为 true

如何解决SAT ‒ 将最大变量数设置为 true

我希望解决以下与 SAT 相关的问题，最好使用 Z3 或其他一些免费的求解器：

给定一组布尔变量上的谓词逻辑公式（没有量词或否定），找到变量的最大子集，这样如果 true 精确地分配给这个子集中的所有变量，所有公式都满足。公式都是 variable => CNF-formula 形式。

通常，我想找到经典 SAT 问题的“最佳”解决方案，即估值将 true 分配给尽可能多的变量。

解决方法

通用方法

您可以使用 z3 的优化引擎来解决此问题。这是一个例子。

假设我们有 4 个变量 a,b,c,d，谓词是 a -> b&c 和 c & !d。我们首先创建它们并将约束添加到引擎中：

from z3 import *

a,d = Bools('a b c d')
bools = [a,d]

s = Optimize()
s.add(Implies(a,And(b,c)))
s.add(And(c,Not(d)))

现在我们保留一个计数器，并为每个真实变量加 1：

goal = 0
for v in bools:
    goal = goal + If(v,1,0)

最后，我们告诉 z3 最大化这个目标：

s.maximize(goal)

我们现在可以查询最优模型：

print(s.check())
print(s.model())

打印：

sat
[b = True,a = True,d = False,c = True]

从中我们可以得出结论，对于我们的约束，a 最大满足子集是 {a,c}；您可以轻松看到的也是唯一一个。

使用软约束

另一种方法是为每个布尔值添加软约束，而不是创建 goal 变量，如下所示：

from z3 import *

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

s = Optimize()
s.add(Implies(a,Not(d)))

s.add_soft(a)
s.add_soft(b)
s.add_soft(c)
s.add_soft(d)

print(s.check())
print(s.model())

这将产生完全相同的输出；并且当您只想最大化 true 分配的数量时等效。 （如果您想将某些变量优先于其他变量，则第一种形式更为通用，因为您可以为所有变量分配不同的“整数”而不是 1，以确保它们优于其他变量。）