如何在Prolog中创建算法约束和不相等约束

Question

我对Prolog非常陌生，我有兴趣将以下单词问题转换为(SWI) Prolog：

有四个孩子:亚伯，丹，玛丽和苏。他们的年龄，没有特别的顺序，是3，5，6和8岁。亚伯比丹老。苏比玛丽年轻。苏的年龄是丹的年龄加上3岁。玛丽比亚伯大。

到目前为止我已经想出了

child(X) :-
    member(X, [3,5,6,8]).

solution(Abe, Dan, Mary, Sue) :-
    child(Abe),
    child(Dan),
    child(Mary),
    child(Sue),
    Abe > Dan,
    Sue < Mary,
    Sue == Dan+3,
    Mary > Abe,
    Abe \== Dan,
    Abe \== Mary,
    Abe \== Sue,
    Dan \== Mary,
    Dan \== Sue,
    Mary \== Sue.

但是运行查询

?- solution(Abe, Dan, Mary, Sue)

我刚得到false。作为一个附带的问题，Prolog是执行蛮力搜索解决方案，还是有比O(n!)更好地解决这个(某种程度上)问题的机制？

我想要的结果是Abe = 5, Dan = 3, Mary = 9, Sue = 6。

Answer 1

答复：@WillemVanOnsem-generate和低水平算术测试-是老派的

• 遗留Prolog代码将所有低级的过程细节都交给了您。
• 调试/优化遗留代码通常归结为程序跟踪的某些变体。

相比之下，@mat密码在通用性/多功能性/健壮性、声明性、简洁性、效率等方面赢得了胜利！怎么会这样?运气？天才？神的干预？这两种工具可能各有一点，但主要原因是：@mat使用的是高级工具。@mat使用clpfd。

好消息！clpfd是通用的。使用它并从中获益：

• 请注意@mat的Prolog代码和原始规范有多近！
• 代码保留逻辑纯度。这将产生重要后果：

- High-level debugging methods (which harness useful algebraic properties of pure Prolog code) can be used!
- Low-level debugging is _also_ possible, but explore **high-level methods first!**

​

Answer 2

由于这些值是在child调用之后接地的，所以可以使用is运算符：

child(X) :-
    member(X, [3,5,6,8]).
solution(Abe, Dan, Mary, Sue) :-
    child(Abe),
    child(Dan),
    child(Mary),
    child(Sue),
    Abe > Dan,
    Sue < Mary,
    Sue is Dan+3,
    Mary > Abe,
    Abe =\= Dan,
    Abe =\= Mary,
    Abe =\= Sue,
    Dan =\= Mary,
    Dan =\= Sue,
    Mary =\= Sue.

您可以通过交错生成和测试来进一步提高性能，而不是先生成然后测试：

child(X) :-
    member(X, [3,5,6,8]).
solution(Abe, Dan, Mary, Sue) :-
    child(Abe),
    child(Dan),
    Abe > Dan,
    Abe =\= Dan,
    child(Mary),
    Mary > Abe,
    Abe =\= Mary,
    Dan =\= Mary,
    Sue is Dan+3,
    Sue < Mary,
    child(Sue),
    Abe =\= Sue,
    Dan =\= Sue,
    Mary =\= Sue.

然后，您还可以消除一些不相等的谓词(=\=)，因为它们是由小于(<)或大于(>)谓词或is谓词所隐含的：

child(X) :-
    member(X, [3,5,6,8]).
solution(Abe, Dan, Mary, Sue) :-
    child(Abe),
    child(Dan),
    Abe > Dan,
    child(Mary),
    Mary > Abe,
    Dan =\= Mary,
    Sue is Dan+3,
    Sue < Mary,
    child(Sue),
    Abe =\= Sue.

然而，使用约束逻辑编程(CLP)工具可能是解决此问题的最佳方法。