Einstein谜的SAT求解

作者：田聪; 段振华; 王小兵

来源：计算机科学, 2010, (05): 184-186.

• Einstein谜
• 命题逻辑
• 可满足性
• 验证
• 形式化方法 Einstein's puzzle
• Propositional logic
• SAT
• Verification
• Formal methods

Einstein谜,亦称Zebra谜,是爱因斯坦在20世纪初提出的,他说世界上有98%的人答不出来。该问题是一个典型的逻辑推理题,可以通过SAT求解给出问题的答案。现将Einstein谜转换成SAT求解问题,并使用当前流行的SAT求解器,如MinSat,对Einstein谜进行自动求解。

• 单位
  西安电子科技大学; 软件工程国家重点实验室