可满足性问题全部解的求解算法

Algorithm for finding all-solutions of satisfiablity problem

SAT问题在人工智能、计算机基础理论研究和人工智能等领域有着广泛的应用,近年来,证明该问题的可满足性取得了巨大的成功,但在求出SAT问题的所有解方面还有待进一步研究。利用一个简单的变换,将可满足性(SAT)问题转化为多项式形式,然后根据命题逻辑的性质以及多项式的性质,得到一个求解出SAT问题所有解的算法。

Satisfiability problem has been widely used in many fields such as artificial intelligence,computer theory research and computation theory.Many algorithms about this NP-hard problem have been built,but how to get all of the truth assignments is still difficult.By establishing the correspondence between the primitive operation in polynomial and clause solution in SAT,an efficient algorithm has been built to obtain all solutions which satisfied the problem.Experiment shows that the new algorithm is feasible.