Lion 和 Unicorn 使用 Prolog SAT 求解器

Question

Prolog SAT 求解器在解决这个谜题方面是否有优势：

当爱丽丝进入遗忘森林时，她并没有 忘记一切，只忘记某些事情。她经常忘记她 名字，而她最容易忘记的就是那天 一周中的。现在，狮子和独角兽经常出现 来到这片森林的游客。这两个是奇怪的生物。这 狮子在周一、周二和周三撒谎并讲述 一周中其他日子的真相。独角兽，在 另一方面，周四、周五和周六撒谎，但告诉 一周中其他日子的真相。

有一天，爱丽丝遇到了在树下休息的狮子和独角兽。 他们发表了以下声明：

狮子：昨天是我撒谎的日子之一。
独角兽：昨天是我撒谎的日子之一。

从这些陈述中，聪明的女孩爱丽丝能够 推断出星期几。那是什么？

与此处的解决方案相比具有性能优势（免费访问）：

狮子与独角兽遇见PROLOG
https://dl.acm.org/doi/10.1145/382278.382395

Answer 1

将论文的解决方案复制到SWI Prolog中并查询

?- time(solve_for(Today)).

需要31个逻辑推理才能解决。使用两个变量 Lion AND Sunday 设置 CLPB，以表明如果今天是星期日，则狮子说的是真话：

:- use_module(library(clpb)).   % Boolean constraints

solve() :-
    sat(Lion * Sun),
    labeling([Lion, Sun]).

仅此一项就需要 588 次推论。与使用 CLPFD 类似，假设一周中的日子编号为一到七，然后我们直接选择一个：

:- use_module(library(clpfd)).   % Finite domain constraints 

solve(Day) :-
    Day in 1..7,
    Day = 2,
    label([Day]).

我们已经有了 154 个推论。通过为完整的解决方案添加更多代码，似乎都不太可能将推理次数降至 31 以下。

我认为这个难题太小了 - 搜索空间只有 7 天，而约束传播可以带来的最大好处是避免搜索其中的 6 天 - 并且节省的工作量不足以抵消设置约束的开销，进行约束传播，并调用求解器来搜索/标记解决方案。

一个很大的优点是将一些答案编码到简单的 Prolog 中：

lying_day(lion, monday).
lying_day(lion, tuesday).
lying_day(lion, wednesday).

lying_day(unicorn, thursday).
lying_day(unicorn, friday).
lying_day(unicorn, saturday).

solve_for(Today) :- 
    (member(Today, [tuesday, wednesday, thursday]),
     lying_day(unicorn, Today))
    ; (member(Today, [friday, saturday, sunday]),
       lying_day(lion, Today)).

“今天是狮子撒谎、独角兽撒谎之后的日子之一。或者今天是独角兽撒谎、狮子撒谎之后的日子之一”。 6 个推论。