如何在 Z3-Python 中使用软约束来表达 SAT 搜索中的"抽象"偏差：例如"我更喜欢一半的文字为真，一半为假"

Question

我之前在《如何偏置Z3'；s(Python(SAT朝着一个标准求解，例如'；偏好'；为了有更多否定的文字，Z3(Python(中是否有方法将SAT搜索"偏向"于"标准"？

在那篇文章中，我们学到了"简单的偏见"，比如我希望Z3获得一个模型，但不是任何模型：如果可能的话，给我一个有大量否定文字的模型

这是使用新的求解器(Optimize而非Solver(和软约束(add_soft而不是add(执行的。具体地，对于每个文字lit_n和优化的求解器o_solver，添加了：o_solver.add_soft(Not(lit_n))；或者等效地：o_solver.add_soft(Or(Not(lit1), Not(lit2), ...)。

然而，我想表达一个"稍微复杂一点的偏见"。具体来说：如果可能的话：我更喜欢文字一半的模型，而不是True，一半是False。

有什么方法可以用Optimize工具表达这种和类似的"偏见"吗？

Answer 1

这里有一个简单的想法可能会有所帮助。计算正文字的数量，并从负文字的数量中减去。取差值的绝对值，并使用优化器将其最小化。

这应该会找到一个具有尽可能多的正和负文字的解决方案，满足"大约一半"的软约束。

这里有一个简单的例子。假设你有六个文字，你想满足它们的析取。惯用的解决方案是：

from z3 import *
a, b, c, d, e, f = Bools("a b c d e f")
s = Solver()
s.add(Or(a, b, c, d, e, f))
print(s.check())
print(s.model())

如果你运行这个，你会得到：

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

因此，z3简单地使a成为True，而所有其他的都成为False。但你希望有大致相同的积极和消极的文字计数。所以，让我们对其进行编码：

from z3 import *
a, b, c, d, e, f = Bools("a b c d e f")
s = Optimize()
s.add(Or(a, b, c, d, e, f))
def count(ref, xs):
s = 0
for x in xs:
s += If(x == ref, 1, 0)
return s
def sabs(x):
return If(x > 0, x, -x)
lits = [a, b, c, d, e, f]
posCount = count(True,  lits)
negCount = count(False, lits)
s.minimize(sabs(posCount - negCount))

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

注意我们如何"；象征性地"；计算负数和正数，并要求z3将差值的绝对值最小化。如果你运行这个，你会得到：

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

有3个正面和3个负面文字。如果你有7个字开始，它会发现一个4-3的分裂。如果你更喜欢正面文字而不是负面文字，你可以额外添加一个形式的软约束：

s.add_soft(posCount >= negCount)

以这种方式偏移解算器。希望这能让你开始。。