• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

计算机工程与科学

• 高性能计算 • 上一篇    下一篇

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

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

  1. (国防科技大学计算机学院,湖南 长沙 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   

  1. (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

摘要:

基于命题逻辑的布尔可满足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)