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

摘要

可满足合取范式(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) (∪)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 (n4) to solve such a question.