| MAX^＋公式的结构特征 |
| |
| 引用本文： | 姚雷博,董红政,郭超,张伟民,段晓明.MAX^＋公式的结构特征[J].计算机与数字工程,2010,38(9):130-134. |
| |
| 作者姓名： | 姚雷博 董红政 郭超 张伟民 段晓明 |
| |
| 作者单位： | 洛阳理工学院,洛阳,471023 |
| |
| 摘 要： | 改名是一个将变元映射到变元本身或它的补的函数,变元改名是公式变元集合上的一个置换,文字改名是一个改名和一个变元改名的组合。改名技术在简化一些难例公式的消解证明和构造高效的可满足算法方面有重要意义。MAX^＋公式是MU公式中的一个重要子类,该类公式可以通过递归的方式产生。通过分析MAX^＋公式的结构,得到了一些关于此类公式的结构特点,对进一步研究这类公式的改名问题有较大意义。
|
| 关 键 词： | MAX^＋ 结构 特征 公式 |
Structure Characteristics of MAX+ Formulas |
| |
| Yao Leibo,Dong Hongzheng,Guo Chao,Zhang Weimin,Duan Xiaoming.Structure Characteristics of MAX+ Formulas[J].Computer and Digital Engineering,2010,38(9):130-134. |
| |
| Authors: | Yao Leibo Dong Hongzheng Guo Chao Zhang Weimin Duan Xiaoming |
| |
| Affiliation: | Yao Leibo Dong Hongzheng Guo Chao Zhang Weimin Duan Xiaoming (Luoyang Institute of Science and Technology, Luoyang 471023) |
| |
| Abstract: | A renaming is a function mapping propositional variable to itself or its complement, a variable renaming is a permutation over the set of propositional variables of a formula, and a literal renaming is a combination of a renaming and a variable renaming. The renamings has played a significant role in the construction of efficent satisfiability algorithms and simplifying resolution proofs of some hard formulas. A subclass MAX＋ formulas in minimal unsatisfiable formulas ean be constructed recursively. The tructure of the MAX＋ formulas is analyzed, and some valuable structure characteristics of the MAX＋ formulas are shown. |
| |
| Keywords: | MAX+ |
| 本文献已被 维普 万方数据 等数据库收录！ |
|
