% You are on an island where every inhabitant is either a knight or a
% knave. Knights always tell the truth, and knaves always lie. The
% following examples show how various cases can be solved with CLP(B),
% Constraint Logic Programming over Boolean variables.
% These examples appear in Raymond Smullyan's "What Is the Name of
% this Book" and Maurice Kraitchik's "Mathematical Recreations".
:- use_module(library(clpb)).
% We use Boolean variables A, B and C to represent the inhabitants.
% Each variable is true iff the respective inhabitant is a knight.
% Notice that no search is required for any of these examples.
% Example 1: You meet two inhabitants, A and B.
% A says: "Either I am a knave or B is a knight."
example_knights(1, [A,B]) :-
sat(A=:=(~A + B)).
% Example 2: A says: "I am a knave, but B isn't."
example_knights(2, [A,B]) :-
sat(A=:=(~A * B)).
% Example 3: A says: "At least one of us is a knave."
example_knights(3, [A,B]) :-
sat(A=:=card([1,2],[~A,~B])).
% Example 4: You meet 3 inhabitants. A says: "All of us are knaves."
% B says: "Exactly one of us is a knight."
example_knights(4, Ks) :-
Ks = [A,B,C],
sat(A=:=(~A * ~B * ~C)),
sat(B=:=card([1],Ks)).
% Example 5: A says: "B is a knave."
% B says: "A and C are of the same kind."
% What is C?
example_knights(5, [A,B,C]) :-
sat(A=:= ~B),
sat(B=:=(A=:=C)).
/**
?- example_knights(1, [A,B]).
?- example_knights(2, [A,B]).
?- example_knights(Example, Knights).
*/