计算机学报
計算機學報
계산궤학보
CHINESE JOURNAL OF COMPUTERS
2014年
11期
2262-2267
,共6页
形式化验证%可满足问题%不可满足子式%悖论证明%局部搜索
形式化驗證%可滿足問題%不可滿足子式%悖論證明%跼部搜索
형식화험증%가만족문제%불가만족자식%패론증명%국부수색
formal verification%satisfiable problem%unsatisfiable subformula%refutation proof%local search
随着软硬件设计规模日益增加,功能越来越复杂,功能验证与调试在整个设计周期中占有的比重越来越大,迫切需要高效的方法诊断与定位设计中的错误,而求解不可满足子式可以显著提高自动化工具定位错误的效率.近年来,求解不可满足子式的算法多是基于DPLL(Davis-Putnam-Logemann-Loveland)回溯搜索过程的完全算法,很少有研究涉及到不完全方法.文中针对求解不可满足子式的不完全方法,提出了悖论证明与悖论解析树的概念,并提出一种启发式局部搜索算法,从布尔公式的悖论证明中求解不可满足子式.算法首先采用融合了布尔推理技术、动态剪枝方法及蕴含消除方法的局部搜索过程,逐步构建悖论证明所对应的悖论解析树;然后调用递归函数搜索悖论解析树,最终得到不可满足子式.基于实际测试集与随机测试集进行了实验对比,结果表明文中提出的算法优于同类算法,而且动态剪枝与蕴含消除技术能够有效地减少存储空间及运行时间.
隨著軟硬件設計規模日益增加,功能越來越複雜,功能驗證與調試在整箇設計週期中佔有的比重越來越大,迫切需要高效的方法診斷與定位設計中的錯誤,而求解不可滿足子式可以顯著提高自動化工具定位錯誤的效率.近年來,求解不可滿足子式的算法多是基于DPLL(Davis-Putnam-Logemann-Loveland)迴溯搜索過程的完全算法,很少有研究涉及到不完全方法.文中針對求解不可滿足子式的不完全方法,提齣瞭悖論證明與悖論解析樹的概唸,併提齣一種啟髮式跼部搜索算法,從佈爾公式的悖論證明中求解不可滿足子式.算法首先採用融閤瞭佈爾推理技術、動態剪枝方法及蘊含消除方法的跼部搜索過程,逐步構建悖論證明所對應的悖論解析樹;然後調用遞歸函數搜索悖論解析樹,最終得到不可滿足子式.基于實際測試集與隨機測試集進行瞭實驗對比,結果錶明文中提齣的算法優于同類算法,而且動態剪枝與蘊含消除技術能夠有效地減少存儲空間及運行時間.
수착연경건설계규모일익증가,공능월래월복잡,공능험증여조시재정개설계주기중점유적비중월래월대,박절수요고효적방법진단여정위설계중적착오,이구해불가만족자식가이현저제고자동화공구정위착오적효솔.근년래,구해불가만족자식적산법다시기우DPLL(Davis-Putnam-Logemann-Loveland)회소수색과정적완전산법,흔소유연구섭급도불완전방법.문중침대구해불가만족자식적불완전방법,제출료패론증명여패론해석수적개념,병제출일충계발식국부수색산법,종포이공식적패론증명중구해불가만족자식.산법수선채용융합료포이추리기술、동태전지방법급온함소제방법적국부수색과정,축보구건패론증명소대응적패론해석수;연후조용체귀함수수색패론해석수,최종득도불가만족자식.기우실제측시집여수궤측시집진행료실험대비,결과표명문중제출적산법우우동류산법,이차동태전지여온함소제기술능구유효지감소존저공간급운행시간.
