具体化整合问题

Question

我为最近的问题提供了以下基于 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] 中的每个非奇数项目留下了一个 无用的选择点。

替代实施

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

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 是个好主意吗？

我是否遗漏了这条路上的问题？请帮助！提前致谢！

Answer 1

直接的解决方案（适用于任何可具体化的 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 还是 true/false 用作真值在这里并不重要。在算术求解器中首选 0/1 约定的原因很简单，您可以轻松地在算术约束中重用真值，例如加起来等等

Answer 2

在 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].

Answer 3

我重新考虑了 if_/3 的 "double-use" 提议，我觉得我现在看得更清楚了。

@false 和@lurker 的评论以及@mat 的回答在帮助我理解方面发挥了重要作用。谢谢！

我得到的"insights"绝不是戏剧性的；我仍然想与您分享它们：

像我一样调整 if_/3 是可行的，并且可能与某些 LOC 相同。
但是，它混淆了两个在程序上完全不同的概念：默认情况下，clpfd 传播然后延迟。具体化的术语平等 OTOH 立即强制做出选择。
因此，将这两个用例分开会更清晰。当然，"Cleanliness is indeed next to Godliness"...

具体化整合问题

Reification integration issues

prolog

clpfd

reification

替代实施

底线