命题变元及其否定统称为文字，文字的析取称为子句，子句的合取称为合取范式(CNF公式)。如果存在一个赋值使得公式的值为1，则称该公式可满足；否则称该公式不可满足。判定一个公式是否是可满足的问题称为可满足性问题，简称为SAT问题。解决SAT问题的一个重要算法是DPLL算法。一个公式是极小不可满足的是指该公式本身不可满足，但是从中删去任意一个子句后得到的公式可满足。德国学者H．K．Büning，O．Kullmann等人在这方面做了许多重要的工作。极小不可满足公式的结构和性质将有助于判定SAT算法的研究。对于3-SAT来说，很多学者所做的大量实验表明，在m/n大约为4．26时(其中m是子句个数，n是变元个数)，可满足概率为0．5。一般认为，在这个比值下随机生成的3-SAT问题实例非常难解决，而在其它比值下生成的实例容易解决，这种容易-困难-容易的现象就是所谓的相变现象，它原本是物理学中的概念。基于相变现象，Monasson等人于1999年介绍了最大可满足公式的脊。在最大可满足赋值中均取真的文字构成的集合称为最大可满足公式的脊。Dubois等人于2001年根据可满足公式脊的概念，定义了寻找可满足公式的脊的启发式算法，但是没有进行理论研究。本文在启发式算法的基础上，一方面定义可满足公式的关键文字，研究关键文字的性质，给出DPLL算法的一种改进方法；另一方面，利用极小不可满足公式的特殊结构，定义极小不可满足公式的相对关键文字，研究相对关键文字与极小不可满足公式之间的关系，可以证明，仅使用关键文字规则和纯文字规则，就可以将MU(1)公式的任何最大可满足子公式在O(n~2)时间内化简为空集。