3

最近引起我注意的是，一些最新版本的FlatZinc支持半具体化的谓词：

半具体化的谓词本质上表示由布尔变量隐含的约束，而不是等价于一个。

来源：文档

问：

  • 现在所有全局谓词都有一个_reif版本吗？
  • 所有全局谓词也都有_imp版本吗？

看里面的内容share/minizinc/可以看到 insidestd只nosets.mzn使用_imp了谓词，所以我的印象是还不是强制支持_imp谓词的。问：这是正确的吗？

查看文档，我发现了这一点：

因此，求解器库应尽可能提供约束的具体版本。该库包含fzn__reif.mzn用于此目的的文件。

来源：文档

如果我正确解释它，则没有必要支持_reif谓词，因为它们已经在其中重新定义share/minizinc（尽管它可能对性能有益）。问：这是正确的吗？

4

1 回答 1

3

大多数情况下，谓词（调用）、R(...)、 用作实际约束：constraint R(...). 现在处理表达式时的问题R(...)是它是否可以直接提供给求解器，或者它是否具有需要评估的重新定义。

如果谓词用于更复杂的表达式B \/ R(...)，那么我们不能只给求解器调用R(...)，因为我们不想强制执行R(...)。相反，我们想知道所描述的关系是否R(...)成立。这就是我们所说的物化。

因此，必须有一个R_reif(..., r)谓词 force r <-> R(...)。本质上，这给出了 的真值R(...)。同样，当编译器被赋予表达式R_reif(...,r)时，它将查看是否可以直接将其提供给求解器，或者是否有可用的重新定义。如果这两个都不可用，那么编译器将尝试从R(...). 如果这也失败了，那么编译器将停止编译。

如果我们回顾一下我们的示例，B \/ R(...)那么人们可能会注意到使用r <-> R(...)不仅仅是必要的。如果R(...)是假的，那么我们仍然需要B，true如果B是false我们仍然要强制R(...)；然而，我们知道没有什么会强迫R(...)成为false. 我们说R(...)是在积极的背景下。在这种情况下，这意味着拥有r -> R(...)就足够了。这被称为半具体化。

在 MiniZinc 中，可以引入一个R_imp(..., r)谓词来提供一个单独的半具体化谓词。这又可以是直接传递给求解器或重新定义的东西。如果编译器必须具体化一个表达式R(...)并看到它处于肯定的上下文中，那么它将首先尝试查看它是否可以找到R_imp(..., r)，否则回退到R_reif(..., r). 请注意，如果生成了重新定义，则调用的上下文会向内传播，并且在重新定义中仍会发生半具体化。

总结并直接回答您的问题：

  • 所有全局谓词都可以被具体化。的重新定义_reif可以显式定义，也可以通过从它们的重新定义生成。
  • 没有一个全局变量是半实体化的。这不是必需的，因为在生成重新定义的具体化时仍然可以触发半具体化，并且目前没有已知的情况下明确的半具体化定义表现更好。
  • 目前没有需要求解器支持的半具体化谓词。但是请注意，任何_reif可以_imp由求解器实现的谓词（包括 FlatZinc 内置函数）。
  • 不需要支持任何全局_reif谓词；_reif但是， FlatZinc 内置函数中有几个必需的谓词确实需要支持。如果求解器没有重新定义或实现这些谓词，则求解器无法支持生成的 FlatZinc。
于 2020-06-04T01:23:19.717 回答