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

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