# How to solve the liar problem?

In an island live two kinds of people: liar and truth-teller, the former only tells lies and the latter only tells truth, now there're two men A and B from the island, A said: "B is a truth-teller." B said: "We two are different kinds of people." Please identify the sort of them.

If we mark A with a and B with b and use True to represent truth-teller, the answer is apparently b == False && a == False . This seems to be easy to translate into mathematica code, I first tried:

Reduce[{Refine[a, b == True] == False, Refine[b, a == True] == True}]
(* b == True && a == False *)


…What's this? Maybe I have some misunderstandings for the Functions… I didn't think much and tried another approach:

Reduce[{Implies[b == True, a == ! b], Implies[a == True, b == True]}, {a, b}]
(* (a == False && b == True) || (a - True) (-b + True) != 0 *)


…What's this? Maybe I have some misunderstandings for the Functions… I didn't think much and tried my third approach:

Reduce[{If[b == True, a == ! b, a == b], If[a == True, b == True, b == False]}]
(*b == False && a == False && False - True != 0*)


…This time I get the right answer, but what's False - True != 0!? Reduce doesn't know booleans?

Surely I'm not solving the problem in the right way, how to get the answer properly with mma? And I would be appreciate if you can tell me where I'm wrong in the first two samples.

…I forgot a important thing: in logic, if $p$ is false and $q$ is true, then $p\Rightarrow q$ is still true, so my first two translations for the liar problem is incomplete and the third one is correct because I unconsciously add the missing rule in If, so my second sample should be modified to:

Reduce[Implies[b == True, a == ! b] &&
Implies[b == False, a == b] &&
Implies[a == True, b == True] &&
Implies[a == False, b == False], {a, b}]
(*
(a == False && b == False && False - True != 0) ||
(a - False) (-b + False) (a - True) (b - True) != 0
*)


Though the result is still a little strange, at least this time the right answer is involved in it, and together with the comment from @Daniel Lichtblau it's not that unacceptable now.

And of course the answer from @halirutan using !Xor is terser.

And had I noticed the correct syntax for SatisfiabilityInstances earlier, perhaps I would have lost my curiosity and this question wouldn't exist anymore…:

SatisfiabilityInstances[Implies[b == True, a == ! b] &&
Implies[b == False, a == b] &&
Implies[a == True, b == True] &&
Implies[a == False, b == False], {a, b}]
(* {{False, False}} *)

SatisfiabilityInstances[If[b == True, a == ! b, a == b] &&
If[a == True, b == True, b == False], {a, b}]
(* {{False, False}} *)


However, I'm still unable to give a good explanation for my first sample: as we've seen, it gives an answer similar to the second sample, but:

SatisfiabilityInstances[Refine[a, b == True] == ! b &&
Refine[a, b == False] == b &&
Refine[b, a == True] == True &&
Refine[b, a == False] == False, {a, b}]
(* {} *)


…Why?

…I get the truth: Refine is not available for the logical judgement，and the "right" answer for the first sample is just a illusion, that's just because a and b don't have a explicit relationship so the assumption inside Refine is considered as something meaningless by Reduce, the process is similar to:

Reduce[{Refine[a, b == 3] == 1, Refine[b, a == 4] == 2}]
(* b == 2 && a == 1 *)


OK, now it's all clear 囧.

-
In the Booleans, you can always replace b == True with just b, and If[a, b, !b] with a == b. So then you can do Solve[{a == b, b == (a != b)}] and get {{b -> False, a -> False}}. I'm not familiar with the other functions you used, but surely someone more knowledgeable will come along and explain why they don't work. – Rahul Narain Nov 3 '12 at 9:52
@RahulNarain Hehe, I'm unfamiliar with them, too. In fact it's the first time I use Refine and Implies in my code. – xzczd Nov 3 '12 at 10:04
Reduce is not readily able to handle booleans as such. You can convert to algebraic equations in Z_2 if you want to go that route. Or else use the nice methods indicated by Halirutan. I'd probably go that latter route myself. – Daniel Lichtblau Nov 3 '12 at 19:38
@DanielLichtblau Er…what does Z_2 mean? – xzczd Nov 4 '12 at 6:52
Various notations: Z_2 == Z/<2> == GF[2] == finite field comprised of {0,1}. – Daniel Lichtblau Nov 4 '12 at 17:01
show 2 more comments

Have you seen, that Mathematica is capable of many boolean computations using special boolean functions? Let's assume someone from the island makes a statement, then when the statment is true, whether or not he tells the statement is true, depends on whether or not he is a truth-teller. When we know, which kind he is, we know the correct statement through what he says. Therefore, let's define a function for this and check the truth-table

trueStatement[statement_,isTruthTeller_]:=!Xor[statement,isTruthTeller]
BooleanTable[{a,b,trueStatement[a,b]},{a,b}]//TableForm
(*
True    True    True
True    False   False
False   True    False
False   False   True
*)


So, if A says a statement is true and A is a truth-teller, the statement is true for sure. On the the other hand if A is not a truth-teller, then the real statement is false.

Now we want to transform the two statements

A said: "B is a truth-teller." B said: "We two are different kinds of people."

without knowing whether a or b are liars or truth-tellers

eq = trueStatement[b, a] && trueStatement[a == ! b, b]


The statements read as: a says that b is a truth-teller and b says, that a is not of the same kind as b. Now we can simply do

SatisfiabilityInstances[eq, {a, b}]

(* {{False, False}} *)


Therefore, both, a and b are liars.

-
 Well…in fact I've already tried SatisfiabilityInstances but failed, because I didn't notice that we can combine equations with either && or {} in Solve and Reduce while only && is available for SatisfiabilityInstances囧. Also, I notice the mistake in my original analysis, see my edit of the question for more details. – xzczd Nov 4 '12 at 6:53