Einstein谜的SAT求解

摘要：

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

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

所属期刊栏目：37

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金重点基金项目60433010;国家自然科学基金项目60373103,60873018;总装115预研项目51315050105;教育部博士点基金200807010012;软件工程国家重点实验室SKLSE20080713

在线出版日期：2010-06-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：184-186