可以通过命名表达式实现软约束吗？

Question

我想知道是否可以使用命名表达式来实现软约束，而无需显式使用手动“跟踪”变量。

• 在消息 Soft/Hard constraints in Z3 中，Leonardo 解释了如何使用辅助布尔值以手动方式实现软约束。
• 在以下消息中： z3 behaviour changing on request for unsat core，Leonardo 说命名表达式本质上被视为模型查找目的的含义。

使用上面第一条消息中描述的手动跟踪相当麻烦，因为它需要多次调用求解器（事实上，在最坏的情况下可能需要调用2^n 以获得最大可能的软约束集当我们有n 软约束时感到满意）。 是否有可能将这两个想法结合起来让 Z3 以更简单的方式实现软约束？根据这两条消息的想法，我天真地尝试了以下方法：

(set-option :produce-models true)
(set-option :produce-unsat-cores true)
(assert (! false :named absurd))
(check-sat)

我希望 z3 会告诉我sat，因为在模型中将absurd 变成false 可以满足这个人为的例子；但它却产生了unsat；这是合理的，但没有那么有用..

如果您能提供任何见解，我将不胜感激；或者向我指出一些关于 z3 如何更详细地使用命名表达式的文档。 （我浏览了手册，但没有在任何地方看到它们的详细解释。）

Answer 1

命名表达式是 SMT-LIB 2.0 标准的一部分。 在 Z3 中，它们只是使用辅助布尔常量的方法的“语法糖”。

在 SMT-LIB 2.0 标准中，命名表达式用于“跟踪”命令的断言，例如 (get-unsat-core)（参见 SMT-LIB 2.0 reference manual 的第 5.1.5 节）。在您的示例中，如果我们在(check-sat) 之后执行(get-unsat-core)，我们将得到(absurd)。 Here是在线示例的链接。

关于软/硬约束，您似乎想要 MaxSAT。 Z3 附带了一个示例，该示例使用 2 种不同的算法使用 C API 和辅助布尔常量来实现 MaxSAT。最简单的就是使用下面的基本思想。

• 对于每个软约束C_i，它断言b_i implies C_i，其中b_i 是一个新的布尔变量。

• b_i 为 false 的赋值实质上是忽略了约束 C_i。

• 使用AtMostK 形式的约束来强制最多K b_i 为假。 然后，我们可以使用线性搜索来找到可以满足的最大软约束数。我们还可以使用二分搜索（在这种情况下，只需要调用log N，其中N 是软约束的数量）。许多伪布尔求解器都使用了这种方法的变体。

examples\maxsat 的示例还包含 Fu 和 Malik 建议的更智能算法。该示例还显示了如何对约束 AtMostK 进行编码。