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

• 作者: 张建民 李思昆 沈胜宇
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 形式化验证 最小不可满足子式 极大可满足子式 贪心遗传算法 蚁群算法
• 年，卷（期）: 2009,（5）
• 所属期刊栏目: 学术论文
• 页码范围: 993-999
• 页数: 7页
• 分类号: TP391
• 字数: 7459字
• 语种: 中文
• DOI: 10.3321/j.issn:0372-2112.2009.05.016

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李思昆	国防科学技术大学计算机学院	133	1339	18.0	31.0
2	张建民	国防科学技术大学计算机学院	10	26	3.0	4.0
3	沈胜宇	国防科学技术大学计算机学院	8	30	3.0	5.0