模型检测是一种被广泛应用的自动化的形式化验证技术，当今在这领域的热门研究课题是如何解决模型检测中的状态爆炸问题．抽象((abstraction)是解决状态爆炸问题最为普遍和重要的技术之一．抽象技术中的一个难题是如何构建恰当的抽象模型．因为过于粗糙的抽象会令验证失败而无法得出结论，过于精确的抽象会令模型过大而无法在有限的时间和空间内完成验证．变量抽象(variable abstraction)技术就比较好的解决了这个难题．本文主要研究变量抽象技术中的极小变量不可满足性(VMU)的一些理论和提取极小不可满足公式的方法． 当基于变量集Va生成—个抽象模型Ma后，我们可以通过模型检测工具验证Ma是否满足公式F(其中F表示所要验证的属性)，如果Ma满足公式F，则原始模型M也同样满足公式F．否则，我们会得到一些抽象反例，通过有界模型检测方法(BMC)我们可以判定这些反例中哪些路径是模型M中同样拥有的，哪些是在M中不存在的，即虚假路径．虚假路径意味着模型Ma太粗糙而并不能够验证预期的结论，这时需要从原始变量集V中抽取新的变量集Va来生成更精细的抽象模型．而理想的新变量集Va就应当满足两个要求： 1．有效性：即基于Va的抽象模型Ma应当剔除所有的虚假路径； 2．极小性：即由比Va更小的变量集V1a所生成的抽象模型M1a中至少包含一条虚假路径．变量极小不可满足性(VMU)的概念的引出就是为了更好的描述这样的问题． 本文集中研究变量极小不可满足逻辑公式(VMU)的一些性质，并给出判定一个不可满足逻辑公式是否是变量极小不可满足的充要条件，从而给出提取变量极小不可满足公式的方法．已有的结论表明了VMU判定问题的复杂性和MU判定问题一样是属于Dp完全的这意味着必须使用启发式搜索方法来解决VMU问题．从近年来流行的一些SAT技术，我们给出一种可实现的从不可满足公式中提取VMU公式的方法．目前流行的有效的SAT技术主要基于两种方法：一种是DP消解法(Davis-Putnam．Resolution)，这是以消解法为基础；还有一种是DLL方法(Davis-Logemann-Loveland)，用回溯搜索的方法寻找可满足的指派(assignments)．在本文中，我们主要采用DP消解法，这种方法可以实现多步消解．给定一个CNF的逻辑公式F，DP消解法通过不断的消去变量最终得到空集或空子句从而达到判断F是否可满足的目的。为了判定一个不可满足公式F是否是VMU公式，我们还引入了依赖子句的概念．直观上说，在DP消解树上，在每一层消解结果中，DP消解法通过消去某个变量x可能得到一些新的子句，我们称这些子句是依赖于x的。显然，如果最后得到的空子句依赖于所有变量，那给定的公式F就是变量极小不可满足(VMU)的。为了便于实现，我们还递归的给出依赖子句的集合表示．在第i步．DP消解式DPi(F)中依赖于xk的依赖子句集Depi(xi)可以表示成下列式子： Depi(xk)=DPi(F)-DPi-1(F)，当k=i时；Depi(xk)=DPi(F)-DPxi(DPi-1(F)-Depi-1(xk))，当1≤k＜i时．基于这个表达式，我们给出提取VMU子公式的算法． DP消解法在实现过程中的—个主要困难就是会产生存储空间爆炸．在每步消解后所有的消解式都必须被存储起来，其中会包含许多冗余子句．BDDs(Binary Decision Diagrams)是一种非常有效的存储子句的数据结构，但传统的BDD结构并不能很好的解决DP消解所产生的空间爆炸问题．ZBDDs(Zero-suppressed Binary Decision Diagrams)的出现让DP消解得到了很好的应用．本文引用ZBDD及基于ZBDD上的算子实现DP消解过程，从而减少了提取VMU公式在空间和时间上的复杂度．ZBDDs采用类似于二叉树的数据结构存储子句，在存储过程中允许结点共享，而且不用考虑文字在子句中的顺序．在用ZBDDs的表示图当中，每条从根结点指向终端结点1，而且所经过的边均标有1的路径代表一个子句．因此这样的数据结构不依赖子句的个数，而依赖于结点的个数，这显然很大程度上节省了存储空间，也就减少了时间的复杂度．给定一个逻辑公式，ZBDD表示法删除了诸如包含子句，重言式等冗余子句，很大地提高了逻辑公式的存储效率．由于这些优点，即使是处理巨大的子句数目的逻辑公式时，基于ZBDD结构上的子句的并，子句的交，子句分配(Clause Distribution)等算子能够同时实现多步消解，并且在DP消解过程同时删除冗余子句，这就非常有效的克服了DP消解法引起的空间爆炸问题．这些优点的应用也很大程度上提高了本文所给出算法的效率．