计算机与数字工程
計算機與數字工程
계산궤여수자공정
COMPUTER & DIGITAL ENGINEERING
2010年
9期
130-134
,共5页
姚雷博%董红政%郭超%张伟民%段晓明
姚雷博%董紅政%郭超%張偉民%段曉明
요뢰박%동홍정%곽초%장위민%단효명
MAX+%结构%特征%公式
MAX+%結構%特徵%公式
MAX+%결구%특정%공식
改名是一个将变元映射到变元本身或它的补的函数,变元改名是公式变元集合上的一个置换,文字改名是一个改名和一个变元改名的组合.改名技术在简化一些难例公式的消解证明和构造高效的可满足算法方面有重要意义.MAX+公式是MU公式中的一个重要子类,该类公式可以通过递归的方式产生.通过分析MAX+公式的结构,得到了一些关于此类公式的结构特点,对进一步研究这类公式的改名问题有较大意义.
改名是一箇將變元映射到變元本身或它的補的函數,變元改名是公式變元集閤上的一箇置換,文字改名是一箇改名和一箇變元改名的組閤.改名技術在簡化一些難例公式的消解證明和構造高效的可滿足算法方麵有重要意義.MAX+公式是MU公式中的一箇重要子類,該類公式可以通過遞歸的方式產生.通過分析MAX+公式的結構,得到瞭一些關于此類公式的結構特點,對進一步研究這類公式的改名問題有較大意義.
개명시일개장변원영사도변원본신혹타적보적함수,변원개명시공식변원집합상적일개치환,문자개명시일개개명화일개변원개명적조합.개명기술재간화일사난례공식적소해증명화구조고효적가만족산법방면유중요의의.MAX+공식시MU공식중적일개중요자류,해류공식가이통과체귀적방식산생.통과분석MAX+공식적결구,득도료일사관우차류공식적결구특점,대진일보연구저류공식적개명문제유교대의의.
