基于悖论证明与局部搜索的不可满足子式求解算法

• 作者: 张建民 李思昆 沈胜宇
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 形式化验证 可满足问题 不可满足子式 悖论证明 局部搜索
• 年，卷（期）: 2014,（11）
• 页码范围: 2262-2267
• 页数: 6页
• 分类号: TP391
• 字数: 5023字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2014.02262

摘要

随着软硬件设计规模日益增加,功能越来越复杂,功能验证与调试在整个设计周期中占有的比重越来越大,迫切需要高效的方法诊断与定位设计中的错误,而求解不可满足子式可以显著提高自动化工具定位错误的效率.近年来,求解不可满足子式的算法多是基于DPLL(Davis-Putnam-Logemann-Loveland)回溯搜索过程的完全算法,很少有研究涉及到不完全方法.文中针对求解不可满足子式的不完全方法,提出了悖论证明与悖论解析树的概念,并提出一种启发式局部搜索算法,从布尔公式的悖论证明中求解不可满足子式.算法首先采用融合了布尔推理技术、动态剪枝方法及蕴含消除方法的局部搜索过程,逐步构建悖论证明所对应的悖论解析树;然后调用递归函数搜索悖论解析树,最终得到不可满足子式.基于实际测试集与随机测试集进行了实验对比,结果表明文中提出的算法优于同类算法,而且动态剪枝与蕴含消除技术能够有效地减少存储空间及运行时间.

作者信息

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