中文摘要：

从研究如何在不可满足公式中计算极小不可满足公式出发，研究不可满足公式中所带最小公式差的极小不可满足公式的计算方法。利用公式差为1 的极小不可满足公式(MU(1)公式)的优良性质、以及极小不可满足公式的分裂技术，研究极小不可满足公式的结构、以及由MU(1)公式重新构造极小不可满足公式的计算方法。从而研究不可满足公式的结构。利用图论和矩阵方法研究极小不可满足公式的同构与同态判定问题的计算复杂性，寻找在多项式时间内可进行同构或同态判定的某些极小不可满足公式子类。利用某些公式类中公式间的同构判定结果，研究带有对称规则的DPLL算法，寻找某些在多项式时间内能够证明其不可满足性的不可满足公式类。研究某些难例公式的局部对称结构，并研究这些难例在带有对称规则的DPLL算法下的计算复杂性。

结论摘要：

本项目研究成果包括(1)系统地研究了极小不可满足（MU）公式类、以及相关的典型子类中公式的同构与同态判定问题的计算复杂性。结果表明MU公式的同构与同态判定问题的复杂性与图的同构和同态判定问题的难度相同，而某些子类的同构判定问题在多项式时间内可解。(2) 给出了不可满足公式的一个同态证明系统，将一个不可满公式的MU子公式分裂成若MU（1）公式，借助于MU（1）的特殊结构，以完成一个确定性消解证明。(3) 利用极小不可满足公式的特性，介绍了几种有用的公式归约方法，利用我们引入的方法，可以将CNF公式归约到一些特殊的公式类，并对具有某些特殊结构和限制的公式类进行了深入的研究。解决了一个k-CNF到t-CNF转换的公开问题；并一般性地解决线性公式不可满足公式存在性问题。(4) 引入了带有对称规则的DPLL算法，验证了某些消解难例在此算法下的多项式可解。此外，我们还对某些公式子类的结构和不满足性证明进行了研究。如变元出现次数受限的固定参数复杂性问题，基于关键文字的启发式满足性算法，部分指派简化公式到特殊子类问题，极小不可满足公式分裂到MU（1）的算法和复杂性等问题。