计算机辅助设计与图形学学报
計算機輔助設計與圖形學學報
계산궤보조설계여도형학학보
JOURNAL OF COMPUTER-AIDED DESIGN & COMPUTER GRAPHICS
2008年
10期
1253-1260
,共8页
形式化验证%布尔公式%可满足问题%不可满足子式%DPLL算法
形式化驗證%佈爾公式%可滿足問題%不可滿足子式%DPLL算法
형식화험증%포이공식%가만족문제%불가만족자식%DPLL산법
解释布尔公式不可满足的原因在诸如形式化验证与电子设计自动化等众多领域中都具有非常重要的理论与应用价值.不可满足子式能够为布尔公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由.针对近年来出现的许多求解布尔不可满足子式的研究工作,根据算法的类型归类比较,对各种求解方法进行了概述评论,并简要介绍了在该领域所做的一些研究工作.最后讨论了布尔不可满足子式的求解方法目前面临的主要挑战,并对今后的研究方向进行了展望.
解釋佈爾公式不可滿足的原因在諸如形式化驗證與電子設計自動化等衆多領域中都具有非常重要的理論與應用價值.不可滿足子式能夠為佈爾公式不可滿足的原因提供精確的解釋,幫助應用領域的自動化工具迅速定位錯誤,診斷問題失敗的本質緣由.針對近年來齣現的許多求解佈爾不可滿足子式的研究工作,根據算法的類型歸類比較,對各種求解方法進行瞭概述評論,併簡要介紹瞭在該領域所做的一些研究工作.最後討論瞭佈爾不可滿足子式的求解方法目前麵臨的主要挑戰,併對今後的研究方嚮進行瞭展望.
해석포이공식불가만족적원인재제여형식화험증여전자설계자동화등음다영역중도구유비상중요적이론여응용개치.불가만족자식능구위포이공식불가만족적원인제공정학적해석,방조응용영역적자동화공구신속정위착오,진단문제실패적본질연유.침대근년래출현적허다구해포이불가만족자식적연구공작,근거산법적류형귀류비교,대각충구해방법진행료개술평론,병간요개소료재해영역소주적일사연구공작.최후토론료포이불가만족자식적구해방법목전면림적주요도전,병대금후적연구방향진행료전망.
