SMT求解器理论组合技术研究

J4 ›› 2011, Vol. 33 ›› Issue (10): 111-119.

SMT求解器理论组合技术研究

李〓婧，刘万伟

LI Jing，LIU Wanwei（并行与分布处理国防科技重点实验室，湖南长沙 410073）

收稿日期:2010-09-13 修回日期:2010-12-25 出版日期:2011-10-25 发布日期:2011-10-25

A Survey on Theoretical Combination Techniques of SMT Solvers

LI Jing，LIU Wanwei

（National Laboratory for Parallel and Distributed Processing，Changsha 410073,China）

Received:2010-09-13 Revised:2010-12-25 Online:2011-10-25 Published:2011-10-25

摘要/Abstract

摘要：

可满足模理论(SMT)求解器是计算机科学中用来判定一阶逻辑公式可满足性的程序，是许多形式化方法的验证引擎。理论求解器实现了SMT基于不同理论背景的求解过程，然而实际问题常以多个理论为背景。因此，本文重点介绍理论组合判定方法，概述SMT求解器的发展现状，并分析了几个主流SMT求解器理论组合判定关键技术。通过对照实验，评估各组合判定方法的优缺点以及目前流行的支持理论组合SMT求解器在工业应用中的性能。

关键词: 可满足模理论, SMT求解器, 组合理论

Abstract:

Satisfiability modulo theories solver is a decision procedure for the satisfiabilily of formulas of the firstorder logics. It is the verification engine for many formalization methods. Theory solvers solve problems with different theoretical backgrounds; however, the problems in the realworld applications often are supported by multiple theories. This paper mainly introduces the methods of theory combination, summarizes the status quo of the SMT solvers. Besides，it analyzes several major techniques on the theoretical combination for SMT solvers. Testing with the industrial cases, we finally evaluate methods of combination theory with experimental results, and compare the performances of several popular SMT solvers which support theoretical combination techniques.

Key words: satisfiability modulo theories;SMT solver;combination theory

李〓婧，刘万伟. SMT求解器理论组合技术研究[J]. J4, 2011, 33(10): 111-119.

LI Jing，LIU Wanwei. A Survey on Theoretical Combination Techniques of SMT Solvers[J]. J4, 2011, 33(10): 111-119.