Trouble modelling a burglar puzzle in Prolog

Question

I am trying to model this simple logic puzzle:

Only one of three people, Alice, Beto, and Carl stole the money from Ms. Doubtfire. She hires you as a consultant detective. After interrogating them each, you have the following:

Alice : Don't trust Carl. He is lying and he took the money.

Carl : Beto is lying but Alice didn't take the money.

Beto : Carl took the money. I didn't take the money.

After gathering information, you know that whenever one of them lies, they lied for both parts of their statement. Also, if one of them tells the truth, they tell the truth for both parts of their statement. Who took the money?

I modeled it in a similar fashion to this video about Knights and Knaves. In particular, I modeled it off the "Prolog based" solution near 11:34 instead of the SAT solver based one presented earlier. I made some adaptations to the false relation.

says(guilty_liar, S) :- not(S).
says(innocent_liar, S) :- not(S).
says(guilty_but_honest, S) :- S.
says(innocent_and_honest, S) :- S.

false(A = guilty_liar) :- A = innocent_and_honest.
false(A = guilty_but_honest) :- A = innocent_liar.
false(A = innocent_liar) :- A = guilty_but_honest.
false(A = innocent_and_honest) :- A = guilty_liar.
false((P ; Q)) :- false(P), false(Q) .
false((P , Q)) :- ( false(P) ; false(Q) ).

Then I would make the following queries:

?- [burglar].
  true.

?- says(A, (C = guilty_liar)), says(C, ((B = guilty_liar ; B = innocent_liar), (A = innocent_liar ; A = innocent_and_honest ))), says(B, ((C = guilty_liar ; C = guilty_but_honest) , (B = innocent_and_honest ; B = innocent_liar))).
    A = guilty_but_honest,
    C = B, B = guilty_liar ;
    A = guilty_but_honest,
    C = guilty_liar,
    B = innocent_and_honest ;
  false.

Although I would expect more than the correct solution (because I haven't put all the restraints down), I would expect the correct solution to show up; namely, Alice is innocent but lying, Carl is telling the truth, and Beto is a guilty liar.

Also, here is the second query split across multiple lines for easier reading:

says(A, (C = guilty_liar)),
says(C, ((B = guilty_liar ; B = innocent_liar), (A = innocent_liar ; A = innocent_and_honest ))),
says(B, ((C = guilty_liar ; C = guilty_but_honest) , (B = innocent_and_honest ; B = innocent_liar))).

I am confused why the correct solution is not showing up.

---

UPDATE

I stupidly used not instead of the false function that I defined, however, even switching out not(S) with false(S) gives simply false. for the query.

Answer 1

Can solve using clpb:

:- use_module(library(clpb)).

bools_person('100', alice).
bools_person('010', beto).
bools_person('001', carl).

says(P, Statements) :-
    length(Statements, Len),
    % All truth xor all lies
    sat((P * card([Len], Statements)) # (~P * card([0], Statements))).
    
burglar :-
    % There are 3 people who could be the burglar
    Burglar = [A, B, C],

    % Only 1 person is the burglar
    sat(card([1], Burglar)),

    % In person name order, for consistency
    % The person variable is whether they are truthful
    says(_Alice, [~Carl, C]),
    says(Beto, [C, ~B]),
    says(Carl, [~Beto, ~A]),

    % Turn into ground alternatives
    labeling(Burglar),

    atomic_list_concat(Burglar, Bools),
    bools_person(Bools, Culprit),
    write(Culprit),
    writeln(' is the burglar').

Result in swi-prolog:

?- burglar.
beto is the burglar
true.

The says(_Alice, [~Carl, C]) constraint or the says(Beto, [C, ~B]) constraint (but not both) can be removed, with the same result.

Answer 2

This looks very suspicous to me: says(A, (C = guilty_liar)). There is supposed to be a constraint that both statements are true or both are false, and here you have only one statement. You think your logic handles this correctly?

Anyway here is my naive solution :-) Creating a true/false variable for each proposition and expressing all constraints in therms of these variables.

true_or_false(X) :- X = true.
true_or_false(X) :- X = false.

bool_to_int(true, 1).
bool_to_int(false, 0).

true_or_false_list([]).
true_or_false_list([V | T]) :- true_or_false(V), true_or_false_list(T).

solution(AliceCorrect, CarlCorrect, BetoCorrect,
         AliceThief, CarlThief, BetoThief) :-
  true_or_false_list([AliceCorrect, CarlCorrect, BetoCorrect,
                      AliceThief, CarlThief, BetoThief]),
  % Alice statement.
  AliceCorrect \= CarlCorrect,
  AliceCorrect = CarlThief,
  % Carl statement.
  CarlCorrect \= BetoCorrect,
  CarlCorrect \= AliceThief,
  % Beto Statement.
  BetoCorrect = CarlThief,
  BetoCorrect \= BetoThief,
  % There can be only one thief.
  bool_to_int(AliceThief, AliceThiefInt),
  bool_to_int(CarlThief, CarlThiefInt),
  bool_to_int(BetoThief, BetoThiefInt),
  1 is AliceThiefInt + CarlThiefInt + BetoThiefInt.

Beto is a thief.

Answer 3

I did it this way:

?- People = [alice(_, _), beto(_, _), carl(_, _)], alice(People), carl(People), beto(People), write(People), nl, fail.

alice(People) :-
    member(alice(honest, innocent), People),
    member(carl(liar, thief), People).

alice(People) :-
    member(alice(liar, _), People),
    member(carl(honest, innocent), People).

carl(People) :-
    member(carl(honest, _), People),
    member(beto(liar, _), People),
    member(alice(_, innocent), People).

carl(People) :-
    member(carl(liar, _), People),
    member(beto(honest, _), People),
    member(alice(_, thief), People).

beto(People) :-
    member(beto(honest, innocent), People),
    member(carl(_, thief), People).

beto(People) :-
    member(beto(liar, thief), People),
    member(carl(_, innocent), People).

The result [alice(liar, innocent), beto(liar, thief), carl(honest, innocent)].

---

This is slightly simpler:

alice([alice(honest, innocent), beto(_, _), carl(liar, thief)]).        
alice([alice(liar, _), beto(_, _), carl(honest, innocent)]).
carl([alice(_, innocent), beto(liar, _), carl(honest, _)]).     
carl([alice(_, thief), beto(honest, _), carl(liar, _)]).
beto([alice(_, _), beto(honest, innocent), carl(_, thief)]).
beto([alice(_, _), beto(liar, thief), carl(_, innocent)]).