可满足性问题的归约技术

摘要：

通过一个恰当的归约变换，可以将一个CNF公式变换为另一个具有某种特殊结构或性质的公式，使其两者具有相同的可满足性。一个典型的归约是将一般的CNF公式变换为3．GVF公式。通过构造一些恰当的工具，可以将公式类变换为所要求的正则类。极小不可满足公式具有一个临界特征，公式本身不可满足，从原始公式中删去任意一个子句后得到的公式可满足。我们提供了一种归约技术，通过构造恰当的极小不可满足公式作为工具，将公式类变换为具有正则结构的公式类。研究正则结构的公式的复杂性及性质很有意义。如，将一个从3．CNF公式变换为（3，4）一CNF公式，这里（3，4）一CNF公式是指公式中每个子句的长度恰为3，每个变元出现的次数恰为4。因此，（3，4）．SAT是一个NP．完全问题，并且正N-部图的诸多良好性质对于研究正则结构的SAT问题具有许多潜在的作用。

关键词：归约、技术、性问题、SAT、公式、结构、性质、复杂性

所属期刊栏目：5

分类号：N0(自然科学理论与方法论)

资助基金：The work is supported by the National Natural Science Foundation of China 600863005

在线出版日期：2012-08-02（万方平台首次上网日期，不代表论文的发表时间）

页数：共15页

页码：35-49