| Einstein谜的SAT求解 |
| |
| 引用本文： | 田聪,段振华,王小兵.Einstein谜的SAT求解[J].计算机科学,2010,37(5):184-186. |
| |
| 作者姓名： | 田聪 段振华 王小兵 |
| |
| 作者单位： | 1. 西安电子科技大学计算理论与技术研究所,西安,710071;武汉大学软件工程重点实验室,武汉,430072
2. 西安电子科技大学计算理论与技术研究所,西安,710071 |
| |
| 基金项目： | 国家自然科学基金重点基金项目(60433010);;国家自然科学基金项目(60373103,60873018);;总装115预研项目(51315050105);;教育部博士点基金(200807010012);;软件工程国家重点实验室(SKLSE20080713)资助 |
| |
| 摘 要： | Einstein谜,亦称Zebra谜,是爱因斯坦在20世纪初提出的,他说世界上有98%的人答不出来。该问题是一个典型的逻辑推理题,可以通过SAT求解给出问题的答案。现将Einstein谜转换成SAT求解问题,并使用当前流行的SAT求解器,如MinSat,对Einstein谜进行自动求解。
|
| 关 键 词： | Einstein谜 命题逻辑 可满足性 验证 形式化方法 |
| 收稿时间： | 6/8/2009 12:00:00 AM |
| 修稿时间： | 9/3/2009 12:00:00 AM |
Solving Einstein's Puzzle with SAT |
| |
| TIAN Cong,DUAN Zhen-hu,WANG Xiao-bing.Solving Einstein's Puzzle with SAT[J].Computer Science,2010,37(5):184-186. |
| |
| Authors: | TIAN Cong DUAN Zhen-hu WANG Xiao-bing |
| |
| Affiliation: | Institute of Computing Theory and Technology/a>;Xidian University/a>;Xi'an 710071/a>;China;State Key Laboratory of Software Engineering/a>;Wuhan University/a>;Wuhan 430072/a>;China |
| |
| 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. |
| |
| Keywords: | Einstein's puzzle Propositional logic SAT Verification Formal methods |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
