摘要：解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值，而最小不可满足子公式能够为公式不可满足的原因提供精确的解释，帮助自动化工具迅速定位错误，诊断问题失败的缘由．针对最小不可满足子式的求解问题，提出并证明了布尔公式最小不可满足性与极大可满足性之间的关系．基于二者的关系，提出了求解最小布尔不可满足子式的贪心遗传算法与蚁群算法，并且通过实验与当前最好的方法分支一限界算法进行了对比，结果表明：两种算法在运算效率以及单位时间内剔除的短句数上都显著优于分支．限界算法，而贪心遗传算法优于蚁群算法．

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

单位：国防科学技术大学计算机学院; 湖南长沙410073