计算机工程与科学
計算機工程與科學
계산궤공정여과학
COMPUTER ENGINEERING & SCIENCE
2010年
9期
139-141,168
,共4页
王倩%陈彩%吕关锋%苏开乐
王倩%陳綵%呂關鋒%囌開樂
왕천%진채%려관봉%소개악
BDD%一致性理论%可满足赋值算子
BDD%一緻性理論%可滿足賦值算子
BDD%일치성이론%가만족부치산자
在很多应用领域中,我们都需要获取逻辑公式所有无冗余的可满足解集合,即集合中的任意两个解不能互相蕴涵.为了获取无冗余解集合,本文提出了两种实现方案.由于二叉决策图BDD具有对逻辑公式的高效表达特性,因此两种方案都是在逻辑公式转换成BDD的基础上实现的[1].一种方案是直接对该BDD进行遍历,获取从根节点到终端节点1的所有路径集合,然后借助一致性理论获取无冗余解的一致性算子的实现.另一种方案借助香农分解定理对BDD先进行逐层分解,然后对分解后的BDD再进行一致性运算的可满足赋值算子的实现.本文最后对两种方案的实验效果进行对比分析.
在很多應用領域中,我們都需要穫取邏輯公式所有無冗餘的可滿足解集閤,即集閤中的任意兩箇解不能互相蘊涵.為瞭穫取無冗餘解集閤,本文提齣瞭兩種實現方案.由于二扠決策圖BDD具有對邏輯公式的高效錶達特性,因此兩種方案都是在邏輯公式轉換成BDD的基礎上實現的[1].一種方案是直接對該BDD進行遍歷,穫取從根節點到終耑節點1的所有路徑集閤,然後藉助一緻性理論穫取無冗餘解的一緻性算子的實現.另一種方案藉助香農分解定理對BDD先進行逐層分解,然後對分解後的BDD再進行一緻性運算的可滿足賦值算子的實現.本文最後對兩種方案的實驗效果進行對比分析.
재흔다응용영역중,아문도수요획취라집공식소유무용여적가만족해집합,즉집합중적임의량개해불능호상온함.위료획취무용여해집합,본문제출료량충실현방안.유우이차결책도BDD구유대라집공식적고효표체특성,인차량충방안도시재라집공식전환성BDD적기출상실현적[1].일충방안시직접대해BDD진행편력,획취종근절점도종단절점1적소유로경집합,연후차조일치성이론획취무용여해적일치성산자적실현.령일충방안차조향농분해정리대BDD선진행축층분해,연후대분해후적BDD재진행일치성운산적가만족부치산자적실현.본문최후대량충방안적실험효과진행대비분석.
