EUF-DPLL过程：验证等式逻辑公式满足性的扩展Davis-Putnam-Loveland-Logemann过程

理论计算机科学电子笔记225（2009）405-420www.elsevier.com/locate/entcsEufDALG--一个检验等式逻辑公式满足Olga Tveretina1Radboud大学计算和信息科学研究所，荷兰奈梅亨Wieger Wesselink2埃因霍温理工大学计算机科学系荷兰埃因霍温摘要一阶逻辑子集的判定过程构成了许多验证工具的核心。应用程序包括硬件和软件验证。 等式与未解释函数（EUF）的逻辑一阶逻辑的可判定子集。EUF逻辑及其扩展已被应用于证明系统之间的等价性。我们提出了一个分支定界决策过程的基础上推广的Davis-Putnam-Loveland-Logemann过程（EUF-DPLL）的EUF逻辑。EufD是一种工具，用于检查基于此程序的EUF公式的满足性。保留字：具有未解释函数的等式逻辑，可满足性，DPLL过程。1介绍具有未解释函数的等式逻辑（EUF）是用于验证无限状态系统的主要可判定理论[9]。这些函数被称为EUF公式是在项之间相等的原子上的布尔公式。在这个逻辑中，公式具有真值，而项具有来自某个域的值例如，公式：f（x）/f（z）是一个未知数。1电子邮件：o. cs.ru.nl2 电子邮件：j.w. tue.nl1571-0661/© 2008 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2008.12.089406O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405GDPLL过程[2]是著名的DPLL过程[ 6 ]的推广，DPLL过程[6]是在60年代早期作为一阶逻辑的证明过程引入的。GDPLL过程由四个基本操作（REDUCE，Eliqualified，SatCriterion和Filter）定义，必须为特定逻辑填充。在命题逻辑的情况下，原始DPLL过程是GDPLL的实例EUF逻辑的可满足性问题自然适合GDPLL框架。在本文中，我们提供了一个算法，这种逻辑是GDPLL的一个实例。由于该算法是GDPLL的一个实例，我们必须通过验证第3节中提到的条件来检查其可靠性和完整性。EufD是一个工具，用于检查等式逻辑中公式与未解释函数的满足性。它是基于所提出的理论框架。作为编程语言，使用了C++和ATPLAN库。ATTRAN的实现基于最大子项共享和自动垃圾收集。因此，可以在恒定的时间内检查术语的语法一致性1.1应用测试和验证是复杂系统开发的瓶颈这尤其适用于硬件和软件系统。最近定理证明器被用来验证流水线微处理器。Burch和Dill [5]提出的方法大大增强了验证技术。寄存器在计算过程中任何一点的状态都可以用符号项表示未解释的函数可用于将组合逻辑块（例如ALU）抽象为黑盒。没有参数的未解释函数被认为是术语变量，可以用来抽象具有特殊语义的常量值，例如数据值0。因此，具有未解释函数的等式逻辑提供了一种在验证其控制逻辑的正确性时抽象处理器对数据的操作的方法。软件的行为比硬件的行为复杂得多，这是由于程序的潜在的巨大状态空间。强大而复杂的软件系统的开发需要比传统技术更复杂的方法软件系统在规模和功能上都在增长。由于复杂性的增加，出错的可能性 因此，正式核查已成为一项日益重要的技术来建立设计的正确性关于程序操作符的精确推理通常是不可判定的。一种常见的做法是将n元运算符建模为等式理论下的未解释函数。 使用了EUF逻辑对于翻译验证[13，12，14，15]，即通过验证源代码和目标代码之间的等价性来检查编译器翻译的正确性一般来说，这种逻辑主要用于证明系统之间的等价性。该方法有两个阶段：第一个阶段包括构造一个逻辑公式，当且仅当实现相对于规范是正确的时，该逻辑公式才有效。在验证两个公式之间的等价性时，可以用未解释的函数替换除等号和命题运算符之外的所有函数。在第二阶段，O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405407检查公式的有效性。 这个逻辑的有效性问题是可判定的。1.2相关工作在过去的几年里，已经提出了各种程序来检查这些公式的适用性Barrett等人[3]提出了一种基于计算同余闭包结合案例分裂的决策过程。在[1]中，Ackermann指出，确定EUF公式的有效性的问题可以归结为检查等式公式的可满足性。许多当前的方法[7，4]使用EUF公式到等式逻辑公式的变换。然后，等式逻辑公式可以转换为一个比例公式，并且可以应用标准的满足性检查器。Goel et al. [7]和Bryant et al. [4]通过添加传递性约束将等式公式简化为命题公式。在这种方法中，它分析了哪些传递性属性可能是相关的。一种不同的方法被称为范围分配[13，15]。在这种方法中，分析公式结构以定义每个变量的小域。然后使用标准的基于BDD的工具来检查该公式在域下的满足性另一种方法在[8]中给出。这种方法是基于BDD计算，与一些额外的规则来处理传递性。不幸的是，约化的BDD的唯一性丢失。在[10，11]中介绍了一种基于EUF的DPLL过程的方法。所提出的DPLL过程调用正方程的同余闭包模块。2基本定义和分类2.1语法EUF公式可以看作是项之间等式的命题组合这些术语递归定义如下。定义2.1（术语、子术语）• 给定一个签名f =（Fun，ar），项的集合Term（f），或者为了简单起见，在f上的Term，被递归地定义：对于n≥ 0，f（t1，. ..，tn是项，f∈Fun，ar（f）=n.• 我们使用小写字母s、t和u表示术语。• 对于a_c_t_m_f（t1， . . ，tn）∈Termm，n≥0，则setSubTermm（f（t1， . . ，tn））的子项f（t1，. ，t n）递归地定义：nSub Ter m（f（t1， . . ，tn））={f（t1， . . ，tn）}SubTerm（t i）.i=1公式递归定义如下。408O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405定义2.2EUF公式定义如下：formula：=formula|公式|atom原子：=项term：=变量|函数（术语列表），其中变量定义在某个域（可能是有限域）在下文中，EUF-CNF是指合取正规形式的EUF公式。所有EUF-CNF的集合由EUF-Cnf表示。EUF-CNF是子句的连接，其中每个子句是文字的析取。我们将用集合表示法来表示这些合取和析取。在其余的简化和/或更新中，如果已将其删除以进行更新，EQUU IVAALETTOTOSANDT/SRESPECTIVELY.2.2语义设At是一组原子。我们将解释定义为一个函数，I：At→ {true，false}。一个字面l在Ii中为真，或者l是一个原子a且I（a）=真，或者l是一个否定的原子<$a且I（a）=假。我们写I| = l，如果在I中文字l为真。我们将E-解释定义为满足以下条件的解释。• 我|= t t;• 如果我|那我|= t s;• 如果我|= S u和我|那我|= t;• 如 果我|= s it ifor all i∈{1 ，. ，n}则 我|= f（s1，. ，s n） n=f（t1，. ，t n）。我们写I| = φ如果公式φ在I中为真。定义2.3一个公式φ被称为可满足的，如果I| = φ对于某些E-解释I.否则，φ被称为不可满足。根据定义，空分句“不满意”是不可满足的。我们将利用这一时间来完成这一任务。 Lett/S∈ub Ter m（s）。则φ [t：= s]表示一个公式φ，它是通过将项t的反复出现替换为项s直到没有t的出现而从φ获得的。例2.4让我们考虑φ={{f（f（x））<$y}，{x<$g（y）}}。nφ[f（x）：=x]={{x∈y}，{x∈g（y）}}。W e definneφ|l={C−{<$l}|C∈φ，l/C∈}。E示例2.5L etuscond erφ={{x/f（y）， z/g（z）}，{x/f（y）， y/g（z）}}。The n φ|xf（y）={{yg（z）}}。在下文中，Lit（φ）和Term（φ）的意思是，相应地包含在φ中的文字集合和φ中的项集合。O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）4054093数字锁相环的推广戴维斯、普特南、洛格曼和洛夫兰提出的DPLL程序是一些最成功的命题满足性求解器的基础。最初的DPLL程序是作为一阶逻辑的证明程序开发的到目前为止，它在这一章中，我们简要介绍了GDPLL的基本思想，GDPLL是DPLL程序的通用版本。读者可参考[2]以获得完整的描述。DPLL算法是一个完整的，基于回溯的算法，用于确定合取范式中命题逻辑公式的可满足性。它由以下三个规则组成：单位子句规则、拆分规则和纯文字规则。这些规 则根据 某些 标准简 化公式 因此， 假定 执行公 式归约 的所有 规则 的函数REDUCEGDPLL和DPLL一样，也有一个分裂规则，它对DPLL进行了实例分析， 原子，原子如[2]中所定义，我们假设函数REDUCE：Cnf→Cnf，其中Cnf表示合取范式中的公式集我们定义集合R={R∈ EDUCE（Cnf）}|{\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}.在下文中，我们还假设函数• 合格：R→At，• SatCriterion：R→ {true，false}，• Filter，其中Filter（f，a）定义为f∈R和a∈Eligible（f）。在[2]中，对上述函数引入了如下要求：对所有α∈Cnf，对所有α∈R，对所有α∈Eligible（α），函数应满足如下性质。(i) REDUCE（减少）是令人满意的，如果减少令人满意，(ii) 如果滤波器（Filter，a）或滤波器（Filter，a）中的至少一个是满意的，则滤波器（Filter，a）是满意的，(iii) 对于REDUCE（Cnf）上的某个有根据的严格序集，REDUCE（Filter（，a））可解和REDUCE（Filter（，<$a））可解(iv) 如果SatCriterion（条件）=true，则条件满足，(v) 如果SatCrit erion（R）=false，则Eligibl e（R）/=0。该算法如图1所示。 该过程将一个输入α∈Cnf作为输入。GDPLL继续进行，直到函数SatCriterion至少为一个分支返回true，或者为所有分支导出空子句。分别返回SAT或UNSAT4减持规则函数REDUCE由一组归约规则定义，可以以任何顺序应用。在本节中，我们定义EUF-CNF的归约规则410O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405GDPLL（）：{SAT，UNSAT}=开始return（）;如果（∈），则返回UNSAT;如果（SatCriterion（）），则返回SAT;选择∈Eligible（）;如果GDPLL（Filter（a））=SAT，则返回SAT;如果GDPLL（Filter（Filter（Filter，<$a））=SAT，则返回SAT;返回UNSAT;结束;Fig. 1. GDPLL程序从任意的CNF开始，我们可以简化其中包含的所有子句定义4.1（简化条款）• 假设C是一个子句。我们用C↓表示在应用以下简化规则后从CC→C\{t/t}i如果对于任意的t，（t/t）∈C.• 一个子句C被称为单纯化的，如果C = C ↓。给定一个CNF，我们可以通过重复应用以下简化规则来简化它。定义4.2（简化CNF）• 假设a是CNF。我们所说的↓是指应用以下规则后的的标准形式。· 对于某个子句C∈C，C→C↓。· 对于子句C∈C，如果对某项t，（t<$t）∈C，则C→C。• 如果= ↓，则称CNF为简化的。现在我们可以定义一个归约规则系统。从一个任意的CNF开始，我们可以通过重复应用归约规则来转换它我们将使用不相交并集的符号，即当我们写union时，我们是在假设at=t定义4.3（CNF的归约规则）我们定义EUF-CNF的归约系统EUF-REDUCE如下。(i) 如 果 s ， t∈Sub T e r m（ T ） 和 ds/S∈ub T er m （ t ） ，则 {{s <$t}} → {{s<$t}}[ s：= t]。(ii) →约简系统EUF-REDUCE的规则i允许用equals代替equals。回想一下，我们认为文字是无序的，所以这个规则也适用于t规则ii通过从以下等式中删除所有形式t=t的等式来简化CNF：一个公式通过归约规则的变换产生逻辑上等价的CNF。O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405411定义4.4（约化的EUF-CNF）我们定义约化的EUF-CNF是关于约化系统EUF-REDUCE的标准形式。通过以下推论，我们展示了约化的EUF-CNF可能具有的形状。命题4.5如果k是一个约化公式，则下列公式成立。(i) 如果ε={{sεt}}εJ，则heneit hers/S∈ub Ter m（εJ）或rt/S∈ub Ter m（εJ）。(ii) 不包含t t形式的等式。证据 如果n不满足i，则可以应用归约系统EUF-REDUCE的规则i。如果n不满足ii，则可以应用归约系统EUF-REDUCE的规则iiQ我们在4.1节中证明了归约规则集是终止的，所以至少存在一个规范形式。不幸的是，这些规则并不一致，如下面的例子所示。所以范式不是唯一的。例4.6考虑n={{x<$f（y）}，{x<$g（z）}，{f（y）<$h（x，z）}}。(i) 应用约简系统EUF-REDUCE的规则i对x<$f（y），我们可以用f（y）代替x因此，简化公式为：J={{x <$f（y）}，{f（y）<$g（z）}，{f（y）<$h（f（y），z）}}。(ii) 我们也可以用x代替f（y）。结果是简化公式JJ={{x4.1终止现在，我们证明终止的减少系统和相应的GDPLL程序。在下文中，我们使用非传播单位子句的定义，即归约系统的规则i可以应用于的单位子句。定义4.7（非传播单元子句）• 在CNF中，如果存在以下情况，则单元子句{s_t}被称为非传播子句·{st}∈，·s，t∈SubTerm（n\{{s<$t}}）。• NPCl（NPCl）表示NPCl中所有非传播单元子句的集合在定义4.3（i）中，s_t在{{s_t}}周期中不传播，而stispropagatedin{{st}}[s：=t]. Notethats/S∈ub Ter m（n[s：=t]）.我们从引理4.9和定理4.9中使用的一个技术引理开始，四点十一分 引理4.9也是一个技术引理。Lemma4. 8Supposes，t∈Tem，其中s/S∈ub Tem（t），T是s项的集合. 然后|≥|T [ s：= t ]{ s，t}|.|.412O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405证据我们可以观察到，对于任意项TJ和任意项sJ，tJ以下成立。• |为|T j [ s j：= t j]|i如果对于所有分布T U，V ∈ T J，U [ S J：= T J ] / = V [ S J：= T J ]，|ifforalldistinctu,v∈TJ,u[sJ:=tJ]/=v[sJ:=tJ],• |>>| T j [ s j：= t ]j|如果存在不同u，v ∈ T使得u [ s j：= t j ] = v [ s j：= tj ]。|if there are distinct u, v ∈ T such that u [sJ:= tJ] = v [sJ:= tJ].因此，我们认为，|为|（T \{ s，t }）{ s，t}|(T\{s, t}) ∪ {s, t}|≥|（T\{s，t}）[s：= t]{s，t}|为|T [s：= t]{s，t}|Q引理4.9假设f，F，f ∈ Cnf，f ={{s f t}}F，其中s，t ∈ SubTerm（f，J）和ds/∈SubTer m（t），且df={{sft}}f ff，J[s：=t]。 这是不可能的。(i) |SubTerm|子术语（<）|或|or(ii) |≤|子术语（）|和|NPCl（英语：NPCl）|NPCls|NPCl（英语：NPCl<）|.|.证据根据引理4.8，|子术语（）| ≤ |子术语（）|.因此，它是足够的表明，从|NPCl（英语：NPCl）|≥ |NPCl（英语：NPCl）|它遵循|子术语（）|<|子术语（）|.假设|NPCl（英语：NPCl）| ≥ |NPCl（英语：NPCl）|. 则存在某个C∈N使得C/∈NPCls（n）和C[s：=t] ∈NPCls（n）。假设C有n个文字，n≥2。这些文字必须包含至少n+1个不同的原子，以使它们是不同的。 替换[s：=t]映射这些n+ 1个原子与C[s：=t]的2个原子。因此，至少有两个不同的C原子映射到同一个C原子[s：=t]。由此我们可以得出结论，|>>|子术语（）|.|.剩下的是C只有一个字面量的情况 设C ={u ∈ v}，其中u，v∈m。我们可以用一个简单的公式来表示u∈/SubTer m（C）. 如果C[s：=t]∈NPCls（N），则必须使用CJ∈N，CJ/=C[s：=t]，其中u[s：=t]是连续的。 设tCJJ∈u[s：=t]，CJJ/=Cbethhat的子句映射到C J，设w是子句CJ J中映射到u [s：= t]的子项.同样，我们发现两个不同的项u，w ∈ SubTerm（n）映射到相同的项u [s：= t] ∈ SubTerm（n）。 因此，我们可以得出结论，|子术语（）|>>|子术语（）|.Q定义4.10对于每一个ε∈EUF-Cnf，我们用范数（ε）将一对数联系起来，如下所示：（1）A =（|子术语（）|+的|照明（瓦）|、|NPCl（英语：NPCl）|）的。定理4.11归约系统EUF-REDUCE终止。证据我们证明了约简系统EUF-REDUCE的终止性，证明了在将约简系统的每一步应用于公式之后，范数（范数）关于字典序的范数（范数）减少。假设→，/=O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405413(i) Suppose={{st}}J，其中s，t∈Sub Ter m（J）和s/∈Sub Ter m（t），并且={{st}}J[s：= t]。考虑到引理4.8，我们得出结论：|为|L it（j [ s：= t ]<${{ s <$t }}）|Lit(ϕJ[s:=t]∪{{s≈t}})|≤|Lit（j<${{s<$t}}）|为|照明（瓦）|根据引理4.9，|子术语（）|<|子术语（）|或|子术语（）|为|子术语（）|和|NPCl（英语：NPCl）|<|NPCl（英语：NPCl）|.我们得到，要么|子术语（）|+的|照明（瓦）|<|子术语（）|+的|照明（瓦）|或|+|照明（瓦）|为|子术语（）|+|照明（瓦）|和|NPCl（英语：NPCl）|NPCls|NPCl（英语：NPCl<）|.|.(ii) 假设= ↓。然后|≤| L it（）|−| { tt|（t <$t）∈ L it（t）}|−|{t /t}|（t /t）∈ L it（）}|(t/≈t) ∈Lit(ϕ)}|< |照明（瓦）|显然，|子术语（）|≤|子术语（）|. 我们得出结论，|子术语（）|+|照明（瓦）|<|+的|照明（瓦）|.|.因此，请注意，Q我们证明了约简系统EUF-REDUCE是终止的。5可满足性准则在本节中，我们将考虑满足EUF-CNF的条件。这些条件将形成函数SatCriterion的基础。定义5.1（EUF-CNF的核心）设f∈Cnf。然后是一组肯定分句（即完全由长度至少为2的正字面值s（t）组成的子句被称为s（t）的核心，并由Core（t）表示设k是不包含空子句的约化EUF-CNF，使得C or e（k）=k。 我们将 提 供 一 个令 人 满 意 的EUF-CNF模型。在不失去一般性的情况下，我们可以将自己限制在EUF-CNF包含只有单位子句。它从以下事实得出：如果有一个赋值满足CNFφ的每个子句中的一个文字，则φ是可满足的。仅包含单元子句的EUF-CNF的集合由UCnf表示。首先，我们引入了两个二元关系的一组包含在项。定义5.2设f∈UCnf。二元关系是最小的关系，项（）×项（），使得：(i) st，如果{st}∈。(ii)它是自反的、对称的和传递的。414O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405第 五 章 . 3THEEBINAR RRELATIONN=THESMALLESTRRELATIONNOVERSUBTERM（N）×子项（B），使得：O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405415（i）s=t，if{st} ∈.（ii）f（第1条， . . ，sn）n=nf（t1， . . ，tn），ifsin=nti，1≤i≤n，且ndf（s1， .. . . ，sn），f（t1，... ，t n）∈ SubTerm（n）.（iii）n=n，i，r，e，Xive，s，y，m，m，n，t，n，t，n，n，t，n，t，n，n，t，n，n我们将证明一个引理，说明减少CNFs的二元关系是等价的。引理5.4设UCnf是约化的。 则对于每个s，t ∈ Termstifanddotifs = t.证据（）Supposesought. ThenbyDefiniitions5. 2和5。3、我们在s中的位置=t。（）Supposes=t. 我们将根据您的要求进行预处理。假设s/t。这意味着定义5.3的条件（ii）至少应用了一次。在不失一般性的情况下，我们可以假设我们应用了该条件一次。然后有f（s1，.，s n），f（t1，...，t n）∈ SubTerm（n）使得s i≠t i，1 ≤ i ≤ n。在这种情况下，有U0，...，u n∈Term（n），使得{s i=（u0<$u1）}，{u1<$u2}，.，{（u n−1<$u n）= t n}∈ <$，其中i∈ {1，.，n}。在这种情况下，EUF-REDUCE还原系统的规则i将适用。这就与"减少了“的说法相矛盾。 我们得到了这个答案。Q给我5分。5Supposen∈UCnf，nisreddandd{s/nt} ∈Nf orsomes，t∈Ter m. Thensoul/=soul.证据首先，我们用反证法证明了这一点。假设这是不可能的。 那么以下情况之一成立。• s=t。 n{s/s}∈n。在这种情况下，我们可以把它当作一个PP。 这意味着可编程逻辑器件减少了。• 有你0，.，u n∈Term（n），使得{s = u0u1}，{u1u2}，.，{u n−1<$u n= t}∈ n.然后可以应用规则i。 这就与"减少了“我们可以得出这样的结论：S/S。5.我爱你4我们有一个很好的机会。Q416O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405定理5.6<$∈UCnf是不满足的当且仅当存在s，t∈Term（<$）使得{s/t} ∈且s = t。证据 参见[16]。Q方程5.7（Satifabilitycriteria）Supose=dCNF，ε/∈ε，且C or e（ε）=ε. 这是令人满意的。证据 从定理的假设中，我们得出结论，每个长度大于1的子句至少包含一个负文字。令从所有子句中除去除一个负文字外的所有文字，从Cnf中得到 因此，减少了建设。根据引理5.5和定理5.6，可满足。我们可以得出这样的结论，也是令人满意的Q6EUF逻辑的GDPLL构建块我们现在来定义GDPLL程序的构建模块。用于EUF逻辑的过程GDPLL调用以下函数。• 我们定义函数REDUCE（REDUCE）为关于归约系统EUF-REDUCE的任何正规形式。• 对于每个R∈R，函数SatCriterion（）定义如下：.如果Core（ε）=ε，则为真，SatCriterion（饱和度）=否则为假。• 对于每个R∈R，函数Eligible（）定义如下：合格（Eli）= Lit（Core（Eli））。• 对于每个R∈R和每个a∈Eligible（R），函数Filter（）定义为Filter（A，A）={{A}} A|a和过滤器（，<$a）={{<$a}}|-a.例6.1作为一个例子，我们考虑源自翻译器（编译器，代码生成器）验证的公式[13]，其中具体函数已被未解释的函数符号所取代。0={{u1{z/n（f（x1，y1），f（x2，y2））}}.应用规则i后，我们得到1={{u12={{u1O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405417（a）100（b）100f（x）<$f（z）f（x）/<$f（z）ϕ0ϕ1xyx/yϕ2ϕ3f（x）<$f（z）f（x）/<$f（z）ϕ0ϕ1图二. a）一个非终止推导的例子：{0={{x<$y，y<$z}，{f（x）<$f（z）}}。b）终止推导的示例<$0={{x<$y，y<$z}，{f（x）<$f（z）}}3={{u1在应用规则II之后，我们得到4={{u1因为∈4，4是不满意的，所以0也是不满意的。因此，函数REDUCE（）是通过归约规则定义的，可以以任何顺序应用。归约规则允许用等号替换等号，以及通过去除形式tt的所有等式来简化公式。因此，EUF逻辑的所有工作都由函数REDUCE完成。函数Eligible（）允许我们从长度大于1的纯肯定子句中选择文字因此，只要一个简化公式的核心是空的，并且公式不包含空子句，我们就可以用SAT在例6.2中，我们展示了选择在任意正字面量上分裂可以导致非终止派生。例6.2图2（a）给出了一个CNF<$0 ={{x<$y，y<$z}，{f（x）<$f（z）}}的树形表示法的例子 在一个字面量f（x）<$f（z）上的分裂可以导致一个非终止的推导，因为对于一个正的分支<$0是推导出来的。 对于负分支，导出CNF <$1<${{x<$y}，{y<$z}}。在Core（Core）中包含的文字上进行拆分会导致终止派生。对于给定的CNF<$0，Core（<$0）={x<$y，y<$z}。图2（b）中描绘了终止派生。 在对文字x进行分裂后，对于正分支，CNF<$2<${{x<$y}，{f（x）<$f（z）}}被导出，并且对于负分支，导出了CNF<$3<${{y =z}，{f（x）<$f（z）}}根据定理5.7，R2和R3都是满意的。418O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）4057可靠性和完备性在本节中，我们证明了EUF逻辑的GDPLL过程是合理和完整的。我们可以看到，归约系统EUF-REDUCE的规则保持了公式的（不）满足性。引理7.1设f∈Cnf.当且仅当Reduce（减）满足时，则满足。证据我们证明了每一个约简步骤都保持（不）满足性。所以，让我们来看看→- 是的（2）假设满足条件。 假设我是一个任意的E-解释，我|= 0。(i) 补充pose{{st}}J ，其中s，t∈Sub Ter m（ J ）和s/∈Sub Ter m（t），并且{{st}}J[s：= t]。考虑到I| = st，我们得到I| = J [s：= t]。 所以我|= 0。(ii) 让我们来看看。Hence，={C↓|（C∈T）<$（t∈Term：（t<$t）/∈C）}.对于一个C∈N，I|=C. Sinceforeacht∈Ter m，I/=|t/t，我们必须在t/t，|=C↓。所以我|= 0。（2）假设满足条件。假设我是一个任意的E-解释，我|= 0。(i) 补充pose{{st}}J，其中s，t∈Sub Ter m（J）和s/∈Sub Ter m（t），并且{{st}}J[s：= t]。考虑到I = s t，我们得到I| =0.0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000|所以我|= 0。(ii) 假设是↓。 对于每一个C∈N，下列之一成立。• C<$D，其中D∈C。 自从我|那我|= D. 所以我|= C.• （t <$t）∈ C，其中t ∈ Term. 因为对于每个t ∈ Term，I|那我|= C. 因为对于每一个C ∈ C，I |= C，我们得出结论，|= 0。Q引理7.2设f∈Cnf，且s，t∈Term。 “那就不一样了，我都不信。{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080} |standd{{s/t}}|s/tareunsatisfiale。我的律师。 （1）LetIbenarbitraryE-iterpra t insuchtI/=|- 是的 Hence，I/=|{{st}}n d I/=|{{s/t}}不好意思。在不失一般性的情况下，我们可以考虑以下情况：|= st. 在这种情况下I/=|{{s/t}}|s/t。C ons ider{{st}}|好吧。 SinceI|=st，则r是someC∈su c hth atO. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405419I/=|C\{s/t}。 Hence，I/=|{{st}}|好吧。（三）LetIbeanarbitraryE-interpetation。 Sinceboth{{st}}|Stand{{s/t}}|s/tareunsatisfiale，I/=|{{st}}|standdI/=|{{st}}|好吧。如果你不知道，|=storrI|=s/t。 如果你能把所有的东西都弄丢，|=st. Ther eforre，I/=|这是一个很好的选择。Q420O. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405定理7.3（可靠性和完备性）CNF是不可满足的，当且仅当GDPLL（k）返回“不可满足”。证据 为了应用定理5，我们必须检查以下性质。性质i和ii已经在引理7.1和引理7.2中得到证明。性质iv和性质v已在定理5.7中得到证明。为了证明性质iii，我们定义一个有根据的序如下。对于所有的，REDUCE（Cnf）12如果 ΣC∈Core（n =1）|C|<ΣC∈Core（n =2）|C|.通过函数Filter（）的定义，对于所有l∈Eligible（n），C or e（Filt er（n，l））<${C∈C or e（n）|l/C∈}。通过函数Eligible（）的定义，存在某个C∈Core（）使得l∈C。因此，对于每一个l∈Eligible（），Filter（，l）。考虑过滤器（filter，<$l）。 通过函数Filter（）的定义，对于所有l∈Eligible（n），核心（滤波器（滤波器，滤波器））滤波器{C\{l}|C∈ Core（C）}由于存在某个C∈Core（ε）使得l∈C，我们得出结论，对于每个l∈Eligible（），Filter（，<$l）.Q8执行该算法用C++语言实现。使用ATSTOM库[17]来表示文字。在al-出租m中经常发生的文字操作是项的等价性检查和子项的替换。这些操作可以使用ATerms高效地实现。ATtagem实现使用最大子项共享，这使得检查项的语法出于效率原因，简化过程中的包含步骤是可选的。我们实验了一个与命题演算Φn=1≤i j≤nxi/=xjnj=1⎛⎝i∈{x1，···，xn}，i/=j⎞xi=y一个公式，它是[13]中公式的一个生成，m，n =.n1≤ij≤m..nk=1Σxik/=xjkΣfi=fj..n∧i=1Σui/=fiΣ1g=2gi=1ui=fiz=g1在这两种情况下，简单的Meta论证都可以用来证明这些公式是不可满足的。我们的算法能够在几秒钟内解决n= 100的Φn和m = 50，n = 100的Φm，nO. Tveretina，W.Wesselink/Electronic Notes in Theoretical Computer Science 225（2009）405421此外，我们还用随机公式进行了试验。从一组随机子句开始，应用了许多随机替换（如x：=f（x）），以确保可以应用约简。问题大小约为1000个子句和10 个 不 同 的 符 号 。 EufDoppler 算 法 能 够 解 决 所 有 这 些 问 题 。 然 而 ，AnalogicTools程序（SMT-COMP 2005竞赛的获胜者）[11]可以做同样的事情，并且在确定解决方案方面要快得多。9结论和今后的工作本文提出了基于广义DPLL过程的EUF逻辑可满足性问题的求解算法我们的方法是在EufDocs工具中实现的。基于DPLL的系统只有与良好的优化策略相结合才真正有效。该过程可以结合SAT社区为DPLL方法开发的一些优化技术。并非所有适合于命题逻辑的方法都能自动适用于EUF逻辑.有些技术可能会变得不正确，而另一些仍然正确，可能会失去它们的效率。一个 EufDoppler是一个原型实现。 我们已经在不同的环境中进行了测试基准，包括SMT-COMP'05的基准。与其他证明器进行认真的比较还为时过早然而，我们的方法看起来很有希望。它也可以很容易地扩展到计算一个解释作为一组条款的模型未来研究的另一个方向可以扩展到非小句程序。引用[1] Ackermann，W. 决策问题的可解情形。逻辑与数学基础研究。1954年阿姆斯特丹北荷兰[2] 巴德班河，de Pol，J.，Tveretina O.，和Zantema，H. 推广DPLL和等式的可满足性。Information andComputation，vol. 205，issue 8，（August 2007），pp. 1188-1211.[3] 巴雷特角W.，Dill，D.， Levitt