z3 中有两种主要方法来处理此类问题。使用优化器，或者通过多次调用求解器来手动计算。
使用优化器
正如阿克塞尔指出的，处理这个问题的一种方法是使用优化求解器。您的示例将编码如下：
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 求解的引擎不同：特别是，该引擎是not增加的。也就是说，如果你打电话check两次（在引入一些新的约束之后），它将从头开始解决整个问题，而不是从第一次的结果中学习。此外，优化求解器并不像优化作为常规求解器（双关语！），因此它通常在直接可满足性方面表现也较差。看https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf了解详情。
手动接近
如果您不想使用优化器，您也可以使用跟踪变量的想法“手动”执行此操作。这个想法是识别软约束（即那些可能以一定成本违反的约束），并将它们与跟踪器变量相关联。
这是基本算法：
-
列出你的软约束。在上面的例子中，他们将是Not(A) and Not(B)。 （也就是说，您希望这些满足给您负数文字，但显然您希望只有在可能的情况下才满足这些。）调用这些S_i。假设你有N其中。
-
对于每个这样的约束，创建一个新的跟踪器变量，该变量将是一个布尔值。打电话给这些t_i.
-
Assert N常规约束，每种形式Implies(t_i, S_i)，对于每个软约束。
-
使用伪布尔约束，其形式为AtMostK，最多强制K这些跟踪器变量t_i是假的。然后使用类似于二分搜索的模式来找到最佳值K。请注意，由于您使用的是常规求解器，因此您可以在增量模式下使用它，即调用push and pop.
有关此技术的详细说明，请参阅https://stackoverflow.com/a/15075840/936310.
Summary
上述两种方法中哪一种有效取决于问题。从最终用户的角度来看，使用优化器是最简单的，但您会引入可能不需要的重型机械，因此可能会遭受性能损失。第二种方法可能更快，但存在编程更复杂（因此容易出错！）的风险。像往常一样，进行一些基准测试，看看哪种方法最适合您的特定问题。
