SMT求解器技术对比分析及其能力扩展研究.pdf

《SMT求解器技术对比分析及其能力扩展研究.pdf》由会员分享，可在线阅读，更多相关《SMT求解器技术对比分析及其能力扩展研究.pdf（64页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、国防科学技术大学硕士学位论文SMT求解器技术对比分析及其能力扩展研究姓名：李婧申请学位级别：硕士专业：计算机科学与技术指导教师：王戟2010-11国防科学技术大学研究生院硕士学位论文 第 i 页 摘 要 形式化方法是一种有效的计算机软、硬件系统可信性验证手段。其主要技术包括模型检验，定理证明，等价性检验以及语言包含等。许多形式化验证问题最终都归结于布尔可满足问题(SAT)，它用来判断命题逻辑公式是否为可满足的。SAT 是第一个被证明的 NP 完全问题。与 SAT 相比，SMT 问题具有表达能力更强、抽象层次更高的优点，因而，迅速成为了形式化验证中的重要问题。而本文重点关注两个问题：目前 SMT

2、 求解器能力以及如何扩展 SMT 求解器能力。SMT 问题属于一阶逻辑范畴，SMT 求解器可判定的理论域包括：等式与未解释函数、线性算术、位向量以及量化公式等。而多种理论组合是适应当今工业应用日益复杂、多元化需求的，因此对该领域的判定技术的研究具有重大实际意义。本文对比分析了该技术的主要方法：Nelson-Oppen 方法，Delayed Theory Combination 方法，Ackerman 方法。另外，分析了主流求解器的关于该技术采用的最新策略。本文面向工业应用构建测评框架，对比评测 5 个当前主流并可用的支持理论组合判定技术的 SMT 求解器。从实验结果中看出 Z3 所采用的基于模

3、型的DTC 方法使其整体性能最佳，并且在各应用领域中 Z3 求解能力最强，特别是量化问题领域。并非所有的理论域 SMT 求解器对其都具有完全判定方法，仍存在无法判定的SMT 问题，特别是在量化领域。文中给出一类目前 SMT 求解器无法判定的量化SMT 公式一般形式，并由此构造一个自动机的符号化表示，文中证明了该过程转换的正确性。最终结合 SMT 公式解析模块和自动机语言判空技术，实现了一个完整的量化 SMT 公式判定过程。通过例子测试说明该方法的可行性并扩充了 SMT求解器能力，是兼具理论价值和实际意义的。关键词：SMT，理论组合技术，量化 SMT 公式，自动机符号化表示，-自动机判空问题 国

4、防科学技术大学研究生院硕士学位论文 第 ii 页 ABSTRACT Formal method has been proven to be an effective technique in verifying the trustness of software and hardware systems,and it includes several applicable methods such as model checking,theory proving,equivalence checking as well as language containment.Many of these

5、 formal methods can be translated to Boolean/Propositional Satisfiability Problems(SAT),which is used to decide whether a formula according to propositional logic is satisfied.SAT is well-known as the first proved NP-Complete problem.Compared with SAT,Satisfiable Module Theories(SMT)problems are mor

6、e expressive and abstractive,thus SMT becomes critical problems in verification field.This thesis mainly focuses on two things,one is to make sure of the state-of-the-art abilities of SMT solvers,and the other is to find a way to enlarge and complement the capabilities of SMT solvers.SMT problem bel

7、ongs to first-order logic and its decidable theories ranges over fields as equalities and uninterpreted functions,linear arithmetic,bitvectors as well as quantified problems.However,combination of mutiple theories is considered to be with great applicable values due to the demands of the presently c

8、omplex and multi-era industrial applications.This article comparatively analyzes three of theory combination techniques:Nelson-Oppen,Delayed Theory Combination and Ackermann methods.Besides,we present the newest techniques for SMT solvers in dealing with thoery combination,and then a capabilities en

9、valuation platform totally oriented to real-world applications for SMT solvers is given,we comparatively testing the latest and usable verisions of five SMT solvers.Through the results,we can find out that Z3 beats others for the whole performance with the refined DTC approach based on model,especia

10、lly in dealing with quatified formulas.Not all the theory domains SMT solvers have got a complete decidable method;there are still some unsolvable SMT problems,especially the quantified problems.This article shows a generalized formula pattern which SMT slovers can not solve at present.A new method

11、for solving this formula pattern is proposed,we construct a symbolic form of automata,and the correctness of this translating process has been proved in this article.Finally,we realize a complete decision procedure for quantified SMT formula,which combines our translating program with the input pars

12、er module and language decision technique of automata.Results prove our new method is feasiblible;besides,it strengthens the capability of SMT solvers and makes contributions both to theoreticle meanings and applicatible values.Key Words：SMT,Theory Combination,Quantified SMT Formula,Symbolic Express

13、ion of Automata,Emptyness Problem of-Automata国防科学技术大学研究生院硕士学位论文 第 III 页 表 目 录 表 1.1 SMT 求解器总表.6 表 2.2 -(字)自动机接收条件(不含 Finite)的布尔编码.16表 3.1 SMT-COMP08 各求解器理论组合判定执行结果.25表 3.2 SMT-COMP09 各求解器理论组合判定执行结果.25表 3.3 SMT 求解器理论组合判定方法.26表 3.4 按理论组合分类的实验结果统计表.27表 3.5 按工业应用分类的实验结果统计表.29表 4.1 运算符号表.33 国防科学技术大学研究生院硕

14、士学位论文 第 IV 页 图 目 录 图 1.1 验证方法与验证引擎.2图 1.2 基于 DPLL 算法的 SAT 求解器.3图 2.1 自动机的一次运行示例.15图 2.2 各类自动机表达能力之间的关系.17图 3.1 NO 方法传递接口等式.20图 3.2 改进 NO 方法传递接口等式实现非凸理论判定.21图 3.3 NO 方法框架图(左)、DTC 方法框架图(右).22图 4.1 迁移系统的符号化表示示意图.35图 4.2 为例 1 构造的自动机 M1(F)及其符号化表示.37图 5.1 实验基本框架图.42图 5.2 例 1smtlib 格式源文件：testcase1.smt.44图

15、5.3 CVC3 对 testcase1.smt 的解析和判定结果.44图 5.4 testcase1.smv 文件.45图 5.5 NuSMV 对 testcase1.smt 的判定结果.46图 5.6 NuSMV 为 testcase1.smt 的判定结果生成解释模型.46图 5.7 例 2smtlib 格式源文件：testcase2.smt.47图 5.8 CVC3 对 testcase2.smt 的解析和判定结果.47图 5.9 testcase2.smv 文件.48图 5.10 NuSMV 对 testcase2.smt 的判定结果.48图 5.11 NuSMV 为 testcase

16、2.smt 的判定结果生成解释模型.49 国防科学技术大学研究生院硕士学位论文 第 1 页 第一章 绪论 1.1 课题研究背景课题研究背景 1.1.1 形式化验证方法形式化验证方法 随着科技的快速发展和计算机技术的不断进步，人类社会的信息化和多元化程度越来越高。从飞机、汽车、阀门等工业制造到智能控制的家用电器，计算机软、硬件已经融入到人类生活的方方面面，那么，如何保证这些软、硬件设计的正确性？这对涉足该领域的人们提出了重大的挑战。为了满足用户的需求，软、硬件的设计日趋复杂，这种增长的复杂性常常伴随着设计中的错误也相应增多。如 2001 年 Bentley 在设计自动化年会上报告了 Pentiu

17、m 4 的设计中检测出“bug”的数目比 Pentium Pro 增长了 350%1。在芯片设计中，任何细微的错误都可能导致极严重的后果，如 1994 年 Pentium处理器浮点除法部件设计的一个错误致使英特尔公司的损失高达 4.75 亿美元，2005 年，日本汽车制造公司 Toyota 由于一个引擎控制器中的软件错误，召回 16 万余辆汽车2。为了极大的避免如此严重的损失，研究人员必须确保计算机系统的可靠性，安全性等性质在内的高可信性质。人们在 20 世纪 90 年代提出了形式化方法，它被认为是一种极具发展前景的验证方法。保证可靠、安全性是贯穿整个软硬件设计与实现的重要任务。面向可靠安全性

18、质的形式化验证方法是一种重要且十分有效的手段，并得到了长期和广泛的研究和应用。形式化验证方法一般分为两类：动态方法指运行待检验的程序，并根据程序的运行情况来判断所验证的性质是否被满足，例如测试方法；而静态方法则指的是通过对程序源代码进行静态的分析来验证其是否满足某性质。两种方法各具优缺点：动态方法往往不能确保对程序进行完全的分析与验证，如测试的输入常是部分的输入可能，从而使得验证是不完备的；而静态方法花费的时间和空间代价往往比动态方法大很多，但却是一个完全验证方法即考虑了所有可能的输入用例，并且不需要产生测试的激励，是一种具有数学完备性和逻辑推理严格特性的方法，通过符号化手段描述系统的属性，并

19、支持系统属性的推理以及系统描述的正确性验证。无论在计算机软件或是硬件系统中，形式化静态方法都更具有研究意义和应用价值，已成为当前的研究热点。本文是在静态方法的环境中讨论形式化验证技术及其验证工具。形式化验证方法的一般思路是用形式的方法验证设计的实现(Implementation,Imp)是否满足某种规范(Specification,Spec)，常包括以下几类技术3：1）模型检验模型检验：将规范表示成逻辑公式，而把系统实现抽象为语义模型，规范国防科学技术大学研究生院硕士学位论文 第 2 页 是否被满足通过这些语义模型来确立。2）定理证明定理证明：将实现满足规范的关系视为逻辑描述的定理，而规范提供

20、了证明规程要利用的公理以及假设，其验证过程是证明演算的过程。3）等价性检验等价性检验：将实现和规范抽象成逻辑公式，以及自动机的形式，用来确立实现与规范之间的等价性关系。4）语言包含语言包含：将实现和规范抽象成语言，检验前者的语言是否包含在后者的语言之后。随着形式化验证方法不断成熟，还出现了谓词抽象，静态检验等技术。无论采用何种方法，形式验证的终极目标是确立实现(Imp)和(Spec)之间满足以下几种关系之一3：1)实现与规范等价：Imp Spec；2)实现蕴含规范：ImpSpec；3)实现抽象成状态转移模型，如有限自动机，Kripke 结构等。规范描述为时态逻辑，如计算树逻辑，线性时序逻辑等。

21、该模型上所有可能的行为满足该规范的要求：Imp Spec。1.1.2 验证工具验证工具 然而，随着研究的不断深入，研究者发现许多形式化方法中都包含可满足问题(Boolean/Propositional Satisfiability,SAT)，即给定一个布尔函数，是否存在某种变量赋值使得函数的值为真，或者给出证明，该函数在任何赋值下都为假。即问题是可满足的(Satisfiable)，或是不可满足的(Unsatisfiable)。可满足性问题在数理逻辑、人工智能、机器学习、约束满足问题、VLSI 集成电路设计与检测以及计算机科学理论等等领域具有广阔的应用背景。目前，可满足性问题算法是形式验证的核心

22、引擎。图 1.1 验证方法与验证引擎 为了实现形式验证的最终目标，形式化方法将验证过程交由验证引擎实现。这些工具就是用来判定实现与规范是否满足某种关系的程序。各类形式化方法都有国防科学技术大学研究生院硕士学位论文 第 3 页 专门的验证工具，如定理证明工具 Simplify4，模型检验工具 SPIN5等。伴随着许多形式化验证方法都可归结到可满足性问题，其求解工具也已经逐渐支撑起诸如模型检验，定理证明等多种形式化验证方法中，逐渐成为了一种支持多种形式化验证方法的验证工具。1.1.2.1 SAT 求解器 可满足性问题在上世纪 60 年代开始引起广泛关注6，许多重要的基本问题都可以(在多项式时间内)

23、规约到 SAT 问题。它是第一个 NP 完备问题，并且是一大类 NP 完备问题的核心。大量的实践表明，许多 NP 完备问题无论是对于计算机科学理论还是工程应用都有着至关重要的意义。可满足问题求解器可满足问题求解器(SAT 求解器求解器)是用来判定 SAT 问题的程序，是一个高效的验证工具。它的输入一般采用合取范式(CNF)的方式，合取范式是对一些子句进行“与”操作，子句是对一些字进行“并”操作，而字则是布尔变量的否定或肯定的形式。采取合取范式的表达方式简洁且有效，同时表达布尔函数的其他方式都能通过引入一些辅助变量的途径在多项式时间内转为合取范式。对于一个布尔函数，其合取范式来表达方法不唯一，即

24、它并非正则表达方式。这种表达方式的好处在于它不像如模型检验求解技术中二叉决策图的方法一样，带有节点数目随布尔变量数目成指数倍增长的特点。图 1.2 基于 DPLL 算法的 SAT 求解器 作为 NP 问题的原型，可满足问题引起广泛关注。早在上世纪 60 年代，Davis，Putnam，Longemann，Loveland 等人就对解决该类问题进行研究，形成求解可满足问题的最常用的基本算法，称为 DPLL 算法6，也是 SAT 求解器算法的基础。随着 SAT 问题在验证领域广泛应用，SAT 求解器迅速推广，研究者在体验到求解算法的高效求解能力的同时也发现其不足，随之而来的是对 SAT 求解算法的

25、不断改进，继而推动了 SAT 技术向前发展。近年来，基于 DPLL 算法已有人提出了各种改进局部搜索算法和回溯算法，使 SAT 求解器解决问题的能力不断加强，同时规模也不断增大。其中局部搜索算法对随机的 SAT 问题特别适用，而回溯算法则对国防科学技术大学研究生院硕士学位论文 第 4 页 大规模工业应用中的 SAT 问题十分有效。SATO7，zChaff8，Berkmin9，Minisat10等求解器的主要算法就是基于 DPLL 算法改进的。随着布尔可满足求解技术的进步，SAT 求解器也日渐成熟与完善，目前已能够解决工业应用中的包含数万短句和数百万变元的问题。SAT 问题的种种应用包括规划调度

26、问题，寻找蛋白质的折叠态，以及计算机芯片的验证等11。1.1.2.2 SMT 求解器 SAT 求解器的判定对象是属于命题逻辑范畴，而命题逻辑的表达能力相对较弱，无法直接表达许多特定应用领域的问题。比如在 RTL 电路中，由于 SAT 求解器抽象层次较低，用位级信息描述问题将丢失大量的逻辑信息，同时会增加问题的规模和复杂性，从而导致结果不准确，以及求解的空间与时间开销也极高。一阶逻辑在命题逻辑基础上补充量词和项，与之对应的可满足性判断问题称为 SMT 问题(Satisfiability Modulo Theories，SMT)。一阶逻辑扩充了命题逻辑的表达能力，SMT 求解技术的出现扩充了 SA

27、T 技术的表达能力和应用范围，因而 SMT求解器得到更广泛的应用，并基于 SAT 技术趋于成熟而迅速崛起，并逐渐成为下一代验证引擎。SMT 处理的对象是一阶逻辑表达的公式，公式中的函数变元与谓词变元通常来源于一些特定的背景理论，从而弥补了 SAT 表达能力较弱的缺陷。SMT 典型的理论包括固定规模的位向量、数组、未解释函数、线性算术运算、差分逻辑等，甚至可以允许包含量词、非线性算术、复杂数据结构(元组，包等)的情形，以及这些不同知识领域的组合。对于位向量，未解释函数，差分逻辑等理论的一阶逻辑公式，SMT 技术已有完全判定的方法，但随着应用需求的不断发展，大多数应用都涉及多领域知识的结合，因此，

28、需要一种理论间组合技术以保证理论组合后的可满足性，这一项技术极大的推动 SMT 求解技术进步。然而，SMT 求解技术存在着局限性，对于带量词的或非线性算术领域的一阶逻辑公式，目前 SMT 求解技术对此无完全判定方法，研究者正在这些领域不断探求新的方法来扩充 SMT 求解技术。用以求解 SMT 问题的自动化工具称为 SMT 求解器求解器。SMT 求解技术在有界模型检验，基于符号执行的程序分析，线性规划和调度，测试用例生成，以及电路设计和验证等领域有非常广泛的应用。比如在程序静态分析中，从源程序提取出控制流图后，分析路径条件需要对其进行约束求解，此时将使用到 SMT 求解器；在有界模型检验(BMC

29、)中，将系统模型和待验证的属性转换为一阶逻辑公式，此时 SMT 求解器用来判定此公式是否可满足，从而验证该属性是否是可满足的。正是因为 SMT 求解器在不同的形式验证领域都发挥着重大的作用，各大科研机构积极研发 SMT 求解器，并且许多工具都已被成功应用于验证与分析领域。目国防科学技术大学研究生院硕士学位论文 第 5 页 前流行的 SMT 求解器有:Barcelogic12，Beaver13，Boolector14，CVC315，ALT-Ergo16，Mathsat417，OpenSMT18，Sword19，VeriT20，Yices21，Z322，STP23，以及 Spear24等。许多 S

30、MT 求解器提供了调用接口和使用手册，为学术研究提供免费服务。部分求解器是开源的，如 Beaver,OpenSMT，VeriT 和 CVC3等，这类工具旨在为科研和工业应用提供免费开源、自动化的工具。随着 SMT 求解技术飞速发展，SMT 求解器已经能够解决实际领域中许多问题。在有界模型检验(BMC)中，SAL 有界模型检测器采用 Yices 作为后端求解器，Boolector，MathSAT，CVC3 等求解器也常用于 BMC；在程序分析与验证领域中，用 SMT 求解器灵活的分析验证条件，证明程序的正确性，查找错误路径，程序分析框架 Klee23调用 STP 作为约束求解器，另外，Z3 已成

31、功应用于Spec#/Boogie 中，Calysto25采用 Spear 用于求解路径条件等；SMT 求解器亦可用于交互的定理证明，如 Z3，Yices，ALT-Ergo，Spear，CVC3 等，其中，Z3 将取代专门的定理证明器 Simplify 作为默认验证推理引擎；另外，SMT 求解器也可以应用于线性规划以及调度等问题，如 Barcelogic，HySAT 等。为了比较这些工具，可满足性理论及其应用国际学术年会(SAT)举办SMT-COMP26竞赛。从 2005 年到 2010 年已经成功举办了 6 届比赛。其测试用例集来源于 SMT-LIB(Satisfiability Modulo

32、 Theories Library)27，SMT-LIB 旨在形成一个格式统一的且基于不同背景理论知识的公式集，为评价和比较求解器的求解能力提供测试用例。SMT-LIB 按不同的理论域将测试用例划分为若干个分组(division)，包括 QF_BV(无量词位向量),QF_IDL(无量词整数差分逻辑),AUFLIA(数组、未解释函数和线性整数运算的组合理论)等。SMT-COMP 的比赛结果是评价 SMT 工具性能的有力依据。同时，这些工具正在被不断的改进，从每年 SMT-COMP 的结果可看出已有的 SMT 求解器性能正在提升的同时又有新的求解器涌现。尽管当前 SMT 求解器能力已经取得了极大的

33、提升，并投入到关键的验证领域，但是研究的脚步不会停止，对其仍然可以提出一些值得研究的问题。比如，是否存在新的更高效的理论组合技术使得SMT求解器对独立理论求解算法利用更加充分；是否可以进一步扩充 SMT 求解器对于带量词公式的求解能力；是否可以将更丰富的理论求解算法集成到 SMT 求解框架中等。这其中的一些问题也是各SMT 求解器的研发者正在思考的。可见，SMT 求解技术引起了广泛关注，是当前的一个研究热点。国防科学技术大学研究生院硕士学位论文 第 6 页 表 1.1 SMT 求解器总表 1.2 问题描述问题描述 SMT 求解器具有强大、高效的推理和分析能力，已成为多项领域如模型检验，定理证明

34、，静态分析和谓词抽象的验证引擎。众所周知，一阶逻辑公式不存在完全判定方法，当我们希望 SMT 求解器能解决尽可能多的一阶逻辑公式而进行方法改进时，遇到了一些它无法判定的问题。如下述例子：例例 1)(.(.)()1()0(,:truejSijjiiSiSifalseSfalsetrueNS=+=公式：；，且已知：其中，S 是一个从自然数到布尔值上的映射，且使得 S(0)初始值为 false，待判定的合取公式是一个包含全称量词和存在量词的，并且涉及等式与未解释函数、线性算术、差分逻辑的量化理论组合公式。分别选取支持这些理论并在 SMT-COMP中总排名靠前的求解器 Z3，CVC3 对该例子进行测试

35、，执行结果为“Unknown”，说明目前的 SMT 求解器无法判定该问题。1.3 课题研究思路与内容课题研究思路与内容 上述问题引发了关于 SMT 求解器的两个思考：1)目前 SMT 求解器的求解技术和能力范围；2)如何进一步扩充 SMT 求解器能力。求解器 开源(Y/N)支持的理论分类 Barcelogic N 等式与未解释函数，差分逻辑，线性算术，非线性算术，组合理论 Beaver Y 位向量 Boolector Y 位向量，数组，组合理论 CVC3 Y 所有理论 Alt-Ergo Y 等式与未解释函数，数组，线性算术，组合理论，量化理论 MathSAT4 N 等式与未解释函数，差分逻辑，

36、线性算术，位向量，数组，组合理论OpenSMT Y 等式与未解释函数，差分逻辑，线性算术，位向量，组合理论 Sword Y 位向量 VeriT Y 等式与未解释函数，差分逻辑，组合理论 Yices N 等式与未解释函数，差分逻辑，线性算术，位向量，数组，组合理论，量词理论 Z3 N 所有理论 STP Y 位向量，数组 Spear N 位向量 国防科学技术大学研究生院硕士学位论文 第 7 页 这就是本课题研究的起点。从第一点思考出发分析 SMT 求解技术，从基本概念、理论到 SMT 求解器的基本框架以及求解器关于等式与未解释函数、线性算术、位向量和数组等一阶逻辑中的运算及数据结构的基本算法，继而

37、扩展到理论组合技术。掌握目前主流的 SMT 求解器及对其最新研究进展，切合工业应用背景对这些求解器能力进行公平评测。在研究求解器能力的同时，分析当前 SMT 求解器的不足，鉴定上述公式不可求解的技术原因，找到由该例推广出的一类目前 SMT 求解器无法求解的公式一般表述形式。本课题欲将 SMT 公式转化为自动机的符号化表示即布尔编码，那么，公式判定问题可等价为自动机的判空问题，最终的实验部分实现了在-自动机判空技术背景下使得被转换的 SMT 问题被正确求解，证明了从 SMT 问题到-自动机判空问题转换的合理性。首先，本课题是面向 SMT 求解器支持多种理论组合的判定技术，重点着眼于挖掘 SMT

38、求解器能力的局限性，继而扩充 SMT 求解器能力。具体来说，本文研究内容如下：?切合工业应用背景，着重分析 SMT 求解器理论组合技术，并以该技术为线索，在工业应用测试集上，设计实验对比评测当前主流的 SMT 求解器：Z3，Yices，MathSAT4，CVC3，VeriT；?基于评估结果分析当前 SMT 求解器能力的局限性，找出 1.2 节中示例问题无法求解的原因，并提取一类目前 SMT 求解器无法判定的 SMT 公式一般形式。给出自动机的符号化表示方法，通过等价可满足的布尔编码将 SMT问题转换为-自动机判空问题；?解析 SMT 公式语法，编码实现问题转换算法，实验证明了本文提出的转换算法

39、的正确性和可行性。1.4 课题创新点课题创新点 由于 SMT 求解技术已经引起了验证领域的广泛关注，并且每年的 SMT-COMP的举办也激发了许多研究者的研究热情，SMT 求解技术是在不断前进的。然而，它存在着可改进的地方，如进一步优化理论组合技术，使得判定多理论域组合公式时能更加有效的利用 SMT 技术已有的关于各理论成熟的判定方法，并且尽可能降低理论组合时的额外开销；再如 SMT 求解器对于量化公式的判定不存在完全判定方法，即要么求解出满足该公式的一组解，要么给出不存在这样的解使得该公式可满足的证明。研究者目前为止没有找到关于量词的完全判定方法，当前的研究都是基于特定类型的量化公式而进行。

40、据了解，这些改进都是针对 SMT 求解技术本身的算法上进行的。本课题从工业应用出发，在研究 SMT 求解技术发展和评测 SMT 求解器求解能力，以及分析其局限性的基础上，提出了一种将 SMT 问题国防科学技术大学研究生院硕士学位论文 第 8 页 转换为-自动机判空问题的可满足性问题判定方法，这是对 SMT 求解技术的一种改进、扩充。主要创新点体现如下：?归纳 SMT 求解器理论组合技术，搭建了 SMT 求解器测试平台，选取工业测试集对目前主流的 SMT 求解器进行技术分析和对比评测。这项测试工作不同于以往的包括 SMT-COMP 在内的 SMT 求解器评测工作，在本实验中，测试集完全来源于工业

41、应用。?综合实验结果和示例问题无法判定的原因，分析 SMT 求解器能力局限性，给出一类目前 SMT 求解器无法判定的量化 SMT 问题公式表述的一般形式；将量化 SMT 公式转化为自动机的符号化表示形式，前后者是等价可满足的，于是找到了一种新的 SMT 问题判定方法即将 SMT 公式的判定问题转化为自动机判空问题。1.5 论文结构论文结构 本课题围绕着上述例子而引发的两个思考展开，文章结构组织如下：?第一章为绪论部分。首先介绍了课题研究背景，再通过一个实际的无法判定的 SMT 问题提出本文研究工作的出发点，介绍了课题研究内容，并概括研究工作的创新点，最后介绍了文章整体结构。?第二章为背景知识部

42、分。介绍了 SMT 求解技术及-自动机原理的基本概念和理论。?第三章为工具评测部分。归纳了 SMT 求解器理论组合的新技术并进行对比分析，介绍 SMT 求解器测试平台的相关工作，即选取测试用例集，选取待测试的 SMT 求解器，给出实验结果并分析。?第四章为 SMT 求解器能力扩充部分。综合 SMT 求解技术和第三章的实验结果提出目前 SMT 求解器能力的局限性，并给出一类目前 SMT 求解器无法判定的量化 SMT 问题的一般公式表达形式，给出自动机的符号化表示，将 SMT 问题映射为自动机的符号化表示，通过证明定理 1 保证了在这样的转换方法后公式的可满足性问题等价于自动机的语言判定问题。?第

43、五章实现部分。解析 SMT 公式的语法，实现从 SMT 公式到自动机布尔编码的转换过程，最终通过自动机语言判定得到结果。实验证明了本课题提出的新方法是合理且可行的，兼具理论意义和实际价值。?第六章总结部分。总结全文，并展望下一步工作。国防科学技术大学研究生院硕士学位论文 第 9 页 第二章 SMT 求解技术及-自动机理论 SMT 问题属于一阶逻辑理论范畴，它扩充了 SAT 问题的表达范围，对原问题的描述具有高的精确性。SMT 问题求解就是判定在某理论域中是否存在使得 SMT公式可满足的理论模型。本课题欲将此求解过程转化为-自动机语言判空问题，因此，本章将分别介绍SMT问题及其求解技术和-自动机

44、理论的相关概念和知识。2.1 SMT 求解技术相关概念及理论求解技术相关概念及理论 2.1.1 可满足性问题可满足性问题(SAT)SAT 问题是计算机科学领域一类重要的命题逻辑判定问题，兼具理论和实际意义。它是被证明了的第一个 NP 完全问题，许多其他问题都可被归结为 SAT 问题求解。上世纪 60 年代提出 DPLL 算法是求解 SAT 问题的基本算法，至今仍受到广泛关注。本节介绍 SAT 问题及其求解技术相关知识。2.1.1.1 命题逻辑 命题逻辑28是一种最简单的形式逻辑系统，命题是其主要的研究对象，给定一个命题，则该命题可能为真，亦可为假。通常用小写字母 p，q，r.代表任意命题，并称

45、之为命题变元；用 1(0)表示命题的值为真(假)。可对真假值集合定义一些函数，称为真值函数(布尔函数)。常见的真值函数包括：合取(又称“与”，记为)，析取(又称“或”，记为)，否定(又称“非”，记为)，蕴含(记为)，等价(记为)，异或(记为)。定义定义 2.1 命题逻辑公式命题逻辑公式 1.命题变元是公式(称为原子公式)；2.若是公式，那么()也是公式；3.若1和2是公式，那么()21R也是公式。这里的 R 指，。4.只有由以上 3 条规则生成的表达式是公式。如)(,),(CBACBA是公式，而A则不是公式。定义定义 2.2 命题赋值命题赋值(解释解释)命题赋值(解释)是从命题变元集合到真值集

46、合的映射。若此函数没有完全定义，即仅部分变元被赋值，则称之为部分赋值。一个给定的赋值可确定一个公式的值。如公式)(rqp在p，q，r的值分别为1，1，0时为0，而在p，q，r 的值分别为0，1，0时为1。国防科学技术大学研究生院硕士学位论文 第 10 页 若存在一个赋值使得公式F值为1，则称公式F是可满足的(satisfiable)；若对于任何赋值公式F的值都为1，那么称公式F是重言式，或者永真式。若不存在一个赋值使得公式F值为1，那么称公式F是永假式，即不可满足的(unsatisfiable)。另外，我们将原子公式或其否定称为文字。子句由若干文字析取而成，子句的长度就是文字的个数，只有一个文

47、字的子句即单文字子句。若干子句的合取而成的公式称为合取范式(conjunctive normal form，CNF)。由上述基本知识可以定义 SAT 问题问题，即给定一个CNF公式F，判定是否存在赋值使得公式F是可满足的。2.1.1.2 DPLL算法 上世纪60年代提出的DPLL算法6是求解SAT问题的基本算法。本节将介绍DPLL算法基本知识。首先假设给定的CNF公式由子句集S表示，DPLL算法依照以下4条规则对S做变换直到不可再进行为止。规则规则 1 重言式规则重言式规则 删除S中所有重言式后剩下的子句集为S1。S可满足当且仅当S1可满足。规则规则 2 单文字规则单文字规则 若S中存在一个单

48、文字子句L，则将L取值为真，且从S中删除所有包含L的子句及L本身，得到S1。若S1为空集，那么S可满足。否则，观察S1中每个子句，若它包含L，则从子句中删去该文字。由此得S2。S是可满足的当且仅当S2是可满足的。规则规则 3 纯文字规则纯文字规则 如果文字L的非L未出现在公式中，则称L为纯文字。从S中删除所有包含L的子句，得到S1。S是可满足的当且仅当S1是可满足的。规则规则 4 分裂规则分裂规则 假设子句集S可写成以下形式：lLLLCC)()()()(111LBLBLALAnm 其中Ai，Bj，Ck都是子句，且不含有L或者L。此情况下可派生两个子句集S1，S2：llCCBBSCCAAS=LL

49、LL11121111 那么，S是可满足的，当且仅当S1是可满足的或者S2是可满足的。基本的DPLL算法是一个完全的SAT求解方法。后来发展的SAT求解算法都是基于这几条基本规则，对局部搜索算法和回溯搜索算法进行改进从而形成了高国防科学技术大学研究生院硕士学位论文 第 11 页 效的非完全方法。为了进一步提高效率究者不断改进DPLL的关键技术，如回退(back jumping)，引理学习(lemma learning)，关注文字(watch literal)和重启(restart)等。2.1.2 可满足性模理论问题可满足性模理论问题(SMT)SMT问题29是继SAT问题已经被证实为一类极具应用价

50、值的计算机科学领域重要问题之后而被提出的，它针对SAT问题表达能力受限，抽象层次不高的特性将可满足性问题扩展至一阶逻辑范畴。SMT问题求解算法是在SAT求解技术的基础上发展起来的，并且与近几年得到了飞速发展。本节介绍SMT问题及其求解技术的相关概念和知识。2.1.2.1 SMT问题 上一节中给出了命题赋值(解释)的定义，在此进一步明确赋值模型的概念。定义定义 2.3 赋值模型赋值模型(MF)给出一个公式F以及它的一个赋值，为一个赋值模型当且仅当(F)=true，表示为M，并称M满足公式F：M|=F。SMT问题是在SAT问题的基础上扩充了一阶逻辑理论中的知识，理论T是一个属于一阶逻辑范畴可满足的