不可满足公式的结构以及证明方法的研究

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