%0 Journal Article
%T Solving Einstein''s Puzzle with SAT<br>Einstein谜的SAT求解
%A TIAN Cong
%A DUAN Zhen-hua
%A WANG Xiao-bing
%A <br>田聪
%A 段振华
%A 王小兵
%J 计算机科学
%D 2010
%I 
%X 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.
%K Einstein's puzzle
%K Propositional logic
%K SAT
%K Verification
%K Formal methods<br>Einstein谜
%K 命题逻辑
%K 可满足性
%K 验证
%K 形式化方法
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=64A12D73428C8B8DBFB978D04DFEB3C1&aid=AE71C0A8013D5EC44436341C2D172FC8&yid=140ECF96957D60B2&vid=42425781F0B1C26E&iid=94C357A881DFC066&sid=798FBE8DE1A255B1&eid=50BBDFAC8381694B&journal_id=1002-137X&journal_name=计算机科学&referenced_num=0&reference_num=6