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

计算机工程与科学

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

张建民，黎铁军，马柯帆，肖立权

（国防科技大学计算机学院,湖南长沙 410073）

收稿日期:2019-07-01 修回日期:2019-09-16 出版日期:2019-12-25 发布日期:2019-12-25
基金资助:
国家重点研发计划(2016YFB0200203)；国家自然科学基金（61103083，61133007）

Research advances in the solving methods of

satisfiability modulo theories based on first-order logic

ZHANG Jian-min，LI Tie-jun，MA Ke-fan，XIAO Li-quan

（School of Computer,National University of Defense Technology,Changsha 410073,China）

Received:2019-07-01 Revised:2019-09-16 Online:2019-12-25 Published:2019-12-25

摘要/Abstract

摘要：

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

关键词: 形式化验证, 一阶逻辑, 布尔可满足, 可满足性模理论

Abstract:

Since Boolean Satisfiability (SAT) based on propositional logic has the problems of weak expression ability, low abstract level, and high solving complexity, Satisfiability Modulo Theories (SMT) based on first-order logic makes up for the shortcomings of SAT. SMT adopts word-level modeling language, more powerful expression ability, higher abstract level, and avoids translating the real instances to bit-level. SMT has been applied widely in numerous fields such as hardware RTL verification, software program verification, real-time system verification, and so on. The existing SMT solving algorithms emerged in recent years are categorized and compared according to their computing engines. The three typical SMT solving methods: Eager method, Lazy method and DPLL(T) method are described and analyzed. Finally, we discuss the current challenges and our research results on SMT, and then outline the future research directions.

Key words: formal verification, first-order logic, Boolean Satisfiability (SAT), Satisfiability Modulo Theories (SMT)

张建民，黎铁军，马柯帆，肖立权. 基于一阶逻辑的可满足求解方法研究进展[J]. 计算机工程与科学.

ZHANG Jian-min，LI Tie-jun，MA Ke-fan，XIAO Li-quan.

Research advances in the solving methods of

satisfiability modulo theories based on first-order logic

[J]. Computer Engineering & Science.

[1]	唐傲, 王晓峰, 何飞. 可满足性模理论综述[J]. 计算机工程与科学, 2024, 46(03): 400-415.
[2]	马雪, 何星星, 兰咏琪, 李莹芳. 一阶逻辑中基于treelet图神经网络的前提选择[J]. 计算机工程与科学, 2024, 46(02): 374-380.
[3]	林玲瑜, 曹锋, 易见兵, 方旺盛, 李俊, 吴贯锋. 基于子句活跃度和复杂度的多元动态演绎算法及应用[J]. 计算机工程与科学, 2023, 45(12): 2256-2264.
[4]	刘永梅, 王国辉, 关永, 张景芝, 施智平, 董璐. 格林定理的形式化及其初步应用[J]. 计算机工程与科学, 2023, 45(07): 1178-1187.
[5]	黎铁军, 马柯帆, 张建民. 基于不完全算法的并行FPGA SAT求解器[J]. 计算机工程与科学, 2021, 43(12): 2126-2130.
[6]	郑小宇, 刘冬梅, 杜益宁, 周子健, 邱玫媚, 朱鸿. 模式驱动的系统安全性设计的验证[J]. 计算机工程与科学, 2020, 42(07): 1197-1207.
[7]	胡军,张维珺,李宛倩. 面向需求的安全关键系统形式化建模与验证方法研究[J]. 计算机工程与科学, 2019, 41(08): 1426-1433.
[8]	何安平，吴尽昭，梁艺，熊玲芳，吴昊. 基于几何规划的布尔可满足问题求解方法[J]. J4, 2013, 35(9): 122-126.
[9]	徐亮，刘宏. 基于SMT的TECTL性质的限界模型检测方法[J]. J4, 2013, 35(10): 166-171.
[10]	任洪敏，刘晋. 基于行为协议的构件替换性分析[J]. J4, 2012, 34(12): 74-80.
[11]	单黎君, 朱鸿. UML的形式化描述语义[J]. J4, 2010, 32(3): 96-103.
[12]	张建民, 沈胜宇, 李思昆. 可满足性求解技术研究[J]. J4, 2010, 32(1): 50-54.
[13]	王俐莉王元元张兴元. 命题演算形式系统在Isabelle／HOL中的形式化[J]. J4, 2008, 30(10): 67-68.
[14]	周倜李梦君刘万伟李舟军. 安全协议的进程代数规约到逻辑程序的自动转换[J]. J4, 2006, 28(1): 22-24.
[15]	吴丹刘芳等. Linux中SystemV进程通信机制安全性形式化验证[J]. J4, 2002, 24(2): 13-17.