论文部分内容阅读
通过一个恰当的归约变换，可以将一个CNF公式变换为另一个具有某种特殊结构或性质的公式，使其两者具有相同的可满足性。一个典型的归约是将一般的CNF公式变换为3．GVF公式。通过构造一些恰当的工具，可以将公式类变换为所要求的正则类。极小不可满足公式具有一个临界特征，公式本身不可满足，从原始公式中删去任意一个子句后得到的公式可满足。我们提供了一种归约技术，通过构造恰当的极小不可满足公式作为工具，将公式类变换为具有正则结构的公式类。研究正则结构的公式的复杂性及性质很有意义。如，将一个从3．CNF公式变换为（3，4