【摘要】 提出了一种解决SAT问题的新算法.该算法首先定义了子句之间的正交关系;然后从消除子句之间的交叠信息出发,利用正交子句的特性,结合有效的简化技术,逐渐将问题简化为一组与原问题完全等价的正交子句组;最后,根据正交子句组对整个赋值空间的覆盖情况来判断SAT是否满足.该算法为SAT问题的解决提供了一个新的思路.更多还原

【Abstract】 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 SAT problems other than the well-known DPLL and DP algorithms.更多还原