物化整合问题答案

【问题标题】：Reification integration issues物化整合问题
【发布时间】：2015-06-12 02:27:41
【问题描述】：

我为最近的问题Segregating Lists in Prolog 提供了以下基于 clpfd 的代码：

list_evens_odds([],[],[]).
list_evens_odds([X|Xs],[X|Es],Os) :-
   X mod 2 #= 0,
   list_evens_odds(Xs,Es,Os).
list_evens_odds([X|Xs],Es,[X|Os]) :-
   X mod 2 #= 1,
   list_evens_odds(Xs,Es,Os).

简洁纯粹，但是会留下很多不必要的选择点。考虑：

?- list_evens_odds([1,2,3,4,5,6,7],Es,Os).

以上查询在[1,2,3,4,5,6,7] 中为每个非奇数项留下一个无用的选择点。

替代实现

使用Prolog union for A U B U C 中@false 演示的具体化技术可以减少不必要的选择点的数量。实现可以更改为：

list_evens_odds([],[],[]).
list_evens_odds([X|Xs],Es,Os) :-
   if_(#<=>(X mod 2 #= 0), (Es=[X|Es0],Os=   Os0),
                           (Es=   Es0, Os=[X|Os0])),
   list_evens_odds(Xs,Es0,Os0).

要直接与 clpfd-reification 交互，if_/3 的实现可以这样调整：

if_( C_1, Then_0, Else_0) :-
   call(C_1,Truth01),
   indomain(Truth01),
   ( Truth01 == 1 -> Then_0 ; Truth01 == 0, Else_0 ).

当然，(=)/3 也需要适应这种约定。

底线

所以我想知道：使用0 和1 作为真值而不是false 和true 是个好主意吗？

我错过了那条路上的问题吗？请帮忙！提前谢谢！

【问题讨论】：

快速修复..., X mod 2 #= M, if_(M=0, ...。另外，您可以给另一个if_/3 取另一个名字，例如if0_/3

标签： prolog clpfd reification

【解决方案1】：

在 SWI-Prolog 中，你可以使用zcompare/3:

:- use_module(library(clpfd)).

list_evens_odds([], [], []).
list_evens_odds([X|Xs], Es, Os) :-
      Mod #= X mod 2,
      zcompare(Ord, 0, Mod),
      ord_(Ord, X, Es0, Es, Os0, Os),
      list_evens_odds(Xs, Es0, Os0).

ord_(=, X, Es0, [X|Es0], Os, Os).
ord_(<, X, Es, Es, Os0, [X|Os0]).

查询示例：

?- list_evens_odds([1,2,3,4,5,6,7], Es, Os).
Es = [2, 4, 6],
Os = [1, 3, 5, 7].

【讨论】：

这看起来不必要地晦涩难懂。为什么要将 {0,1} 映射到 {
发生这种情况是因为我使用您的代码作为起点，它使用一个具体化的值进行分支。使用zcompare/3，不再需要具体化，因此我将其删除。
我不是这个意思，物化很好。 zcompare 是没有意义的。您可以只使用实体化布尔值作为 ord_/6 的第一个参数。
有几个 CLP(FD) 系统还不支持物化。 zcompare/3 或类似的构造更容易添加到此类系统中，并且仍然为与比较相关的此类分支提供声明性解决方案，因此我使用它来展示您如何提供，而无需处理许多具体化的谓词，类似于 CLP(FD) 中原始问题的 if_/3 构造。
mat: “有几个 CLP(FD) 系统还不支持物化” - 真的吗？ “zcompare/3 或类似的结构更容易添加到此类系统中” - 怎么样？它本质上是一种具体化的比较，并不容易实现。没有必要重新发明轮子。

【解决方案2】：

我已经重新考虑了我提议的if_/3 的“双重用途”，我觉得我现在通过它看得更好。

@false 和 @lurker 的 cmets 以及 @mat 的回答在帮助我理解方面发挥了应有的作用。谢谢！

我获得的“洞察力”绝不是戏剧性的；我还是想和你分享：

像我一样适应 if_/3 是可行的，并且可能与某些 LOC 相同。
但是，它混淆了两个在程序上完全不同的概念：默认情况下，clpfd 传播然后延迟。物化术语平等 OTOH 立即强制选择。
因此，将这两个用例分开会更清晰。当然，“清洁确实仅次于敬虔”……

【讨论】：

【解决方案3】：

直接的解决方案（适用于任何可具体化的 clp(fd) 条件）似乎是

:- use_module(library(clpfd)).

list_evens_odds([],[],[]).
list_evens_odds([X|Xs],Es,Os) :-
   B #<==> (X mod 2 #= 0),
   freeze(B, (B=1 -> Es=[X|Es0],Os=Os0 ; Es=Es0,Os=[X|Os0])),
   list_evens_odds(Xs,Es0,Os0).

0/1 或真/假是否被用作真值在这里并不重要。在算术求解器中首选 0/1 约定的原因很简单，您可以轻松地在算术约束中重用真值，例如把它们加起来，等等。

【讨论】：