0

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

使用上面第一条消息中描述的手动跟踪是相当麻烦的，因为它需要多次调用求解器（事实上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 如何更详细地使用命名表达式的文档。（我浏览了手册，但没有在任何地方看到它们的详细解释。）

4

1 回答 1

1

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

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

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

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

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

  • 使用表单的约束AtMostK来强制执行最多K b_i是错误的。然后，我们可以使用线性搜索来找到可以满足的最大软约束数。我们也可以使用二分搜索（在这种情况下，只log N需要调用N软约束的数量）。这种方法的变体用于许多伪布尔求解器。

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

于 2013-02-25T20:25:49.037 回答