问如何使z3 (Python) SAT解偏向于一个标准，例如“更愿意”有更多否定的文字。

EN

在z3中有两种处理这类问题的主要方法。要么使用优化器，要么通过对求解器的多次调用手动计算。

使用优化器

正如Axel所指出的，处理此问题的一种方法是使用优化求解器。您的示例代码如下：

from z3 import *

A, B = Bools('A B')

o = Optimize()
o.add(Or(A, B))
o.add_soft(Not(A))
o.add_soft(Not(B))

print(o.check())
print(o.model())

这些指纹：

sat
[A = False, B = True]

您可以在软约束中添加权重，这提供了一种在违反约束时将惩罚相关联的方法。例如，如果您想使A成为可能，但不太关心B，那么您将把更大的处罚与Not(B)联系在一起

from z3 import *

A, B = Bools('A B')

o = Optimize()
o.add(Or(A, B))
o.add_soft(Not(A))
o.add_soft(Not(B), weight = 10)

print(o.check())
print(o.model())

这些指纹：

sat
[A = True, B = False]

考虑这一点的方法如下:您要求z3：

• 满足所有规则约束。(也就是说，你加入add的那些人)
• 满足尽可能多的软约束(即您在add_soft中加入的约束)。如果一个解决方案不可能满足他们所有的要求，那么求解者就可以“违反”他们，试图最小化所有违反的约束的总成本，通过将权重之和计算出来。
• 当不给出权重时，您可以假设它是1。您也可以对这些约束进行分组，尽管我怀疑您是否需要这种通用性。

因此，在第二个例子中，z3违反了Not(A)，因为这样做需要付出1的代价，而违反Not(B)则需要付出10的代价。

请注意，当您使用优化器时，z3使用的引擎与用于常规SMT解决方案的引擎不同:特别是，该引擎不是增量的。也就是说，如果您在上面调用check两次(在引入了一些新的约束之后)，它将从头开始解决整个问题，而不是从第一个问题的结果中学习。此外，优化求解器没有常规求解器(双关意！)优化，因此它通常在直线可满足性方面表现较差。详情请参见https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf。

手动进场

如果不想使用优化器，也可以使用跟踪变量的思想“手动”执行。其思想是识别软约束(即那些可能以某种代价被违反的约束)，并将它们与跟踪器变量关联起来。

以下是基本算法：

• 列出您的软约束。在上面的示例中，它们将是Not(A)和Not(B)。(也就是说，你希望这些都满足于给你负面的文字，但很明显，你希望这些只有在可能的情况下才能得到满足。)叫这些S_i。假设你有他们的N。
• 对于每个这样的约束，创建一个新的跟踪器变量，它将是一个布尔值。叫这些t_i。
• 为每个软约束断言N规则约束，每个表单Implies(t_i, S_i)。
• 使用表单AtMostK的伪布尔约束，强制这些跟踪器变量的K最多为t_i为假。然后使用类似于二进制搜索的模式来找到K的最优值。注意，由于您使用的是常规的求解器，所以可以在增量模式下使用它，即调用push和pop。

有关此技术的详细说明，请参阅https://stackoverflow.com/a/15075840/936310。

摘要

以上两种方法中哪一种是问题相关的。从最终用户的角度来看，使用优化器是最简单的，但是您正在使用可能不需要的重型机器，因此可能会受到性能损失。第二种方法可能更快，风险更复杂(因此容易出错！)编程。和往常一样，做一些基准测试，看看哪一个最适合你的特定问题。

Z3py提供了一个优化的求解器优化。它有一个具有以下描述的方法软的：

添加带有可选权重和可选标识符的软约束。如果不提供权重，则违反软约束的惩罚为1。软约束按标识符分组。默认情况下，没有标识符而添加的软约束是分组的。

一个很小的例子可以找到这里

优化上下文为可满足性检查提供了三个主要扩展：

  o = Optimize()

  x, y = Ints('x y')
  o.maximize(x + 2*y)           # maximizes LIA objective

  u, v = BitVecs('u v', 32)
  o.minimize(u + v)             # minimizes BV objective

  o.add_soft(x > 4, 4)          # soft constraint with 
                                # optional weight