一种求解布尔不可满足子式的局部搜索算法

• 作者: 张建民 李思昆 沈胜宇
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 布尔可满足问题 不可满足子式 消解序列 局部搜索
• 年，卷（期）: 2009,（4）
• 所属期刊栏目: 算法研究
• 页码范围: 56-59,105
• 页数: 5页
• 分类号: TP391
• 字数: 6192字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2009.04.017

摘要

解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而不可满足子式能够为公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由.近年来涌现了许多基于SAT求解器DPLL回溯搜索过程的完全算法,但关于不完全方法提取不可满足子式的研究相对较少.因此,本文提出一种采用启发式局部搜索过程从公式的不可满足性证明中求解布尔不可满足子式的算法.该算法根据公式的消解规则通过局部搜索过程直接构造证明不可满足性的消解序列,并融合了布尔推理技术以提高搜索效率;而后通过一个递归过程遍历证明序列从而得到不可满足子式.通过实验与贪心遗传算法进行对比,结果表明本文提出的算法优于贪心遗传算法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李思昆	国防科技大学计算机学院	100	974	16.0	27.0
2	张建民	国防科技大学计算机学院	11	15	2.0	3.0
3	沈胜宇	国防科技大学计算机学院	4	15	2.0	3.0