如何在 Prolog 中创建算术和不等式约束

Question

我是 Prolog 的新手，我有兴趣将以下单词问题转换为 (SWI) Prolog：

有 4 个孩子：Abe、Dan、Mary 和 Sue。他们的年龄，排名不分先后，分别是 3、5、6 和 8 岁。Abe 比 Dan 大。苏比玛丽年轻。苏的年龄是丹的年龄加上 3 岁。 Mary 比 Abe 大。

到目前为止，我想出了

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

整数的算术约束，例如这个谜题中的约束，最好用 Prolog 系统的 CLP(FD) 约束来表达。

例如，在 SICStus Prolog、YAP 或 SWI 中：

:- 使用模块（库（clpfd））。 年龄（作为）：- As = [Abe,Dan,Mary,Sue], % 有 4 个孩子：Abe, Dan, Mary, Sue 如 ins 3\/5\/6\/8, % 他们的年龄分别是 3、5、6 和 8 all_different(As), Abe #> Dan, % Abe 比 Dan 年长 Sue #安倍。 % Mary 比 Abe 大

示例查询及其结果：

?- 年龄（[Abe,Dan,Mary,Sue]）。 安倍 = 5, 丹 = 3, 玛丽 = 8, 苏 = 6。

我们从这个答案中看到，这个谜题有一个独特的解决方案。

请注意，无需任何搜索才能获得此答案！约束求解器通过称为约束传播的强大隐式机制推导出唯一解，这是 CLP 系统优于蛮力搜索的关键优势。在此示例中成功使用约束传播来修剪除搜索树的一个剩余分支之外的所有分支。

Answer 2

answer by @WillemVanOnsem——使用低级算术生成和测试——是老派：

• 旧版 Prolog 代码将获取所有低级过程细节的负担直接交给您。

• Debugging / optimizing 遗留代码通常归结为 program tracing 的某些变体。

相比之下， @mat's code 在通用性/多功能性/稳健性、声明性、简洁性、效率等方面胜出！怎么会？运气？天才？神干预？可能每个都有一点，但主要原因是：@mat 使用高级工具。 @mat 使用clpfd。

好消息！ clpfd 普遍可用。使用它并获得好处：

• 注意@mat 的 Prolog 代码和原始规范有多接近！

• 代码保留logical-purity。这会产生重要的后果：

  • 可以使用高级调试方法（利用纯 Prolog 代码的有用代数属性）！

  • 也可以进行低级调试， 但要先探索高级方法！

Answer 3

由于值在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) 工具可能是解决此问题的最佳方法。