Lion and Unicorn with Prolog SAT Solver

Question

Would a Prolog SAT solver have an advantage in solving this riddle:

When Alice entered the forest of forgetfulness, she did not forget everything, only certain things. She often forgot her name, and the most likely thing for her to forget was the day of the week. Now, the lion and the unicorn were frequent visitors to this forest. These two are strange creatures. The lion lies on Mondays, Tuesdays, and Wednesdays and tells the truth on the other days of the week. The unicorn, on the other hand, lies on Thursdays, Fridays, and Saturdays, but tells the truth on the other days of the week.

One day Alice met the lion and the unicorn resting under a tree. They made the following statements:

Lion: Yesterday was one of my lying days.
Unicorn: Yesterday was one of my lying days.

From these statements, Alice, who was a bright girl, was able to deduce the day of the week. What was it?

Performance advantage over a solution like here (Free Access):

The lion and the unicorn met PROLOG
Bruce Ramsey - 1986
https://dl.acm.org/doi/10.1145/382278.382395

Answer 1

Ok, I was using a SAT solver in a little unorthodox way.
Used it as a compiler for a formula, so that I got:

yesterday(0,0,0,1,1,0).
yesterday(0,0,1,0,0,0).
yesterday(0,1,0,0,0,1).
yesterday(0,1,1,0,1,0).
yesterday(1,0,0,0,1,1).
yesterday(1,0,1,1,0,0).
yesterday(1,1,0,1,0,1).

two_liars(T1,T2,T3,Y1,Y2,Y3) :-
   T1=\=Y1,
   T1=:=(T1/\Y2) xor (T1/\Y3) xor (Y2/\Y3),
   Y1=:=(T2/\T3) xor (T2/\Y1) xor (T3/\Y1),
   T1=\=(T1/\T2) xor (T1/\T3) xor T2 xor (T2/\T3) xor T3,
   Y1=\=(Y1/\Y2) xor (Y1/\Y3) xor Y2 xor (Y2/\Y3) xor Y3.

solve_for(T1,T2,T3) :-
   yesterday(T1,T2,T3,Y1,Y2,Y3),
   two_liars(T1,T2,T3,Y1,Y2,Y3).

Works fine and is fast with optimise=true:

/* SWI-Prolog 9.1.17, optimise=false */
?- time(solve_for(T1,T2,T3)).
% 16 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
T1 = 1,
T2 = T3, T3 = 0 ;
% 10 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
false.

/* SWI-Prolog 9.1.17, optimise=true */
?- time((between(1, 1000000, _), solve_for(T1,T2,T3), fail; true)).
% 9,999,999 inferences, 1.203 CPU in 1.199 seconds
(100% CPU, 8311687 Lips)

Edit 14.11.2023
So how to use a SAT solver as a compiler. First model
the problem with library(clpb) as Boolean formulas.

lying_day(A, B, C, D, M) :- M = (
   ~A* ~B* ~C*D+
   ~A* ~B*C* ~D+
   ~A* ~B*C*D+
   A*B* ~C* ~D+
   A*B* ~C*D+
   A*B*C* ~D).

two_liars(T1, T2, T3, Y1, Y2, Y3, ((M1#M2)*(M3#M4))) :-
    lying_day(0, T1, T2, T3, M1),
    lying_day(0, Y1, Y2, Y3, M2),
    lying_day(1, T1, T2, T3, M3),
    lying_day(1, Y1, Y2, Y3, M4).

Then look at the normalform:

?- two_liars(T1,T2,T3,Y1,Y2,Y3,M), sat(M).
sat(1#T2*T3#T2*Y1#T3*Y1#Y1),
sat(T1=:=T1*Y2#T1*Y3#Y2*Y3),
sat(T1=\=Y1),
sat(T1=\=T1*T2#T1*T3#T2#T2*T3#T3),
sat(Y1=\=Y1*Y2#Y1*Y3#Y2#Y2*Y3#Y3).

Take the normalform, reorder the equations a little bit, fewer
variables first, and rewrite them into ISO core standard bitwise
operations, and then take profit.

Answer 2

Preventing execution of yesterday_today twice:

lying_day(lion, mon).
lying_day(lion, tue).
lying_day(lion, wed).

lying_day(unicorn, thu).
lying_day(unicorn, fri).
lying_day(unicorn, sat).

yesterday_today(mon, tue).
yesterday_today(tue, wed).
yesterday_today(wed, thu).
yesterday_today(thu, fri).
yesterday_today(fri, sat).
yesterday_today(sat, sun).
yesterday_today(sun, mon).

lion_unicorn(Today) :-
    animal_consistent_day(lion, Yesterday, Today),
    % Don't call yesterday_today again, for performance
    animal_consistent(unicorn, Yesterday, Today).

animal_consistent_day(Animal, Yesterday, Today) :-
    % Delay yesterday_today, for performance
    lying_day(Animal, Yesterday),
    yesterday_today(Yesterday, Today),
    % Telling truth
    \+ lying_day(Animal, Today).
animal_consistent_day(Animal, Yesterday, Today) :-
    % Lying
    lying_day(Animal, Today),
    yesterday_today(Yesterday, Today),
    \+ lying_day(Animal, Yesterday).

animal_consistent(Animal, Yesterday, Today) :-
    lying_day(Animal, Yesterday),
    % Telling truth
    \+ lying_day(Animal, Today).
animal_consistent(Animal, Yesterday, Today) :-
    % Lying
    lying_day(Animal, Today),
    \+ lying_day(Animal, Yesterday).

Results in swi-prolog:

?- time(lion_unicorn(D)).
% 14 inferences, 0.000 CPU in 0.000 seconds (71% CPU, 1219406 Lips)
D = thu ;
% 16 inferences, 0.000 CPU in 0.000 seconds (91% CPU, 1453224 Lips)
false.

?- time((between(1, 1000000, _), lion_unicorn(_), fail; true)).
% 27,000,001 inferences, 1.314 CPU in 1.316 seconds (100% CPU, 20540412 Lips)

Answer 3

For example one can use four facts and(0,0,0), and(0,1,1), and(1,0,1) and and(1,1,1) to find solution to propositional conjunctions. A SAT solver is a computer program which aims to solve the Boolean satisfiability problem.

Here is a first SAT solving like solution. Unlike other posts, which assume that SAT means library(clpb), I don't assume that. Maybe the below sketch is a starting point for nevertheless some SAT solution that gives it an itch of additional speed?

yesterday(0,0,0,1,1,0).
yesterday(0,0,1,0,0,0).
yesterday(0,1,0,0,0,1).
yesterday(0,1,1,0,1,0).
yesterday(1,0,0,0,1,1).
yesterday(1,0,1,1,0,0).
yesterday(1,1,0,1,0,1).

lying_day(0,0,0,1).
lying_day(0,0,1,0).
lying_day(0,0,1,1).
lying_day(1,1,0,0).
lying_day(1,1,0,1).
lying_day(1,1,1,0).

solve_for(T1,T2,T3) :- yesterday(T1,T2,T3,Y1,Y2,Y3)
, contrary(lying_day(0,T1,T2,T3), lying_day(0,Y1,Y2,Y3))
, contrary(lying_day(1,T1,T2,T3), lying_day(1,Y1,Y2,Y3)).

contrary(S,T) :- \+ S, T.
contrary(S,T) :- S, \+ T.

Also unlike other posts that claim SAT is automatically expensive, since they assume its library(clpb), I only see so far that it has same speed with Bruce Ramseys solution:

?- time(solve_for(T1,T2,T3)).
% 32 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
T1 = 1,
T2 = T3, T3 = 0 ;
% 17 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
false.

?- time((between(1,1000000,_), solve_for(T1,T2,T3), fail; true)).
% 46,000,000 inferences, 3.813 CPU in 3.802 seconds (100% CPU, 12065574 Lips)
true.

Answer 4

Preventing a separate lookup for yesterday_today:

lying_day(lion, mon, tue).
lying_day(lion, tue, wed).
lying_day(lion, wed, thu).

lying_day(unicorn, thu, fri).
lying_day(unicorn, fri, sat).
lying_day(unicorn, sat, sun).

lion_unicorn(Today) :-
    animal_consistent(lion, Yesterday, Today),
    animal_consistent(unicorn, Yesterday, Today).

animal_consistent(Animal, Yesterday, Today) :-
    lying_day(Animal, Yesterday, Today),
    % Telling truth
    \+ lying_day(Animal, Today, _).
animal_consistent(Animal, Yesterday, Today) :-
    % Lying
    lying_day(Animal, Today, _),
    \+ lying_day(Animal, Yesterday, Today).

Results in swi-prolog:

?- time(lion_unicorn(D)).
% 11 inferences, 0.000 CPU in 0.000 seconds (85% CPU, 1104529 Lips)
D = thu ;
% 13 inferences, 0.000 CPU in 0.000 seconds (91% CPU, 1176364 Lips)
false.

?- time((between(1, 1000000, _), lion_unicorn(_), fail; true)).
% 21,000,001 inferences, 1.183 CPU in 1.184 seconds (100% CPU, 17755003 Lips)