最小布尔不可满足子式的求解算法  

Algorithms for Deriving Minimum Unsatisfiable Boolean Subformulae

作　　者：张建民[1] 沈胜宇[1] 李思昆[1] 

机构地区：[1]国防科学技术大学计算机学院,湖南长沙410073

出　　处：《电子学报》2009年第5期993-999,共7页Acta Electronica Sinica

基　　金：国家自然科学基金(No.60603088)

摘　　要：解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而最小不可满足子公式能够为公式不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误,诊断问题失败的缘由.针对最小不可满足子式的求解问题,提出并证明了布尔公式最小不可满足性与极大可满足性之间的关系.基于二者的关系,提出了求解最小布尔不可满足子式的贪心遗传算法与蚁群算法,并且通过实验与当前最好的方法分支-限界算法进行了对比,结果表明:两种算法在运算效率以及单位时间内剔除的短句数上都显著优于分支-限界算法,而贪心遗传算法优于蚁群算法.Explaining the causes of infeasibility of Boolean formulae has practical applications in various fields.A smallestcardinality umatisfiable subformula can provide a succinct explanation of infeasibility, and help automatic tools to rapidly locate the en-ors, and determine the underlying reasom for the failure. We present the relationship between maximal satisfiability and minimum unsatisfiability. Based on the relatiomhip, a compounded greedy genetic algorithm and an ant colony algorithm are proposed to derive a minimum unsatisfiable subformula. We report experimental results on practical benchmarks, as compared with the best known branch-and-bound algorithm. The results show that two algorithms strongly outperform the branch-and-bound algorithm, and the compounded greedy genetic algorithm outperforms the ant colony algorithm on both efficiency and size of unsatisfiable subfonnulae.

关 键 词：形式化验证 最小不可满足子式 极大可满足子式 贪心遗传算法 蚁群算法 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]