求合取范式可满足性问题全部解的一个算法

设p1,p2,…,pn是一些命题符,--pi是pi的否定.考虑由pi,--pi(i=1,2,…,n)构成的文字符集合q,其中的若干个文字符q1,q2,…,q1通过"或者关系"v构成一个子句:……