基于一阶逻辑的可满足求解方法研究进展

• 作者: 张建民 肖立权 马柯帆 黎铁军
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 形式化验证 一阶逻辑 布尔可满足 可满足性模理论
• 年，卷（期）: 2019,（12）
• 所属期刊栏目: 高性能计算
• 页码范围: 2119-2126
• 页数: 8页
• 分类号: TP391
• 字数: 8023字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2019.12.004

摘要

基于命题逻辑的布尔可满足SAT存在描述能力弱、抽象层次低、求解复杂度高等问题,而基于一阶逻辑的可满足性模理论SMT采用高层建模语言,表达能力更强,更接近于字级设计,避免将问题转化到位级求解,在硬件RTL级验证、程序验证与实时系统验证等领域得到了广泛应用.针对近年来涌现的众多SMT求解方法,依据方法的求解方式进行了分类与对比.而后,对3种主流的求解方法Eager方法、Lazy方法和DPLL(T)方法的实现进行了概要介绍.最后,讨论了SMT求解方法当前所面临的主要挑战以及在SMT求解方面的一些研究成果,并对今后的研究进行了展望.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	肖立权	国防科技大学计算机学院	17	79	4.0	8.0
2	张建民	国防科技大学计算机学院	11	15	2.0	3.0
3	黎铁军	国防科技大学计算机学院	13	39	4.0	6.0
4	马柯帆	国防科技大学计算机学院	3	0	0.0	0.0