命题公式有效推理的特殊变元集及算法研究

一个CNF公式经过一个部分真值指派化简后，其可满足性判定可能变得易解；经过一对部分真值指派化简后，得到的两个公式可能同构(称为局部对称)。研究CNF公式的某些特殊变元集(后门集、关键文字集(或称脊))、以及局部对称如何影响可满足性的有效判定及相关算法，寻找给定CNF子类的特殊变元集、局部对称结构特征，使其可满足性的判定算法有本质改进。目的是如果有效地选择这样的变元集，使得基于这部分变元的部分真值指派，化简后的公式其可满足性的判定或同构判定变得容易，局部对称则应用于对DPLL算法的有效剪枝。将极小不可满足公式、变元极小不可满足公式、以及PCP理论应用于相关的研究中，通过对公式的后门集、关键文字集、以及局部对称结构的深入研究，建立命题公式的有效推理和DPLL算法的有效改进策略，就相关问题的算法及复杂性、特殊变元集规模的上下界、不可近似问题、嵌入问题(可嵌入性、最大嵌入)等作深入研究。