CAJ | 학술논문

SMT问题是在特定理论下判定一阶逻辑公式可满足性问题。它在很多领域，尤其是形式验证、程序分析、软件测试等领域，都有重要的应用。介绍了SMT问题的基本概念、相关定义以及目前的主流理论。近年来出现了很多提高SMT求解效率的技术，着重介绍并分析了这些技术，包括积极类算法、惰性算法及其优化技术等。介绍了目前的主流求解器和它们各自的特点，包括Z3、Yices、CVC3/CVC4等。对SMT求解技术的前景进行了展望，量词的处理、优化问题和解空间大小的计算等尤其值得关注。
SMT문제시재특정이론하판정일계라집공식가만족성문제。타재흔다영역，우기시형식험증、정서분석、연건측시등영역，도유중요적응용。개소료SMT문제적기본개념、상관정의이급목전적주류이론。근년래출현료흔다제고SMT구해효솔적기술，착중개소병분석료저사기술，포괄적겁류산법、타성산법급기우화기술등。개소료목전적주류구해기화타문각자적특점，포괄Z3、Yices、CVC3/CVC4등。대SMT구해기술적전경진행료전망，량사적처리、우화문제화해공간대소적계산등우기치득관주。
SMT is the problem of deciding the satisfiability of a first order formula with respect to some theory formulas. It is being recognized as increasingly important due to its applications in different communities, in particular in formal verification, program analysis and software testing. This paper provides a brief overview of SMT and its theories. Then this paper introduces some approaches aiming to improve the efficiency of SMT solving, including eager and lazy approaches and optimum technique which have been proposed in the last ten years. This paper also introduces some state-of-the-art SMT solvers, including Z3, Yices and CVC3/CVC4. Finally, this paper gives a preliminary prospect on the research trends of SMT, which include SMT with quantifier, optimization problems subject to SMT and volume computation for SMT.