二元可满足性问题有解的充要条件

AN SUFFICIENT AND NECESSARY CONDITION FOR 2SAT PROBLEM

二元可满足性问题是一个多项式可解的问题．本文首先证明了该问题有解的充要条件，然后给出了判定该问题的一个新的多项式算法．如果判定某个表达式是可满足的话，那么求解算法不需要任何回溯就能准确地给出它的每个解．本文试图通过对二元可满足性的研究为研究其它问题提供一点启示．

Satisfiability (2SAT) is a determinable problem in polynomial time. This paper proves a sufficient and necessary condition for 2SAT problem, and presents a new polynomial algorithm for 2SAT problem. In addition, if one 2 CNF expression is satisfiable, the algorithm for solution can give every solution without backtracking. This paper tries to give some idea for other problem through the study of 2SAT problem.