论文部分内容阅读
改名是一个将变元映射到变元本身或它的补的函数,变元改名是公式变元集合上的一个置换,文字改名是一个改名和一个变元改名的组合。改名技术在简化一些难例公式的消解证明和构造高效的可满足算法方面有重要意义。MAX^＋公式是MU公式中的一个重要子类,该类公式可以通过递归的方式产生。通过分析MAX^＋公式的结构,得到了一些关于此类公式的结构特点,对进一步研究这类公式的改名问题有较大意义。