计算机工程与科学
計算機工程與科學
계산궤공정여과학
COMPUTER ENGINEERING & SCIENCE
2009年
4期
56-59,105
,共5页
布尔可满足问题%不可满足子式%消解序列%局部搜索
佈爾可滿足問題%不可滿足子式%消解序列%跼部搜索
포이가만족문제%불가만족자식%소해서렬%국부수색
解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而不可满足子式能够为公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由.近年来涌现了许多基于SAT求解器DPLL回溯搜索过程的完全算法,但关于不完全方法提取不可满足子式的研究相对较少.因此,本文提出一种采用启发式局部搜索过程从公式的不可满足性证明中求解布尔不可满足子式的算法.该算法根据公式的消解规则通过局部搜索过程直接构造证明不可满足性的消解序列,并融合了布尔推理技术以提高搜索效率;而后通过一个递归过程遍历证明序列从而得到不可满足子式.通过实验与贪心遗传算法进行对比,结果表明本文提出的算法优于贪心遗传算法.
解釋佈爾公式不可滿足的原因在衆多領域都具有非常重要的理論與應用價值,而不可滿足子式能夠為公式不可滿足的原因提供精確的解釋,幫助應用領域的自動化工具迅速定位錯誤,診斷問題失敗的本質緣由.近年來湧現瞭許多基于SAT求解器DPLL迴溯搜索過程的完全算法,但關于不完全方法提取不可滿足子式的研究相對較少.因此,本文提齣一種採用啟髮式跼部搜索過程從公式的不可滿足性證明中求解佈爾不可滿足子式的算法.該算法根據公式的消解規則通過跼部搜索過程直接構造證明不可滿足性的消解序列,併融閤瞭佈爾推理技術以提高搜索效率;而後通過一箇遞歸過程遍歷證明序列從而得到不可滿足子式.通過實驗與貪心遺傳算法進行對比,結果錶明本文提齣的算法優于貪心遺傳算法.
해석포이공식불가만족적원인재음다영역도구유비상중요적이론여응용개치,이불가만족자식능구위공식불가만족적원인제공정학적해석,방조응용영역적자동화공구신속정위착오,진단문제실패적본질연유.근년래용현료허다기우SAT구해기DPLL회소수색과정적완전산법,단관우불완전방법제취불가만족자식적연구상대교소.인차,본문제출일충채용계발식국부수색과정종공식적불가만족성증명중구해포이불가만족자식적산법.해산법근거공식적소해규칙통과국부수색과정직접구조증명불가만족성적소해서렬,병융합료포이추리기술이제고수색효솔;이후통과일개체귀과정편력증명서렬종이득도불가만족자식.통과실험여탐심유전산법진행대비,결과표명본문제출적산법우우탐심유전산법.
