具体化和半具体化谓词

Question

最近有人提请我注意，最近的一些版本的FlatZinc支持半具体化谓词。

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

Q:

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

查看share/minizinc/的内容，我可以看到在std中只有nosets.mzn使用_imp谓词，所以我的印象是，支持_imp谓词还不是强制性的。Q:是对的吗？

看了看医生，我发现了这个：

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

如果我正确地解释了它，那么就没有必要支持_reif谓词，因为它们已经在share/minizinc中重新定义了(尽管它可能对性能有好处)。Q:是对的吗？

Answer 1

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

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

出于这个原因，必须有一个强制使用R_reif(..., r)的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谓词都可以由求解器(包括FlatZinc构建器)实现为_imp。
• 它不需要支持任何全局_reif谓词；但是，在FlatZinc构建中有几个必需的_reif谓词需要支持。如果求解器没有重新定义或实现这些谓词，则求解程序无法支持生成的FlatZinc。