论文部分内容阅读
本文在算法变换的思想指导下，研究了用吴方法求解可满足性问题的特点．通过建立吴方法的基本操作与子句间有限制的归结操作的对应，证明了吴方法求解可满足性问题基本上是一种以特征列计算为核心的有限制的子句归结过程，不仅使吴方法和归结法相互引入新的概念和认识，而且在算法实现时可以避免复杂的多项式计算，同时可以更好地利用问题特性和已有经验以获得更高的效率．