经典逻辑中的SAT问题是指布尔表达式的可满足性问题，它是计算机科学中的核心问题。SAT问题是NP完全问题，从理论上说，SAT问题不能在多项式时间内解决，它超出了现代计算机的能力。所以，SAT问题是计算机科学发展中的“瓶颈”问题，计算机科学家们一直都在寻求各种快速策略和方法试图改进SAT问题的求解。 极小不可满足公式的研究是近年来兴起的关于SAT问题的一个热点方向。个CNF公式（CNF公式是有限个子句的合取）F称为极小不可满足的（MU），如果F是不可满足，并且在F中删去任意一个子句后所得到的公式是可满足的。MU（k）表示子句数与变元数的差为k的极小不可满足公式的类。Kleine Buning．H等人的研究结果表明：如果k≤0，则公式不是极小不可满足的，也就是说，所有极小小可满足公式其子句数必定大于公式中的变量个数。 在本文中，我们将给出一个在多项式时间内判定可满足公式到MU（1）公式扩张问题的算法。关于公式扩张问题，Kleine Buning H和Zhao X S已经做出了若干结果，他们得出：Horn公式到MU（1）公式的扩张问题可在多项式时间内判定，问题MU-EXT[ext=t]为D^P-难，问题MU-EXT[ext=1]在P⁽NP[logn]之中，问题MU-EXT[ext=t，defi=k]可在多项式时间内判定，这里记MU-EXT[ext=t，defi=k]={F∈CNF|（?）G:F+G∈MU（k），var（G）（?）var（F），|G|=t}。在本论文中，我们考虑对一个给定可满足CNF公式F，是否存在公式G使得F+G∈MU（1）（var（G）（?）var（F））并给出这个问题的多项式时间判定算法。