论文部分内容阅读
通过一个适当的归约变换，可以将一个CNF（conjunctive normal form）公式变换为另一个具有某种特殊结构或性质的公式，使两者具有相同的可满足性。带有正则结构的CNF公式的因子图在图论中具有某些良好的性质和结果，可以用于研究公式的可满足性和计算复杂性。极小不可满足公式具有一个临界特征，公式本身不可满足，从原始公式中删去任意一个子句后得到的公式可满足。借助此临界特性，给出了一个从3-CNF公式到正则（3，4）-CNF公式的多项式归约转换。这里，正则（3，4）-CNF公式是指公式中每个子句的长