摘要
通过一个适当的归约变换,可以将一个CNF(conjunctive normal form)公式变换为另一个具有某种特殊结构或性质的公式,使两者具有相同的可满足性。带有正则结构的CNF公式的因子图在图论中具有某些良好的性质和结果,可以用于研究公式的可满足性和计算复杂性。极小不可满足公式具有一个临界特征,公式本身不可满足,从原始公式中删去任意一个子句后得到的公式可满足。借助此临界特性,给出了一个从3-CNF公式到正则(3,4)-CNF公式的多项式归约转换。这里,正则(3,4)-CNF公式是指公式中每个子句的长度恰为3,每个变元出现的次数恰为4。因此,正则(3,4)-SAT问题是一个NP-完全问题,并且MAX(3,4)-SAT是不可近似问题。
A CNF （conjunctive normal form） 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. The factor graphs of CNF formulas with regular structures have some well properties and known results in theory of graph, which may be applied to investigating the satisfiability and complexity of formulas. 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. By this critical characterization, this paper presents a polynomial reduction from a 3-CNF formula to a regular （3,4）-CNF formula, in which each clause contains exactly three literals, and each variable appear exactly four times. Therefore, the regular （3,4）-SAT is a NP-complete problem, and MAX （3,4）-SAT is inapproximable.
出处
《计算机科学与探索》
CSCD
2013年第8期691-697,共7页
Journal of Frontiers of Computer Science and Technology
基金
国家自然科学基金No.61262006~~
