基于一階邏輯的可滿足求解方法研究進展

摘要：基于命題邏輯的布爾可滿足SAT存在描述能力弱、抽象層次低、求解復雜度高等問題,而基于一階邏輯的可滿足性模理論SMT采用高層建模語言,表達能力更強,更接近于字級設計,避免將問題轉化到位級求解,在硬件RTL級驗證、程序驗證與實時系統驗證等領域得到了廣泛應用。針對近年來涌現的眾多SMT求解方法,依據方法的求解方式進行了分類與對比。而后,對3種主流的求解方法Eager方法、Lazy方法和DPLL(T)方法的實現進行了概要介紹。最后,討論了SMT求解方法當前所面臨的主要挑戰以及在SMT求解方面的一些研究成果,并對今后的研究進行了展望。