首页 文章

SWI Prolog与GNU Prolog - SWI下的CLP(FD)问题

提问于
浏览
4

我在Prolog中写了一个快速谓词,尝试了CLP(FD)及其解决方程组的能力 .

problem(A, B) :-
    A-B #= 320,
    A #= 21*B.

当我在SWI中调用它时,我得到:

?- problem(A,B).
320+B#=A,
21*B#=A.

在GNU中,我得到了正确答案:

| ?- problem(A,B).

A = 336
B = 16

这里发生了什么?理想情况下,我希望在SWI中获得正确的结果,因为它是一个更加强大的环境 .

1 回答

  • 4

    这是一个很好的观察 .

    乍一看,毫无疑问,它似乎是SWI的一个缺点,它无法像GNU Prolog一样强大地传播 .

    但是,这里还有其他因素在起作用 .

    核心问题

    首先,请在GNU Prolog中尝试以下查询:

    | ?- X #= X.
    

    声明性地,查询可以读作: X 是一个整数 . 原因是:

    • (#=)/2 仅适用于整数

    • X #= X 不以任何方式约束整数 X 的域 .

    但是,至少在我的机器上,GNU Prolog回答:

    X = _#0(0..268435455)
    

    所以,事实上,整数 X 的域已经变得有限,即使我们没有以任何方式限制它!

    为了比较,我们在SICStus Prolog中得到了例子:

    ?- X #= X.
    X in inf..sup.
    

    这表明整数 X 的域没有受到任何限制 .

    用CLP(Z)复制结果

    让我们 balancer 竞争环境 . 我们可以通过人为地将变量的域限制为有限区间0..264来模拟SWI-Prolog的上述情况:

    ?- problem(A, B),
       Upper #= 2^64,
       [A,B] ins 0..Upper.
    

    作为回应,我们现在使用SWI-Prolog:

    A = 336,
    B = 16,
    Upper = 18446744073709551616.
    

    因此,将域限制为有限的整数子集使我们能够使用SWI-Prolog的CLP(FD)求解器或其后继者CLP(Z)复制我们从GNU Prolog中获知的结果 .

    原因

    CLP(Z)的目标是完全 replace low-level arithmetic predicates 用户程序 by high-level declarative alternatives 可以用作真正的关系,当然也可以作为替代品 . 因此,CLP(Z)支持无界整数,它可以增长到计算机内存允许的大小 . 在CLP(Z)中,所有整数变量的默认域是所有整数的集合 . 这意味着只要其中一个域是无限的,就不会执行应用于有界域的某些传播 .

    例如:

    ?- X #> Y, Y #> X.
    X#=<Y+ -1,
    Y#=<X+ -1.
    

    这是一个条件答案:如果所谓的残差约束是可满足的,则原始查询是可满足的 .

    相反,我们得到有限域:

    ?- X #> Y, Y #> X, [X,Y] ins -5000..2000.
    false.
    

    只要所有域都是有限的,我们期望所涉及的系统具有大致相同的传播强度 .

    固有的局限性

    求解整数方程式通常是undecidable . 因此,对于CLP(Z),我们知道没有决策算法能够始终产生正确的结果 .

    因此,您有时会获得剩余约束而不是无条件答案 . 在有限的整数集上,方程当然是可判定的:如果所有域都是有限的并且您没有得到具体的解决方案作为答案,请使用枚举谓词之一来穷举搜索解 .

    在可以推理无限整数集的系统中,你迟早会遇到这样的现象 .

相关问题