Abstract: Einstein Puzzle, or Zebra Puzzle, is a widely known riddle given by Einstein in the early 20th century. He said 98% people in the world cannot solve this riddle. The question is a typical logical question which can be formalized as a SAT problem. We investigated how to solve the riddle by SAT. And then the currently popular SAT solvers, such as MinSat, was employed in solving this riddle automatically.

Key words: Einstein's puzzle, Propositional logic, SAT, Verification, Formal methods