利用正交方法解SAT问题  

Solving SAT Problems by Orthogonal Method

作　　者：荆明娥[1] 陈更生[1] 赵长虹[1] 唐璞山[1] 周电[1,2] 

机构地区：[1]复旦大学专用集成电路国家重点实验室 [2]E.E. Department,the University of Texasat Dallas,TX75083,USA

出　　处：《复旦学报（自然科学版）》2008年第6期786-790,共5页Journal of Fudan University：Natural Science

基　　金：国家自然科学基金资助项目(60773125,60673029);中国博士后科学基金资助项目;上海市自然科学基金资助项目(06ZR14016)

摘　　要：提出了一种解决SAT问题的新算法.该算法首先定义了子句之间的正交关系;然后从消除子句之间的交叠信息出发,利用正交子句的特性,结合有效的简化技术,逐渐将问题简化为一组与原问题完全等价的正交子句组;最后,根据正交子句组对整个赋值空间的覆盖情况来判断SAT是否满足.该算法为SAT问题的解决提供了一个新的思路.A novel algorithm for SAT problem is presented.Firstly,the orthogonal relation between the clauses is defined.Then,the algorithm utilizes the character of orthogonal clauses to eliminate the overlap information between clauses,and adopts effective simplification techniques to transform the SAT problem into an orthogonal clause group.Finally,the satisfiability of a SAT problem is verified by the covering of orthogonal clause group on the whole assignment space.Moreover,the algorithm provides a new idea for S...

关 键 词：可满足性问题 卡诺图 正交子句 NP完全问题 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]