clpfd 需要标记才能找到任何解决方案（使用 \+ 时）

Question

我正在尝试写类似“如果你之前得到球，那么你就得到了球，并且从那以后没有给它”：

:- use_module(library(clpfd)).

time(T1, has_ball) :-
    time(T2, get_ball),
    T2 #=< T1,
    \+ (time(T3, give_ball),
         T2 #< T3, T3 #< T1).

time(0, get_ball).
time(2, give_ball).

这正确回答了有关特定时间 T 的直接问题（通过提供 T，例如带有标签）：

?- time(1, has_ball).
true.

?- T in 0..9, label([T]), time(T, has_ball).
T = 0 ;
T = 1 ;
T = 2 ;
false.

但是当被要求查找所有有效时间 T 时，我得到了错误：

?- time(T, has_ball).
false.

据我了解，clpfd 在没有标记的情况下对结果做了一些过度近似，所以我会期待像“T in inf..sup, time(T, has_ball)”这样的东西。告诉我使用标签。但很明显我错了，现在我担心我可能会错过其他情况下的解决方案。谁能帮我理解一下？

编辑： Isabelle Newbie 的回答让我意识到我的意思是：

time(HasBall, has_ball) :-
    time(GetBall, get_ball),
    GetBall #=< HasBall,
    \+ (time(GiveBall, give_ball),
        GetBall #< GiveBall #/\ GiveBall #< HasBall).

因为这个想法是“如果你在之前的某个时间 GetBall 得到球，那么你在时间 HasBall 仍然有球，并且没有给它 SINCE”。所以time(GiveBall, give_ball) 需要否定。这里用#\ 替换\+ 会给出一个新错误（“域错误：预期为`clpfd_reifiable_expression'”），我将对其进行调查。

Answer 1

简短的回答是您不应该将 Prolog 否定 \+ 与 CLP(FD) 混合使用。 CLP(FD) 有自己的否定运算符，可以处理其约束，写为#\。所以你可以把你的谓词写成：

time(HasBall, has_ball) :-
    time(GetBall, get_ball),
    GetBall #=< HasBall,
    time(GiveBall, give_ball),
    #\ (GetBall #< GiveBall #/\ GiveBall #< HasBall).

我重命名了你的变量，因为我真的不明白发生了什么。现在有点清楚了，但是不应该将否定约束只替换为积极的HasBall #=< GiveBall吗？

在任何情况下，它的行为都如我所愿：

?- time(T, has_ball).
T in 0..2.

?- time(T, has_ball), label([T]).
T = 0 ;
T = 1 ;
T = 2.

?- time(1, has_ball).
true.

?- T in 0..9, label([T]), time(T, has_ball).
T = 0 ;
T = 1 ;
T = 2 ;
false.

为了进一步了解发生了什么，我们可以使用您的原始子句并将变量替换为它们的常量值：

step1(T1) :-
    T2 = 0,
    T2 #=< T1,
    \+ ( T3 = 2, T2 #< T3, T3 #< T1 ).

step2(T1) :-
    0 #=< T1,
    \+ ( 0 #< 2, 2 #< T1 ).

step3(T1) :-
    0 #=< T1,
    \+ ( 2 #< T1 ).

所以在最后一步之后，当使用绑定变量和未绑定变量调用谓词时，谓词的行为基本上如下：

?- T1 = 1, 0 #=< T1, \+ (2 #< T1).
T1 = 1.

?-         0 #=< T1, \+ (2 #< T1).
false.

这是因为在第一种情况下，最后一个目标是 \+ (2 #< 1)，它成功是因为 2 #< 1 失败。

但是如果你不绑定T1，那么2 #< T1成功：

?- 2 #< T1.
T1 in 3..sup.

所以它的否定\+ (2 #< T1) 失败了。这个目标本质上是说“没有大于二的数字”，这是错误的。相比之下，CLP(FD) 否定成功并带有“相反”约束：

?- #\ (2 #< T1).
T1 in inf..2.

这几乎肯定在您的程序上下文中更有意义，因为它尊重不 (A = B) 的数学属性：

?- 2 #>= T1.
T1 in inf..2.

编辑：我错过了这样一个事实，即可能没有看到 give_ball 事件，在这种情况下，人们仍然会拿着球。您不能使用#\ 来按照您尝试的方式进行建模，因为#\ 仅 应用于 CLP(FD) 约束（特别是“可重构”约束）但不适用于“正常”Prolog 目标.你也不能这样混合这些级别。

因此，您需要更明确地说明存在的两种情况：如果其中任何一种情况，您都没有放弃球：

• 球在某个时间被放弃了，但那个时间还没有到；或
• 根本没有放弃球。

这在 Prolog 中也是一样的，将应用 Prolog 否定的地方与应用 CLP(FD) 否定的地方分开：

has_not_given_up_ball(HasBall) :-
    time(GiveBall, give_ball),
    \# ( GetBall #< GiveBall #/\ GiveBall #< HasBall ).
has_not_given_up_ball(_HasBall) :-
    \+ time(_GiveBall, give_ball).

（同样，我认为您应该只使用HasBall #=< GiveBall 而不是否定约束。）

然后你可以像这样调整你的定义：

time(HasBall, has_ball) :-
    time(GetBall, get_ball),
    GetBall #=< HasBall,
    has_not_given_up_ball(HasBall).

如果存在time(2, give_ball) 事实，则其行为与以前一样，但有一个额外的选择点。如果我注释掉这一事实，它正确地模拟了球没有被放弃，因此人们持有它的时间更长：

?- time(T, has_ball).
T in 0..sup.

?- time(T, has_ball), label([T]).
ERROR: Arguments are not sufficiently instantiated
...

?- time(1, has_ball).
true.

?- T in 0..9, label([T]), time(T, has_ball).
T = 0 ;
T = 1 ;
T = 2 ;
T = 3 ;
T = 4 ;
T = 5 ;
T = 6 ;
T = 7 ;
T = 8 ;
T = 9.

只有对不受限制于有限域的时间的标记才会出错。