如何使Z3&#39；(Python)的SAT解算偏向某个标准，例如更倾向于有更多否定的文字 [英] How to bias Z3's (Python) SAT solving towards a criteria, such as 'preferring' to have more negated literals

问题描述

在Z3(Python)中，有没有办法将SAT搜索"偏向""条件"？

一个案例：我希望Z3获得一个模型，但不是任何模型：如果可能，请给我一个有大量否定文字的模型。

例如，如果我们必须搜索A or B，可能的模型是[A = True, B = True]，但我宁愿收到模型[A = True, B = False]或模型[A = False, B = True]，因为它们有更多的False分配。

当然，我猜‘标准’必须具体得多(如果可能的话，：我更喜欢文字的一半而不是假的模型)，但我认为这个想法是可以理解的。

我不在乎该方法是否是本机的。有帮助吗？

推荐答案

在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为FALSE。然后使用类似二分搜索的模式来找到K的最佳值。请注意，由于您使用的是常规求解器，因此可以在增量模式下使用它，即通过调用push和pop。

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

摘要

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

这篇关于如何使Z3&#39；(Python)的SAT解算偏向某个标准，例如更倾向于有更多否定的文字的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！