经典逻辑中的SAT问题是指布尔表达式的可满足性问题，它是计算机科学中的核心问题。SAT问题是NP完全问题，从理论上说，SAT问题不能在多项式时间内解决，它超出了现代计算机的能力。所以，SAT问题是计算机科学发展中的“瓶颈”问题，计算机科学家们一直都在寻求各种快速策略和方法试图改进SAT问题的求解。 　　一个CNF公式是有限个子句的合取，k-CNF是子句长度不超过k的公式类，k-SAT就是判定给定的k-CNF公式是否有可满足的解。众所周知，2-SAT问题是线性时间可解的，而k-SAT问题是NP完全的。近年来，寻找k-SAT的最优算法一直没有停止过。最新研究结果表明改进的关于k-SAT的指数时间算法的复杂度随k的递增而增加。在文献[IP99]中，R.Impagilazzo和R.Paturi定义了一个参数Sk=inf{δ|存在解决k-SAT的复杂度为o(2δn)的算法}，同时，还证明了在关于k-SAT有指数时间算法的假设下，{sk}是一个关于k的递增序列。于是，在文献[IP99]中，提出了一个公开问题：如何有效的将k-CNF类公式归约为t-CNF类公式(t＜k)。可以看出，解决上述问题对于k-SAT问题的研究有重要意义。 　　极小不可满足公式的研究是近年来兴起的关于SAT问题的一个热点方向。一个CNF公式F称为极小不可满足的(MU)，如果F是不可满足，并且在F中删去任意一个子句后所得到的公式是可满足的。MU(k)表示子句数与变元数的差为k的极小不可满足公式的类。极小不可满足公式的一些结构和性质将有助于研究CNF公式类之间的归约。 　　本文首先提出了一个从CNF公式归约为3-CNF类公式的新算法，与现有的经典算法相比，我们的新算法在归约过程中需引入的变元更少。然后，我们通过构造合适的极小不可满足公式，得到一个将k-CNF类公式归约为t-CNF类公式(t＜k)的有效算法。对于固定的k，t(3≤t＜k)，我们可以在关于公式F的长度的线性时间内将一个k-CNF类公式F归约为t-CNF类公式F。