微电子学与计算机
微電子學與計算機
미전자학여계산궤
MICROELECTRONICS & COMPUTER
2007年
11期
103-106,109
,共5页
尹文波%荆明娥%周电%周晓方
尹文波%荊明娥%週電%週曉方
윤문파%형명아%주전%주효방
可满足性问题%有界模型检验%子句规则%精简布尔电路
可滿足性問題%有界模型檢驗%子句規則%精簡佈爾電路
가만족성문제%유계모형검험%자구규칙%정간포이전로
为有界模型检验提出了改进的子句规则.在节点分类的基础上,首先对精简布尔电路表示进行逻辑化简,去掉功能冗余节点;然后识别、记录和处理多元运算的操作数,把多元运算作为单个节点直接生成子句;最后合并相邻节点,根据合并后的逻辑关系生成变量和子句.实验结果表明,改进的子句规则普遍减少了可满足性问题的变量、子句数目和运行时间.
為有界模型檢驗提齣瞭改進的子句規則.在節點分類的基礎上,首先對精簡佈爾電路錶示進行邏輯化簡,去掉功能冗餘節點;然後識彆、記錄和處理多元運算的操作數,把多元運算作為單箇節點直接生成子句;最後閤併相鄰節點,根據閤併後的邏輯關繫生成變量和子句.實驗結果錶明,改進的子句規則普遍減少瞭可滿足性問題的變量、子句數目和運行時間.
위유계모형검험제출료개진적자구규칙.재절점분류적기출상,수선대정간포이전로표시진행라집화간,거도공능용여절점;연후식별、기록화처리다원운산적조작수,파다원운산작위단개절점직접생성자구;최후합병상린절점,근거합병후적라집관계생성변량화자구.실험결과표명,개진적자구규칙보편감소료가만족성문제적변량、자구수목화운행시간.
