可满足性问题的归约技术

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

Reduction Techniques for Satisfiability Problems

A CNF formula can be transformed into another formula with some special structures or properties by a proper reduction transformation,such that two formulas have the same satisfiability.A classical reduction is transforming a general CNF formula to a 3-CNF formula.A given class of formulas can be transformed into a class with some regular structures by constructing some excellent gadgets.The minimal unsatisfiable formulas have a critical characterization,which the formula itself is unsatisfiable and the resulting formula moving anyone clause from the original formula is satisfiable.We introduce some reduction techniques by constructing proper minimal unsatisfiable formulas as gadgets for transformations of classes of formulas with some special requirements.It is helpful to investigate complexities and properties for satisfiable problems restricted regular structures.As an example,we can reduce a 3-CNF formula to a regular(3,4)-CNF formula,where each clause contains exactly three literals,and each variable appears exactly four times in a(3,4)-CNF formula.Therefore,the problem(3,4)-SAT is NP-complete,and then some properties of regular bigraphes will be helpful to investigate complexities of NP-hard problems.