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

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

Research advances in the solving methods of satisfiability modulo theories based on first-order logic

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.