可满足公式到极小不可满足公式MU(1)的扩张复杂性(英文)

The Complexity of Extending a Formula to a MU(1) formula

可满足合取范式(CNF)公式F到极小不可满足公式MU(1)的扩张是,对给定的CNF公式F,是否存在一个公式G满足条件var(G)var(F)并使得F+G∈MU(1)。Horn公式到MU(1)公式的扩张问题可在多项式时间内解决,但对一般CNF公式F的扩张问题,至今尚未解决。这里我们将给出一个多项式时间的算法解决这一问题。

The extension problem is the question that for a satisfiable CNF formula F whether there exist a formula G such that F ＋ G ∈ MU（ 1 ） with var（G） lohtain in var（F）. It is known that the problem of extending a Horn formula into a MU（ 1 ） formula is solvable in polynomial time. But for a general satisfiable CNF formula F, the extension problem is still open. In this paper we will present a algorithm which the complexity is polynomial time of O （n^4） to solve such a question.