…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?
