论文部分内容阅读
改名技术在简化一些难例公式的消解证明和构造高效的可满足算法方面有重要意义。MAX^＋公式是MU公式中的一个重要子类,该类公式可以通过递归的方式产生。为研究MAX^＋公式改名问题的复杂性,对MAX^＋（1）和MAX^＋（2）公式的分裂问题进行了分析,得到了一些关于这两类公式的若干分裂特征,对进一步研究MAX＋公式的改名问题有较大的现实意义。