Microsoft Word - C764961F.doc

Transcription

1 计算机学报 2010 年第 3 期, 2010,33(3) 基于否证蕴含的极小一阶不可满足子式求解算法 张建民 +, 沈胜宇, 李思昆 ( 国防科技大学计算机学院, 湖南长沙 ) An Algorithm for Extrating Minimal Unsatisfiable Subformulae in First-order Logi Based on Refutation Impliation * ZHANG Jian-Min +, SHEN Sheng-Yu, LI Si-Kun (Shool of Computer, National University of Defense Tehnology, Changsha , China) Abstrat: Explaining the auses of infeasibility of formulae has theoretial and pratial appliations in various fields, suh as software verifiation and analysis. A minimal unsatisfiable subformula an provide a suint explanation of infeasibility, and help automati tools to rapidly loate the errors, and determine the underlying reasons for the failure. We introdue the definition of refutation impliation graph and its forward and bakward reahable verties, and the relationship between the minimal unsatisfiable subformulae and the refutation impliation graph. Based on the relationship, we propose an algorithm based on onflit analysis and refutation impliation, in whih a tehnique alled refutation impliation graph pruning is implemented. We report experimental results on pratial benhmarks, as ompared with the best known depth-first searh algorithm. The results show that our algorithm outperforms the depth-first searh algorithm. While the formulae are beoming more omplex, our algorithm is muh faster than the depth-first searh algorithm. Key words: First-order formula; Satisfiability Modulo Theories (SMT); minimal unsatisfiable subformulae; resolution refutation; refutation impliation graph 摘要 : 解释公式不可满足的原因在软件分析与验证等众多领域都具有非常重要的理论与应用价值, 而极小不可满足子公式能够为公式不可满足的原因提供精炼的解释, 帮助应用领域的自动化工具迅速定位错误, 准确地诊断问题失败的本质缘由 本文针对极小一阶不可满足子式的求解问题, 引入了否证蕴含图及其正向与逆向可达结点的概念, 并证明了不可满足子式与否证蕴含图之间的关系 基于二者的关系, 提出了基于冲突分析与否证蕴含的极小一阶不可满足子式求解算法, 并融合了蕴含图剪枝技术, 以提高算法效率 通过实验与当前最优的深度优先搜索算法进行了比较, 结果表明 : 本文的算法显著优于深度优先搜索算法, 并且随着公式复杂度的增加, 性能优势更加明显 关键词 : 一阶逻辑公式 ; 可满足模理论问题 ; 极小不可满足子式 ; 消解否证 ; 否证蕴含图中图法分类号 : TP302 文献标识码 : A 本课题得到国家自然科学基金 (No ) 资助. 作者简介 : 张建民 (1979-), 男, 山西平遥人, 博士生, 主要研究领域为计算机辅助验证方法, jmzhang@nudt.edu.n, 联系地址 : 国防科技大学计算机学院博士生队, 电话 : ; 沈胜宇 (1975-), 男, 博士, 副研究员, 主要研究领域为计算机辅助设计与验证方法 ; 李思昆 (1941-), 男, 教授, 博士生导师,CCF 高级会员, 主要研究领域为计算机辅助设计与验证方法, 虚拟现实.

2 近年来, 命题逻辑的可满足求解技术得到了飞速地发展, 涌现了众多高效的 SAT 求解器, 目前 SAT 求解器已经成为软件分析与验证等领域的重要工具 但是, 命题逻辑限于其相对较弱的表达能力, 无法表达许多领域的问题, 例如, 软件的分析与验证 [1] 实时系统的验证 [2] 等 ; 而在另外一些应用中, 如汇编代码与 RTL 级 Verilog 代码的验证问题 [3], 布尔逻辑虽然也能够表达与处理, 但由于其抽象层次较低, 例如字变量会转换为一组无关的布尔变量, 因此大大增加了问题的规模, 显著提高了空间与时间的开销 而基于非量化一阶逻辑的可满足问题, 即可满足性模理论 (Satisfiability Modulo Theories,SMT) 问题恰好弥补了 SAT 技术的不足, 迅速成为验证领域的研究热点 可满足性模理论问题源于实际应用需求, 例如软件的形式化验证 电子设计自动化与人工智能等众多领域的问题, 都能够规约为非量化一阶逻辑公式, 采用 SMT 求解器来解决 当公式不可满足时, 通常要求查找不可满足的原因, 诊断与定位问题的错误, 这就要求移除公式中与不可满足无关的短句, 只保留一部分短句, 也就是提取公式的不可满足子式 而极小不可满足子式, 即其所有真子式都是可满足的, 能够给出关于公式不可满足更加精确的解释, 迅速地定位错误, 应用也更加广泛 [4-6] 近年来, 涌现了众多提取布尔不可满足子式的算法 [7-15], 成为形式验证领域最活跃的分支之一 然而, 自从抽象层次更高 表达能力更强的可满足性模理论出现之后,SAT 面临被 SMT 取代的趋势, 并且随着 SMT 求解技术飞速地发展,SMT 求解器已经能够解决实际领域中较大规模的问题, 为求解 SMT 不可满足子式提供了可靠的理论基础与实践平台, 因此 SMT 不可满足子式的求解方法将成为今后研究的重点及主要突破的方向 Cittma 等 [16] 首次提出了求解 SMT 不可满足子式的算法 Lemma Lifting, 该算法采用分离的布尔不可满足子式求解算法与 SMT 求解器相结合的方法, 但该算法并不能保证所得到的 SMT 不可满足子式的极小性 显然, 相对于不可满足子式来说, 极小不可满足子式的求解难度更大, 算法复杂度更高 因此到目前为止, 国际上还没有公开发表的针对如何求解 SMT 极小不可满足子式的研究成果 针对极小 SMT 不可满足子式的求解问题, 提出了基于冲突分析与否证蕴含的极小 SMT 不可满足子式求解算法 (Conflit-Analysis and Refutation-Impliation Minimal Unsatisfiable Subformulae Extrator, CARI-MUSE) 首先给出了否证蕴含图及其正向与逆向可达结点的概念, 而后证明了它们与不可满足子式的关系 算法基于这些结论, 通过记录 SMT 求解器在证明公式不可满足性的过程中产生的消解否证, 同时构造其否证蕴含图 而后依次选择蕴含图中原始短句, 通过检测原始短句的正向不可达结点集的可满足性, 来确定该短句是否属于极小不可满足子式 ; 若结点集是可满足的, 则将该原始短句加入不可满足子式 ; 否则, 从否证蕴含图中删除该短句及其冲突短句, 构造更小的否证蕴含图 ; 如此反复迭代, 直到遍历否证蕴含图中的原始短句, 这时就得到极小 SMT 不可满足子式 为了提高搜索效率, 算法中集成了蕴含图剪枝技术, 该技术将证明正向不可达结点集的不可满足的步骤, 转换为证明正向可达结点集中不存在一条其短句都为假的路径, 大大减小了算法的搜索空间 实验结果表明,CARI-MUSE 算法的效率明显高于求解极小不可满足子式的深度优先搜索算法 DFS-MUSE ; 并且随着公式复杂度的增加, 性能优势更加显著 1 背景知识 可满足模理论问题基于不包含全称与存在量词的一阶逻辑公式 根据一阶逻辑的定义, 一个 n 元项 τ 可以表示为 : τ = x f ( τ, L, τ ), (1) : 1 n 其中 x 表示个体变元或常元,f 表示 n 元函数变元或常元 而非量化一阶逻辑公式 ϕ 表示为 : ϕ P( τ, L, τ ) τ = τ ϕ ϕ ϕ ϕ ϕ (2) : = 1 n 其中 τ i 为项, 1 i n,p 为 n 元谓词变元 定义 1( 可满足性模理论问题 ). 给出一个非量化的一阶逻辑公式 ϕ, 以及一个赋值模型 M,M 包含一个非空域 M, 其中对于 n 元函数变元 f,m(f):f n M, 对于谓词变元 P,M(P) M n, 对于个体变元 x,m(x) M ; 公式 ϕ 中一个项 τ 的赋值为 M[x]=M(x),M[f(τ 1,,τ n )]=M(f)(M[τ 1 ],,M[τ n ]) 那么,M =ϕ 定义为 :M =P(τ 1,,τ n ) DFS-MUSE 算法及其实现见 它是由本文作者设计的极小 SMT 不可满足子式的求解算法

3 (M[τ 1 ],,M[τ n ]) M(P);M =τ 0 =τ 1 M[τ 0 ]=M[τ 1 ];M = ϕ 0 M ϕ 0 ;M =ϕ 0 ϕ 1 M =ϕ 0 或 M =ϕ 1 ;M =ϕ 0 ϕ 1 M =ϕ 0 且 M =ϕ 1, 如果存在这样的赋值模型 M, 使得 M =ϕ, 那么称公式 ϕ 是可满足的 ; 否则, 称公式 ϕ 是不可满足的 可满足性模理论问题实际上是解决非量化一阶逻辑公式的可满足性问题, 其公式中的函数变元与谓词变元通常基于一些特定的理论域, 而这些理论域都源于应用领域中实际问题的抽象 目前比较常见的理论域包括整数集 / 实数集上的线性算术 (LIA/LRA) 整数集 / 实数集上的差分逻辑 (IDL/RDL) 等式与未解释函数 (EUF) 数组 (AR) 以及位向量 (BV) 等 SMT 求解技术经过近几年的快速发展, 相继出现了 Eager 方法 Lazy 方法以及 [17] 最新的 DPLL(T) 算法, 同时 SMT 求解器也逐渐走向成熟与完善, 目前已经能够解决实际应用中较大规模的问题, 为求解不可满足子式奠定了基础 定义 2(SMT 不可满足子式 ). 给出一个不可满足的非量化一阶逻辑公式 ϕ, ψ = n 1 Ci 是公式 ϕ 的一个 SMT 不可满足子式当且仅当 ψ 是不可满足的, 并且 ψ ϕ, 即 i, 1 i n, 若 C i ψ, 则 C i ϕ, 其中 C i 表示短句 定义 3( 极小 SMT 不可满足子式 ). 给出不可满足的非量化一阶逻辑公式 ϕ, 及其一个不可满足子式 ψ, 那么 ψ 是极小 SMT 不可满足子式当且仅当 φ ψ, 使得 φ 是可满足的 对于 SMT 公式来说, 如果其某个不可满足子式的所有真子式都是可满足的, 那么它是极小不可满足子式 显然地, 相对于不可满足子式来说, 极小不可满足子式的求解难度更大, 算法复杂度也更高 但是极小不可满足子式能够给出关于公式不可满足原因更加精确的解释, 迅速诊断与定位错误, 在实际应用中具有更重要的理论与应用价值 由于在 SMT 求解器中, 都将输入公式转换为合取范式形式从而证明其可满足性, 因此可以利用 CNF 公式的消解理论来提取极小不可满足子式 下面给出消解的定义与消解原理 定义 4( 消解 ). 设 C i 与 C j 为两个短句, 若 l i C i 与 l j C j 是一对互补的文字, 则称 (C i \l i ) (C j \l j ) 为 C i 与 C j 的消解式, 其中 l i 和 l j 称为消解基,C i 和 C j 称为消解母式 引理 1 [18] 若短句 C 为 C i 与 C j 的消解式, 则 (C i,c j ) =C 引理 2 [18] 若 C i = l i 与 C j = l j 为两个单元短句, 并且 l i 和 l j 是一对互补的文字, 则 C i 与 C j 的消解式为空短句, 即 (C i,c j ) = 定义 5( 消解序列 ). 设 S 为短句集, 且 C 为短句, 若存在短句的有穷序列 C 0,, C n, 满足 (1) C n =C; (2) 令 0 i n, 则短句 C i 至少满足下列两个条件之一 : (i) C i S; (ii) j, k,0 j, k< i, 使得 (C j,c k ) =C i ; 那么称短句 C 为 S 的消解结果, 表示为 S - -C, 并将 C 0,, C n 称为由 S 导出 C 的消解序列 引理 3 [18] 设 S 为短句集, 且 C 为短句, 若 S - -C, 则 S = C 引理 4( 消解原理 ) [18]. 短句集 S 为不可满足的当且仅当 S 算法原理 如果根据定义 3 的方法求解极小 SMT 不可满足子式, 假设一个不可满足子式 ψ =n, 那么要进行 2 n 2 次可满足性的判断, 才能确定 ψ 的极小性 所以算法的复杂度非常高, 执行效率也比较低 经过分析, 能够得出下面的结论 : 引理 5 给出不可满足的非量化一阶逻辑公式 ϕ, 及其一个不可满足子式 ψ = n 1 Ci, 其中 C i 为短句, 那么 ψ 是极小 SMT 不可满足子式, 当且仅当从 ψ 中删除任意一个短句 i, C i ψ, 1 i n, 都使得 ψ \C i 是可满足的 采用反证法易证引理 5, 这里不再赘述 根据该结论, 算法只需将不可满足子式删除其中任意一个短句后, 测试剩余短句构成公式的可满足性, 只需进行 n 次可满足性判断, 即可确定其极小性, 从而大大简化了求解极小 SMT 不可满足子式的过程, 降低了算法复杂性

4 根据消解原理, 若短句集是不可满足的, 那么经过有限步消解可以得到空短句, 因此将消解序列的概念延伸, 得到消解否证的定义 : 定义 6( 消解否证 ). 给出一个不可满足的 SMT 公式 ϕ, 令集合 Cla(ϕ)={C C 为 ϕ 中的短句 }, 若 {C 0,, C n } 是 Cla(ϕ) 导出的消解序列, 且 C n =, 则称 R={C 0,, C n 1, } 为公式 ϕ 的一个消解否证 为了能够高效地求解极小不可满足子式, 需要将 SMT 求解器产生的从原始公式到空短句的消解过程记录并转换为一种简洁清晰的数据结构, 因此引入了短句蕴含图的概念 : 定义 7( 短句蕴含图 ). 给出一个不可满足的 SMT 公式 ϕ,g(v,e) 为一个有向无环图 假设 V=V r V, 其中 V r 是由 G 中所有始发结点构成的集合, 即 V r 中结点的入度为 0, 并且 v i V r, 结点 v i 对应的短句 C i ϕ; 而 V 是由 G 中所有非始发结点构成的集合, 由消解结果短句与理论求解器返回的学习短句构成, 称为冲突短句, 记为 D={ C 1, C 2,, C n } 那么: (1) V r = Cla(ϕ), 其中 Cla(ϕ)={C C 为 ϕ 中的短句 }; (2) 对于每一个冲突短句 C i, 都存在一个消解序列 S i ={C i1, C i2,, C ij, (i) C i }, 使得 k, 1 k j,c ij 满足下列两个条件之一 : 第一,C ij Cla(ϕ); 第二, 1 l i, l C i ; C = (ii) m, 1 m j, 在 E 中存在唯一的边 e im, 对应于 C im (3) 出度为 0 的最终结点对应的短句为 n C D, 使得 C ij = 若满足上面的条件, 则 G(V,E) 称为公式 ϕ 的短句蕴含图 而不可满足子式本质上反映的是短句蕴含图中结点之间的逻辑关系, 因此引入短句蕴含图中正向可达结点与逆向可达结点的概念 定义 8( 正向可达结点 ). 给出 SMT 公式 ϕ,g(v,e) 为 ϕ 的一个短句蕴含图, 如果从结点 α 经过 n(n 0) 条边能够到达结点 β, 即存在一条 α 到 β 的路径, 那么称 β 是 α 的正向可达结点 在 G(V,E) 中, 从结点 α 出发所有正向 可达结点构成的集合表示为 FRv(G,; 而从结点 α 出发所有正向不可达的结点构成的集合表示为 ( G, 定义 9( 逆向可达结点 ). 给出 SMT 公式 ϕ,g(v,e) 为 ϕ 的一个短句蕴含图, 如果从结点 β 经过 n(n 0) 条边能够到达结点 α, 即存在一条 β 到 α 的路径, 那么称 β 是 α 的逆向可达结点 在 G(V,E) 中, 到达 α 的所有逆向可达结点构成的集合表示为 BRv(G,; 而不可到达 α 的结点构成的集合表示为 BRv ( G, 定理 1 给出一个不可满足的 SMT 公式 ϕ, 存在一个 ϕ 的消解序列 R={C 0,, C n 1 }, 当且仅当存在一个对应于 R 的短句蕴含图 G(V,E) 证明 : 首先证明充分性, 针对消解序列 R 所包含的短句数 n 采用数学归纳法证明 当 n=1 时,R 只包含 1 个短句, 显然成立 ; 当 n=3 时, 假设 R={C 0,C 1,C 2 }, 则消解过程为 (C 0,C 1 ) =C 2, 且 C 0,C 1 ϕ; 根据定义 7,V r ={C 0,C 1 },V ={C 2 },E={e 1,e 2 }, 其中边 e 1 与 e 2 分别由 C 0 与 C 1 指向 C 2, 构成 G(V r V,E), 满足短句蕴含图的定义, 因此结论成立 ; 假设 n m, 结论成立 ; 当 n=m+1 时,R 产生最终消解结果 C k 的步骤表示为 (C i,c j ) =C k, 根据定义 7 构造否证蕴含图, 此时存在两种情况 : 第一种情况 :C i 与 C j 中只有一个是原始短句, 这里假设 C j ϕ; 而 C i 的消解序列 R i ={C 0,,C i } 包含至多 m 个短句, 符合假设条件, 那么存在一个对应于 R i 的短句蕴含图 G V V, E ) 而后令 V r = r i( i i i C ; l FRv V {C j }, V = V i {C k },E=E i {e 1,e 2 }, 其中 e 1 与 e 2 分别由 C i 与 C j 指向 C k, 构成 G(V r V,E), 满足定义 7, 因此 G(V r V,E) 为短句蕴含图 第二种情况 :C i ϕ, 且 C j ϕ, 假设 C i 与 C j 的消解序列分别为 R i 和 R j, 其包含的短句数记为 n i 与 n j 由 于 k m, 且 C i ϕ,c j ϕ, 因此 n i m 1,n j m 1, 符合假设条件, 那么存在 R i 与 R j 对应的短句蕴含图 Gi ( Vi Vi, Ei ) 和 G j( V j V j, E j ) 而后, 令 V r r r = Vi V j,v = Vi V j { C k },E=E i E j {e 1,e 2 }, 其中 e 1 与 e 2 分别由 C i 与 C j 指向 C k, 从而构成 G(V r V,E), 满足定义 7, 因此 G(V r V,E) 为短句蕴含图 i

5 所以, 给出一个消解序列 R, 则必定存在一个对应于 R 的短句蕴含图 G(V,E) 下面证明结论的必要性, 假设存在一个短句蕴含图 G(V r V,E), 那么针对结点数 V 采用数学归纳法进行证明 当 V =1 时,G 只包含一个空短句, 显然成立 ; 当 V =3 时, 根据定义 7,V ={C 2 },V r ={C 0,C 1 }, 且 (C 0, C 1 ) =C 2, 那么对应于 G 的消解序列 R={C 0, C 1, C 2 }; 假设 V m 时, 结论成立 ; 当 V =m+1 时, 假设 G 的最终结点为 C k, 且 (C i,c j ) =C k,e ik :C i C k,e jk :C j C k, 那么将 G 中的结点 C k 以及边 e ik 与 e jk 删除, 那么剩余的结点和边分别构成两个子图 G i (V i,e i ) 与 G j (V j,e j ), 符合定义 7,G i 和 G j 为短句蕴含图, 并且满足 V i m, V j m 根据假设条件, 可以得到 G i 与 G j 的消解序列 R i 和 R j ; 那么令短句集合 R={C C R i 或 C R j 或 C=C k }, 由于 (C i,c j ) =C k, 且 C i R i,c j R j, 因此 R 构成 C k 的消解序列 所以, 给出一个短句蕴含图 G(V,E), 则必定存在一个对应于 G 的消解序列 R 综合上面充分性与必要性的证明, 得到结论 : 存在一个 ϕ 的消解序列 R, 当且仅当存在一个对应于 R 的短句蕴含图 G(V,E) 证毕 在证明输入公式不可满足性的过程中, 通过修改 SMT 求解器, 使其记录所有冲突结点的消解序列, 以及空短句的消解否证, 同时逐步构造短句蕴含图 G(V,E) 通常来讲, 并不是 G(V,E) 中所有短句都参与到消解空短句的过程, 仅是空短句的逆向可达结点集 BRv(G, ) 才参与该过程 因此能够将 G(V,E) 化简, 把所有与空短句消解无关的结点及其边都删除, 只保留消解否证中的结点, 那么这种非冗余的短句蕴含图称为否证蕴含图 下面给出否证蕴含图的定义 定义 10( 否证蕴含图 ). 给出不可满足公式 ϕ, 及其一个短句蕴含图 G(V,E), 如果从 G 中的每个短句 C 出发, 都至少存在一条路径到达空短句, 那么 G 为否证蕴含图, 记为 G R (V,E ) 如果将定理 1 的结论扩展到否证蕴含图与消解否证上, 是否仍然成立? 经过分析, 给出下面的结论 : 定理 2 给出一个不可满足的 SMT 公式 ϕ, 存在一个 ϕ 的消解否证 R={C 0,, C n 1, }, 当且仅当存在一个对应于 R 的否证蕴含图 G R (V,E ) 证明 : 将定理 1 中的消解序列的概念扩展到消解否证, 而短句蕴含图的概念相应地延伸到否证蕴含图, 根据定义 6 与 10, 易证 给出一个不可满足的 SMT 公式 ϕ, 以及 ϕ 的一个短句蕴含图 G(V,E), 那么否证蕴含图 G R (V,E )= G R (V r V,E ) 的构造方法为 : 其结点集合 V ={v i v i BRv(G R, )}, 即短句蕴含图中所有空短句 的逆向可达结点集, 其中 V r =V ϕ,v =V V r ; 而边的集合 E ={e ij : v i v j v i, v j BRv(G R, )}, 即 E 由所有始点与终点均在 BRv(G R, ) 中的边构成 那么, 根据公式 ϕ 的否证蕴含图 G R (V,E ), 如何得到 SMT 不可满足子式? 下面的结论给出解决方法 定理 3 给出不可满足 SMT 公式 ϕ 的一个消解否证 R, 以及 R 对应的否证蕴含图 G R (V,E ), 那么 BRv(G R, ) ϕ 中的短句合取构成的公式是 ϕ 的一个不可满足子式 证明 : 假设 ψ 为 BRv(G R, ) ϕ 中所有短句通过合取构成的公式 那么 C ψ, 由于 C BRv(G R, ), 根据定义 9 与 10, 表明从短句 C 对应的结点出发, 存在一条路径到达空短句, 也就是说 C 参与到空短句的消解过程 ; 根据引理 4,S ψ - -, 其中 S ψ 表示由公式 ψ 中短句构成的短句集, 则 ψ 是不可满足的 并且证明过程基于 C ϕ, 所以 ψ ϕ, 且 ψ 是不可满足的, 根据定义 2,ψ 为 ϕ 的一个不可满足子式 证毕 下面通过一个例子来说明否证蕴含图及其与不可满足子式的关系 假设一个 CNF 形式的 SMT 公式 ϕ 为 : ϕ = ( a ( x < 0) y 1) ( x < 0) ( a x < 0 y 1) ( a x + y > 3) ( a x < 0 ( y 1)) ( x < 0 x + y > 3) ( a ( x + y > 3)) 公式 ϕ 基于整数集上的线性算术 (LIA) 理论域, 其中 x 和 y 为个体变元,a 是命题变元 图 1 给出了公式 ϕ 的一个否证蕴含图 G R (V r V,E ) 根据定义 10,V r ={C 1, C 2, C 3, C 4, C 5, C 6, C 7 },V ={C 8, C 9, C 10, C 11, C 12, C 13, }, (3)

6 并且 V r V 中的所有结点到空短句都是可达的, 即 V r V =BRv(G, ) 在图 1 中, 短句 C 4 的正向可达结点集为 FRv(G R,C 4 )={C 4, C 9, C 11, C 12, C 13, }, 而短句 C 12 的逆向可达结点集为 BRv(G R,C 12 )={C 1, C 2, C 3, C 4, C 5, C 8, C 9, C 11, C 12 } 3 基于否证蕴含的求解算法 图 1 公式 ϕ 的否证蕴含图 求解极小 SMT 不可满足子式的 CARI-MUSE 算法基于定理 3 的结论, 其主要过程为 : 通过保存 SMT 求解器在证明公式不可满足性时产生的一系列消解步骤, 构成消解否证, 并转换为一个否证蕴含图 ; 但是定理 3 只能从否证蕴含图中提取不可满足子式, 并不保证其极小性, 因此算法需要进一步地推演 首先依次选择蕴含图中的原始短句, 删除该短句及其相关的冲突短句, 将否证蕴含图中的剩余结点构成一个子公式, 调用 SMT 求解器检测其可满足性, 此时通过蕴含图剪枝技术加速该过程 ; 若子公式是可满足的, 则将当前的原始短句加入到不可满足子式中 ; 否则, 表明原始短句不属于极小不可满足子式, 因此将该短句及其冲突短句对应的结点与边从蕴含图中移除, 同时保证非冗余性, 从而构造一个更小的否证蕴含图 ; 而后不断循环, 直到遍历否证蕴含图中的所有原始短句, 此时就得到极小 SMT 不可满足子式 CARI-MUSE 算法的伪代码如图 2 所示 CARI-MUSE 算法的输入为 SMT-LIB 格式的公式 ϕ, 目标是得到 ϕ 的极小不可满足子式 首先, 算法解析输入公式, 并利用 SMT 求解器来求解其可满足性, 并保存所有的消解步骤, 同时构造一个短句蕴含图 G(V,E), 但当前的 G(V,E) 对于空短句的消解过程来说可能是冗余的, 因此需要将其化简为一个非冗余的短句蕴含图, 即否证蕴含图 这里令 G R (V,E )=G R (V r V,E ) 表示一个否证蕴含图, 其中 V r 是指 G R 中所有始发结点的集合, 对应于原始公式 ϕ 中的短句, 而 V 代表所有非始发结点构成的集合, 即中间产生的消解结果短句与理论求解器输出的学习短句 而后算法利用函数 ChooseClause 选择 V U 中的一个原始短句 C α, 检测其是否属于极小 SMT 不可满足子 式 在算法构造否证蕴含图 G(V,E) 的过程中, 同时求解结点 α 的正向不可达结点集合 FRv ( G R, 根据定义 8, 正向不可达结点集 FRv ( G R, 是指在 G(V,E) 中从 α 出发所有不可达的结点构成的集合 为了检测结点 α 对应的短句 C α 是否属于极小不可满足子式, 从 G R (V r V,E ) 中删除 α 的正向可达结点集合 FRv(G R,, 即令 FRv G R 中结点对应的短句构成的公式 φ 作为输入, 调用 SMT 求解器求解 φ 的可满足性 由于 G R (V,E ) 是否证蕴含图, 因此空短句 总是属于 α 的正向可达结点集合 FRv(G R,, 也就是, 从 α 出发经过有限条边最终总能最终到达结点 v, 所以空短句 不会包含在公式 φ 中 那么, 算法以 FRv ( G R, 转换后的公式 φ 作为输入公式, 要么证明 φ 是可满足的, 要么最终产生空短句 (,

7 算法极小 SMT 不可满足子式的求解算法 CARI-MUSE 输入 :SMT 公式 ϕ; 输出 : 极小不可满足子式 MinimalUS; 1 解析公式 ϕ, 转换为内部数据结构 2 记录 SMT 求解器的消解过程 S R 3 根据 S R 为公式 ϕ 构造一个短句蕴含图 G(V,E) 4 将 G(V,E) 化简为否证蕴含图 G R(V r V, E ) 5 MinimalUS = 6 V U = V r 7 while (V U ) do 8 C α=chooseclause(v U ) 9 M = FRv (, G R 10 将 M 转化为子公式 φ 11 if (SMT solver return φ is satisfiable) then 12 MinimalUS = MinimalUS {C α } 13 V U = V U {C α } 14 else 15 记录求解器的消解过程 S M 16 根据 S M 构造 φ 的短句蕴含图 G V V, E ) r r 17 V = V C } 18 N N { α V = FRv( G, α ) V R M 19 EN = { E EFRv( G, α )} EM R M ( M M M 20 转换为 ϕ 的短句蕴含图 G V V, E ) N ( N N N 21 将 G N 化简为 ϕ 的否证蕴含图 G V V, E ) 22 G R(V r V, E ) G V V, E ) 23 V U = 24 return MinimalUS r V P P( P P P 图 2 P( P P P CARI-MUSE 算法 如果 SMT 求解器证明 FRv ( G R, 对应的公式 φ 是可满足的, 令 ϕ\c α 表示从原始公式 ϕ 中移除短句 C α 后的子公式, 那么表明能够得到 ϕ\c α 的可满足赋值模型, 所以短句 C α 属于极小 SMT 不可满足子式, 将 C α 加入 MinimalUS 集合中, 而后跳转到 V U 中的下一个原始短句 如果 SMT 求解器返回公式 φ 是不可满足的, 表示 C α 不属于当前所求解的极小不可满足子式, 此时算法从否证蕴含图 G R (V,E ) 中移除 C α 及其冲突短句所对应的结点 ; 但是必须保证删除这些结点与边后,G R 仍为一个否证蕴含图, 即算法要基于 FRv ( G R, 中的结点构造一个更小的但完整的否证蕴含图, 下面介绍其构造方法 由于公式 φ 是不可满足的, 因此求解器返回一个消解过程 S M, 而后算法构造一个公式 φ 的短句蕴含图 GM ( VM VM, EM ) 根据定义 7, 短句蕴含图的所有始发结点必须是原始公式中的短句, 而 G M 的所有始发结 r 点集合 V M 对应的短句集合为 FRv ( G R,, 因此 G M 仅为 φ 的短句蕴含图, 而不构成原始公式 ϕ 的短句蕴含图, 不能将其作为算法后面循环的输入 但是, GM ( VM VM, EM ) 中冗余的始发结点都是 G R (V,E ) 中的冲突短句, 并且从结点 α 出发是不可达的, 因此可以从集合 V r \C α 中提取这些冲突短句的始发结点, 并且将原始图 G R (V,E ) 中那些从结点 v i V r \C α 到 v j FRv ( G R, 的边 :v i v j 添加到 G M 中, 就能够保证其始发结点对应的短句都属于 ϕ, 从而把 G M 扩展为一个短句蕴含图 根据前面的步骤,CARI-MUSE 算法能够构造一个新的短句蕴含图 GN ( VN VN, EN ), 其始发结点集合 r V N =V \C α, 冲突短句集合 VN = FRv( G, α ) VM, 边的集合是 E N =(E E F ) E M, 其中 E F 表示所有起点或终点 属于 FRv(G R, 的边 由于 GN ( VN VN, EN ) 可能是冗余的, 不构成原始公式 ϕ 的否证蕴含图, 因此要将 G N 化简为否证蕴含图 G V V, E ) 在化简的过程中,G N 中的一些原始短句也可能会被删除, 因此在每次 P( P P P

8 检测到一个原始短句 C α 不属于极小不可满足子式时, 算法不仅要删除 C α, 而且可能移除其他一些原始短句 r 而后算法检 V P 是否为空, 若不为空, 算法通过函数 ChooseClause 选择下一个原始短句, 继续循环 ; 否则, 算法终止, 此时 MinimalUS 即为公式 ϕ 的极小 SMT 不可满足子式 另外, 改变 ChooseClause 函数的选择策略, 以不同的顺序输出短句, 能够得到不同的极小 SMT 不可满足子式 根据定理 3 的结论, 算法仅能从 SMT 公式的否证蕴含图中提取不可满足子式, 而不能保证其极小性, 因此算法必须在否证蕴含图的基础上进一步演绎, 才能得到极小 SMT 不可满足子式 下面给出图 2 所示的 CARI-MUSE 算法的正确性证明 定理 4 给出一个不可满足 SMT 公式 ϕ, 那么 CARI-MUSE 算法的最终结果 MinimalUS 为 ϕ 的一个极小 SMT 不可满足子式 证明 : 根据定理 3, 算法的 line1~line4 得到了 ϕ 的一个不可满足子式, 即否证蕴含图 G R (V r V,E ) 的结点集 V r 对应的所有短句的合取, 记为 ψ 而后算法从 V r 中移除短句 C α, 将 FRv ( G R, 转换后的公式 φ 作为求解器的输入 这时存在两种情况 : 第一种情况 (line11~line13):φ 是可满足的, 即 ψ {C α } 是可满足的, 而 ψ 是不可满足子式, 根据引理 5, C α 属于极小不可满足子式, 保存到 MinimalUS 中 ; 第二种情况 (line15~line23):φ 是不可满足的, 即从 ψ 中移除 C α 不改变 ψ 的最终消解结果, 所以 C α 不属于 极小不可满足子式 ; 而后算法移除 C α 及其相关的冲突短句, 构造一个更小的短句蕴含图 G V V, E ), N ( N N N 并将其化简为 ϕ 的否证蕴含图 GP ( VP VP, EP ); 由于保证了下一次循环的输入始终为非冗余的否证蕴含图, G P 保留了构成极小不可满足子式的短句, 那些在化简过程中删除的原始短句对于空短句的消解来说是冗余的, 因此它们不属于极小不可满足子式 算法继续循环, 直到 ψ 为空 由于 MinimalUS ψ, 根据上面的证明, 每次加入的短句 C α 都是必要的, 而删除的短句都是冗余, 所以,MinimalUS 为 ϕ 的一个极小 SMT 不可满足子式 证毕 以式 3 给出的公式 ϕ 为例来说明 CARI-MUSE 算法的执行过程 假设函数 ChooseClause 返回的短句是 C 1, 那么算法检测 C 1 是否属于极小不可满足子式 而 FRv( GR, C1) ={C 2, C 3, C 4, C 5, C 6, C 7, C 9, C 10, C 11 }, 那么子公式为 φ = C2 C3 C4 C5 C6 C7 C9 C10 C11 将 φ 作为 SMT 求解器的输入, 那么得到 φ 是不可满足 r 的, 并返回 φ 的短句蕴含图 GM ( VM VM, EM ), 其中 V M ={C 2, C 7, C 10, C 11 }, V M ={a (x<0), a, }, 令 C 14 = r a (x<0),c 15 =a,c 16 =,e i,j :C i C j, 则 E M ={e 2,14, e 11,14, e 14,15, e 7,15,.e 10,16, e 15,16 } 但是 V M 中的短句不都属 于原始公式 ϕ, 因此算法将其扩展为公式 ϕ 的短句蕴含图 GN ( VN VN, EN ), 如图 3 所示 由于这个例子比较 简单, GN ( VN VN, EN ) 也为 ϕ 的否证蕴含图, 表明算法从 ϕ 的初始否证蕴含图 G R (V r V,E ) 中移除了结点 {C 1, C 8, C 12, C 13 } 而后算法以 G V V, E ) 作为输入, 继续循环 N ( N N N 图 3 移除短句 C 1 后的否证蕴含图

9 4 蕴含图剪枝技术为了提高 CARI-MUSE 算法的效率, 实现了一种基于否证蕴含图的剪枝技术 (Refutation Impliation Graph Pruning,RIGPruning) 该优化方法的基本思想是 : 给出一个不可满足的公式 ϕ, 将其划分为两个子公式 ϕ=φ ψ, 那么当一个部分赋值模型 M 使 φ=true 时, 则 ψ=false 那么算法求解 FRv ( G R, 对应的公式 φ 的可满足性赋性时, 只要搜索 FRv(G R, 中所有从结点 α 到空短句的路径, 证明不存在一条这样的路径 : 该路径上的所有短句都为 false, 那么就可以表明 φ 是不可满足的, 这样能够显著地减小变元赋值的搜索空间, 加速公式可满足性的判定过程 下面给出蕴含图剪枝技术原理的证明过程 定理 5 给出不可满足的 SMT 公式 ϕ 及其否证蕴含图 G R (V,E ), 若一个部分赋值模型 M = FRv ( G R,, 那么存在一个从 α 到空短句的路径 P={α,, v } FRv(G R,,M 使得 S={C α,, } 中的所有短句都为 false 证明 : 采用反证法, 假设不存在从 α 到空短句的路径 P={α,, v } 根据定义 8 与假设, 空短句 对应的结点 v 不包含在 α 的可达结点集合中, 即 v FRv ( G, 由于 M = FRv ( G,, 即部分赋值模型 M 使得 FRv ( G, 中的所有短句都为 true, 那么 FRv ( G, 中存在一个结点割集 V s, 其对应的短句通过合取构成的子公式 ϕ s 是可满足的 但是空短句 v V s, 根据引理 4 得到, ϕ s 是不可满足的, 产生矛盾 所以, 假设错误 结论成立, 证毕 根据定理 5 的逆否命题 : 如果某个赋值模型 M 使得 FRv(G, 中从结点 α 到空短句的某条路径上的每个短句都为 false, 那么 M = FRv ( G,, 即 M 为 FRv ( G, 的可满足赋值模型 蕴含图剪枝技术利用定理 5 的逆否命题, 如果证明 G R (V,E ) 中不存在这样的路径 P:P 上所有短句都为 false, 那么就说明 FRv ( G, 是不可满足的 通常来说, FRv ( G, 所包含的短句数远远大于 FRv(G, 的短句数, 因此在大多数情况下采用这种方法能够大大简化求解 FRv ( G, 的可满足性的过程, 从而提高算法的效率 以式 3 给出的公式 ϕ 为例来说明定理 5 的结论,G R (V r V,E ) 为 ϕ 的否证蕴含图, 则 FRv( GR, C5) = {C 1, C 2, C 3, C 4, C 6, C 7, C 8 }, 那么使得 FRv( GR, C5) 可满足的部分赋值模型 M={a, (x+y>3), (x<0)}, 那么存在一条路径 P={C 5, C 10, C 13, } FRv(G R, C 5 ),M 使得 P 中的每个短句都为 false 函数 RIGPruning 实现了否证蕴含图的剪枝技术, 集成于 SMT 求解器中 RIGPruning 的基本运行过程为 : 首先, 将 FRv(G, 中所有结点 α 到结点 v 的路径构成一个子图, 记为 G α 而公式 φ 由 FRv ( G R, 中所有结点对应的短句的合取构成, 而后求解器以 φ 与 G α 作为输入, 以深度优先的搜索方式查找 G α 中未被赋值的变元, 并令其为 false 如果在赋值过程中, 遇到了真值为 true 或冲突短句, 那么就将变元的赋值回溯 求解器在 G α 的每条路径上不断地搜索, 直到下面的两种情况之一出现 : (1) 产生一个部分赋值模型 M,M 使得 G α 中的某条路径上的短句都为 false, 那么求解器继续搜索未赋 值的变元, 直至得到 FRv ( G, 的可满足赋值模型 ; (2) 遍历完整个 G α, 表明 G α 中不存在其上所有短句都为 false 的路径, 表明公式 φ 是不可满足的 ; 此时 SMT 求解器继续搜索, 直到产生 φ 的消解否证 5 实验结果与分析 为了验证算法的有效性, 采用业界标准的 SMT Competition 2007 测试集作为基准测试向量 ;SMT Competition 测试集是一年一度的国际计算机辅助验证 CAV 会议中针对 SMT 求解器进行性能评估与竞赛的测试标准, 其所有公式都来源于实际的工业应用 基于测试集中的公式将基于冲突分析与否证蕴含的算法 CARI-MUSE 与深度优先搜索算法 DFS-MUSE 进行了对比与分析, 二者的输入都是 SMT-LIB 格式的公式, 算法的运行环境是 2.5GHz 的 Athlon 2 CPU, 内存 2GB, 操作系统为 Linux 的机器

10 求解极小 SMT 不可满足子式的 CARI-MUSE 算法采用 C++ 与 STL 实现 算法中公式的可满足性检测过程基于一个开源的 SMT 求解器 ArgoLib [19], 它基于 DPLL(T) 算法, 目前支持的理论域包括线性算术 (LRA/LIA) 与差分逻辑 (RDL/IDL) 两种算法的运行时限都设置为 1800 秒 表 1 给出了 CARI-MUSE 算法与 DFS-MUSE 算法基于测试集中 15 个典型公式的实验结果 表中第 2 列数据是每个公式所包含的变元数 ; 第 3 列表示每个公式所包含的短句数 ; 第 4-5 列给出了求解 SMT 不可满足子式算法 (Lemma Lifting +AMUSE) [16] 的结果短句数与运行时间, 该算法不保证不可满足子式的极小性 第 6 列与第 7 列分别是深度优先搜索算法 (DFS-MUSE) 的运行时间与所提取极小不可满足子式包含的短句数 第 8 和第 9 列分别是基本冲突分析与否证蕴含算法 ( 不包含蕴含图剪枝的优化过程 ) 与完整 CARI-MUSE 算法的执行时间对比 ; 最后一列是基本与完整 CARI-MUSE 算法得到的极小不可满足子式的长度 表中所有公式的运行时间都是以秒为单位 Benhmarks 表 1 CARI 与 DFS 算法在 SMT 测试集上的实验结果 variables lauses 求解 unsat ore [16] DFS-MUSE CARI-MUSE time size time(s) size time 1 time 2 size bad_ehos_asend.base s_init_frame_gap.base good_frame_update.indution good_frame_update.base windowreal-safe windowreal-safe lpsat-goal lpsat-goal lpsat-goal windowreal-no_t_deadlok windowreal-no_t_deadlok windowreal-no_t_deadlok windowreal-no_t_deadlok windowreal-no_t_deadlok windowreal-no_t_deadlok 图 4 给出了 CARI-MUSE 算法与 DFS-MUSE 算法基于 SMT Competition 2007 测试集中的 4 组典型公式的实验结果, 其中横坐标轴表示原始公式所包含的短句数, 而纵坐标轴表示算法的运行时间, 单位为秒, 图中的两条曲线分别表示 CARI-MUSE 算法与 DFS-MUSE 算法随公式的短句数递增时运行时间的变化趋势 图 4(a) 是基于 inf-bakery-mutex 测试集, 其公式所包含的短句数范围从 65 到 1053; 图 4(b) 对应于 windowrealno_t_deadlok 测试集, 其公式包含的短句数范围是 203 到 3908; 图 4() 基于 pursuit-safety 测试集, 其公式短句数的范围是 113 到 1763; 而图 4(d) 的测试集是 gasburner-prop3, 其短句数范围是从 28 到 DFS-MUSE CARI-MUSE DFS-MUSE CARI-MUSE runtime runtime number of lauses (a) inf-bakery-mutex 测试集 number of lauses (b) windowreal-no_t_deadlok 测试集

11 DFS-MUSE CARI-MUSE DFS-MUSE CARI-MUSE runtime runtime number of lauses () pursuit-safety 测试集图 number of lauses (d) gasburner-prop3 测试集 CARI-MUSE 与 DFS-MUSE 基于 4 组 SMT 测试集的对比图 5 给出了 CARI-MUSE 算法与 DFS-MUSE 算法基于 SMT Competition 2007 测试集中 200 个公式的实验结果, 运行时限为 1800 秒, 其中横坐标轴表示冲突分析与否证蕴含算法 CARI-MUSE 的运行时间, 纵坐标轴表示深度优先搜索算法的 DFS-MUSE 的运行时间, 二者都采用了对数 (lg) 坐标, 时间单位为秒 从表 1 图 4 与图 5 的实验结果可以看出,CARI-MUSE 算法能够有效地求解 SMT 公式的极小不可满足子式 从表 1 以及图 4(a)~(d) 中能够直观地看出,CARI-MUSE 算法明显优于深度优先搜索算法 DFS-MUSE 根据表 1 的结果, 完整 CARI-MUSE 算法的运行时间小于去除蕴含图剪枝过程的基本算法, 因此蕴含图剪枝技术能够加速算法的可满足性判定过程 另外从表 1 可以看出,CARI-MUSE 算法得到的极小不可满足子式的短句数显著小于 Lemma Lifting +AMUSE 算法得到的不可满足子式, 但运行时间要大于后者 ; 而在实际应用中, 极小不可满足子式能够给出关于公式不可满足更加精确的解释, 迅速地定位错误, 应用也更加广泛 DFS-MUSE CARI-MUSE 图 5 CARI-MUSE 与 DFS-MUSE 基于 SMT Competition 2007 测试集的对比 在图 5 中, 所有测试集中的公式都位于对角线的上方, 但为了数据在图中分布的均匀性, 采用了对数坐标系, 因此两个算法性能的比值接近于对角线, 但是同样能够表明 CARI-MUSE 算法明显优于 DFS-MUSE 算

12 法 其主要原因是 CARI-MUSE 算法采用了一种更为有效的机制来移除公式中的冗余短句, 它每次从否证蕴含图的原始短句集合中删除的短句数为 n 1,DFS-MUSE 算法每次循环都只从原始公式中删除一个短句 另外, 根据表 1 的实验结果, 对于测试集中的 SMT 公式, 极小不可满足子式所包含的短句数远远小于原始公式的短句数, 通常占公式总短句数的 1% 到 50% 左右, 所以极小不可满足子式能够给出公式不可满足原因更加精确的解释, 更加迅速地诊断与定位错误 根据图 4(a)~(d) 的试验结果分析, 可以发现当公式所包含的短句数与变元数较少时, 尽管 CARI-MUSE 算法优于 DFS-MUSE 算法, 但是两种算法的性能差距并不十分显著 ; 而后随着公式复杂度的增大, 即其短句数与变元数逐渐增加时,CARI-MUSE 算法与 DFS-MUSE 算法的运行时间差距越来越大 表 1 的实验结果也在一定程度上反映了这个规律 而在图 5 中, 随着运行时间的推移, 也就是说公式的复杂度越来越大, CARI-MUSE 与 DFS-MUSE 算法的性能比值的总体趋势是越来越偏离对角线, 表明 CARI-MUSE 与 DFS-MUSE 算法的性能差距越来越显著 综上所述, 可以给出一个结论 :CARI-MUSE 算法明显优于 DFS-MUSE 算法 ; 并且随着公式包含的变元数与短句数不断增加时,CARI-MUSE 算法的性能优势更加显著 这主要是由于当公式较小时, 当把短句蕴含图化简为否证蕴含图时, 通常每次只能删除一个原始短句, CARI-MUSE 算法的优势并没有体现出来 ; 但是当公式的复杂度增加时, 当短句蕴含图进行约简时, 多数情况下会删除多个原始短句, 那么就会提高构造极小不可满足子式的效率, 而 DFS-MUSE 算法每次循环通常都只从原始公式中删除一个短句, 因此这时 CARI-MUSE 算法的性能优势就更加明显 6 结束语本文针对极小 SMT 不可满足子式的求解问题, 引入了否证蕴含图及其正向与逆向可达结点集的概念, 并证明了它们与不可满足子式的关系 ; 提出了基于冲突分析与否证蕴含的极小 SMT 不可满足子式的求解算法 该算法首先为输入公式构造否证蕴含图, 而后选择并移除一个原始短句, 通过检测该短句的正向不可达结点集的可满足性, 从而确定它是否属于极小不可满足子式 算法融合了蕴含图剪枝技术, 从而显著地减小了算法的搜索空间 实验结果表明,CARI-MUSE 算法优于深度优先搜索算法 DFS-MUSE, 并且随着公式逐渐增大,CARI-MUSE 算法的性能优势更加显著, 并通过实验证明了蕴含图剪枝技术的有效性 致谢 感谢 ArgoLib 的作者 Filip Mari 提供了求解器的所有源代码, 并针对本文的算法提出了许多建议 Referenes: [1] S. Ranise and D. Deharbe. Light-Weight Theorem Proving for Debugging and Verifying Units of Code. In Pro. of the International Conferene onsoftware Engineering and Formal Methods. IEEE Computer Soiety Press, [2] Audemard G., Cimatti A., Korni_lowiz A., Sebastiani R. Bounded model heking for timed systems. In Pro. of 22nd International Conf. on Formal Tehniques for Networked and Distributed Systems, LNCS Springer- Verlag, [3] Bozzano M., Bruttomesso R., Cimatti A., Franzen A., Hanna Z., Khasidashvili Z., Palti A, and Sebastiani R.. Enoding RTL Construts for MathSAT: a Preliminary Report. In Pro. of the 3rd Workshop on Pragmatis of Deision Proedures in Automated Reasoning, ENTCS 144. Elsevier, [4] Stukey PJ, Sulzmann M, Wazny J. Improving Type Error Diagnosis. Proeedings of the 2004 ACM SIGPLAN workshop on Haskell, Snowbird, Uppsala, 2004: 80~91. [5] Jain H, Kroening D. Word level prediate abstration and refinement for verifying RTL Verilog. Proeedings of the 42nd Design Automation Conferene, Anaheim, San Diego, 2005: 445~450. [6] Simmonds J, et al., Exploiting resolution proofs to speed up LTL vauity detetion for BMC. Proeedings of the 7th International Conferene on Formal Methods in Computer Aided Design, Austin, 2007: 3~12. [7] Zhang L, Malik S. Extrating small unsatisfiable ores from unsatisfiable Boolean formula. In: Giunhiglia E, Tahella A, eds. Pro. of the 6th International Conf. on Theory and Appliations of Satisfiability Testing. LNCS 2919, Berlin: Springer-Verlag,

13 [8] Oh Y, Mneimneh MN, Z. Andraus S, K. Sakallah A, Markov IL. AMUSE: a minimally-unsatisfiable subformula extrator. In Pro. of the 41st Design Automation Conf., San Diego: ACM, [9] Li XW, Li GH, Shao M. Formal verifiation tehniques based on Boolean satisfiability problem. Journal of Computer Siene and Tehnology, 2005, 20(1), [10] Gershman R, Koifman M, Strihman O, Deriving small unsatisfiable ores with dominator. In: Ball T, Jones RB, eds. Pro. of the 18th International. Conf. on Computer Aided Verifiation, LNCS 4144, Berlin: Springer-Verlag, [11] Dershowitz N, Hanna Z, Nadel A. A salable algorithm for minimal unsatisfiable ore extration. In: Biere A, Gomes CP, eds. Pro. of the 9th International Conf. on Theory and Appliations of Satisfiability Testing, LNCS 4121, Berlin: Springer-Verlag, [12] Zhang JM, Li SK, Shen SY. Extrating minimum unsatisfiable ores with a greedy geneti algorithm. In: Sattar A, Kang BH, eds. Pro. of the 19th Australian Joint Conferene on Artifiial Intelligene, LNAI 4304, Berlin: Springer-Verlag, 2006: [13] Gregoire E, Mazuer B, Piette C. Loal-searh extration of MUSes. Constraints, 2007, 12(3): [14] Liffiton MH, Sakallah KA. Algorithms foomputing minimal unsatisfiable subsets of onstraints. Journal of Automated Reeasoning, 2008, 40(1): [15] Maaren H, Wieringa S. Finding guaranteed MUSes fast. In: Buning HK, Zhao X, eds. Pro. of 11th International Conf. on Theory and Appliations of Satisfiability Testing, LNCS 4996, Berlin: Springer-Verlag, [16] Cimatti A, Griggio A, Sebastiani R. A simple and flexible way of omputing small unsatisfiable ores in SAT modulo theories. In: Marques-Silva J, Sakallah K, eds. Pro. of the 10th International Conf. on Theory and Appliations of Satisfiability Testing, LNCS 4501, Berlin: Springer-Verlag, 2007: [17] Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SAT modulo theories: from an abstrat Davis-Putnam-Logemann -Loveland proedure to DPLL(T). Journal of the ACM, 2006, 53(6): [18] Gallier J.H. Logi foomputer siene: foundations of automati theorem proving. Harper & Row Publishers In, revised in [19] Mari F., Janii P. ArgoLib user manual

14 Bakground This work is primarily supported by the National Natural Siene Foundation of China under grant No with the title Methods of automati program repair based on ounterexample explanation, whih involves in the researh works about automati faults diagnosis, loalization and orretion for programs. The authors have made researhes on algorithms of errors loalization, suh as ounterexample minimization and explanation, unsatisfiable subformulae extration and so on. Although loating and orreting faults is diffiult and time-onsuming, it beomes one of the hot topis in SAT-based and SMT-based formal verifiation. Extrating unsatisfiable subformulae from propositional and first-order formulae an provide a suint explanation of infeasibility, and determine the underlying reasons for the failure. There have been many different ontributions to researh on finding unsatisfiable Boolean subformulae, mostly based on SAT solvers. However little attention has been onentrated on extration of unsatisfiable subformulae in Satisfiability Modulo Theories. This work belongs to part of error diagnosis and loalization, and fous on proposing a new algorithm to deriving minimal unsatisfiable subformulae in SMT based on onflit analysis and refutation impliation.