Einstein谜的SAT求解

计算机科学 ›› 2010, Vol. 37 ›› Issue (5): 184-186.

Einstein谜的SAT求解

田聪,段振华,王小兵

(西安电子科技大学计算理论与技术研究所西安710071);(武汉大学软件工程重点实验室武汉430072)

出版日期:2018-12-01 发布日期:2018-12-01
基金资助:
本文受国家自然科学基金重点基金项目(60433010)，国家自然科学基金项目(60373103,608730L8)，总装115预研项目(51315050105)，教育部博士点基金(200807010012)以及软件工程国家重点实验室(SKLSE20080713)资助。

Solving Einstein's Puzzle with SAT

TIAN Cong,DUAN Zhen-hua,WANG Xiao-bing

Online:2018-12-01 Published:2018-12-01

摘要/Abstract

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

关键词: Einstein谜，命题逻辑，可满足性，验证，形式化方法

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

田聪,段振华,王小兵. Einstein谜的SAT求解[J]. 计算机科学, 2010, 37(5): 184-186. https://doi.org/

TIAN Cong,DUAN Zhen-hua,WANG Xiao-bing. Solving Einstein's Puzzle with SAT[J]. Computer Science, 2010, 37(5): 184-186. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed