-
题名基于悖论证明与局部搜索的不可满足子式求解算法
被引量:4
- 1
-
-
作者
张建民
沈胜宇
李思昆
-
机构
国防科学技术大学计算机学院
-
出处
《计算机学报》
EI
CSCD
北大核心
2014年第11期2262-2267,共6页
-
基金
国家自然科学基金(61103083
61133007)
国家"八六三"高技术研究发展计划项目基金(2012AA01A301)资助~~
-
文摘
随着软硬件设计规模日益增加,功能越来越复杂,功能验证与调试在整个设计周期中占有的比重越来越大,迫切需要高效的方法诊断与定位设计中的错误,而求解不可满足子式可以显著提高自动化工具定位错误的效率.近年来,求解不可满足子式的算法多是基于DPLL(Davis-Putnam-Logemann-Loveland)回溯搜索过程的完全算法,很少有研究涉及到不完全方法.文中针对求解不可满足子式的不完全方法,提出了悖论证明与悖论解析树的概念,并提出一种启发式局部搜索算法,从布尔公式的悖论证明中求解不可满足子式.算法首先采用融合了布尔推理技术、动态剪枝方法及蕴含消除方法的局部搜索过程,逐步构建悖论证明所对应的悖论解析树;然后调用递归函数搜索悖论解析树,最终得到不可满足子式.基于实际测试集与随机测试集进行了实验对比,结果表明文中提出的算法优于同类算法,而且动态剪枝与蕴含消除技术能够有效地减少存储空间及运行时间.
-
关键词
形式化验证
可满足问题
不可满足子式
悖论证明
局部搜索
-
Keywords
formal verification
satisfiable problem
unsatisfiable subformula
refutation proof
local search
-
分类号
TP391
[自动化与计算机技术—计算机应用技术]
-