prolog - 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 ).

因此，在最后一步之后，当使用绑定(bind)变量和未绑定(bind)变量调用谓词时，谓词的行为基本上如下:

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

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

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

但是如果不绑定(bind) T1 ，然后 2 #< T1成功:

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

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

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

这几乎可以肯定在您的程序上下文中更有意义，因为它尊重非 (A < B) 等价于 (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.

只是时间的标签不受限制在有限域中，它应该出错。