《理论计算机科学电子札记》59卷第3期（2002年）网址：http://www.elsevier.nl/locate/entcs/volume59.html22页As Time Goes By II：并发规则程序的更自动复杂性分析ThomFru赫拉特乌尔姆大学atfur信息Albert-Einstein-Allee 11，D-89069 Ulm，Germany摘要在以前的论文中，我们表明，从一个合适的终止顺序（称为排名）可以自动计算的最坏情况下的时间复杂度的一个我们结合了最坏情况下的推导长度的查询预测从其排名与最坏情况下的估计的数量和成本的规则应用程序的尝试和规则应用程序的成本，以获得所需的元定理。在这里，我们概括了这些论文中提出的方法，并用它来分析几个非平凡的基于规则的约束求解程序。这些结果也适用于幼稚的可扩展性实现。我们还通过测试运行提供了经验证据，表明由于索引等优化，最先进的JavaScript实现的实际运行时间要好得多。关键词：程序分析，复杂性分析，成本分析，排序，推导长度，终止，约束求解，约束处理规则。1介绍[8，1，23]是一种提交选择并发约束逻辑编程语言，由对约束的合取起作用的保护规则组成[6]。一个递归程序由简化规则和传播规则组成。模拟用更简单的约束代替约束，同时保持逻辑等价。传播增加了新的约束，这些约束在逻辑上是冗余的，但可能会导致进一步的简化。CHR的规则一致性[3]和程序等价性[2]等性质已被研究，这些性质对于终止程序是可判定的。在以前的论文[9]中，我们已经证明了使用排名的简化规则程序的终止性。排序将每个简化规则的lhs（左侧）和rhs（右侧）映射到非负整数，例如在CC BY-NC-ND许可下开放访问。FRU辉日2LH的秩严格大于RH的秩。直观地说，给定约束问题的秩会产生规则应用数量的上限，因为每个规则应用都会使秩至少减少1。例1.1考虑偶数约束，它确保自然数（用后继记法表示）是偶数：even（0）<=>true。even（s（N））<=>N=s（M），even（M）.第一规则说even（0）可以被简化为true，这是一个总是令人满意的内置约束。在第二个规则中，内置约束=代表语法相等：N=s（M）确保N是某个数的后继M.逗号代表连词。 规则说，如果偶数是某个数N的后继数，那么这个数的前身数M一定是偶数。如果约束与规则的lhs匹配，则它将被规则的rhs替换。如果没有规则与约束匹配，则约束将延迟。例如，约束问题（查询）甚至（N）延迟。 当添加约束N=0时，even（N）被唤醒，并且行为类似于查询even（0）。它通过rst规则简化为真对于even（s（X））查询，第二个规则是适用的，答案是X=s（M），even（M）。在应用第二个规则之后，查询even（s（0））导致不一致，因为0=s（M）是不满意的。even规则的一个明显的排序是rank（even（N））= size（N）size（0）= 1size（s（N））= 1 + size（N）这个排序不仅证明了终止性，它还给出了推导长度的上限，如果even的参数是完全已知的：随着每个规则的应用，even的参数的秩减少2。在[10]中，我们已经证明导出长度不是最坏情况时间复杂度的合适度量。程序的运行时间不仅取决于规则应用的次数，而且更重要的是取决于规则应用尝试的次数。在[12]中，我们将预测的最坏情况推导长度与规则尝试的次数和成本以及规则应用的成本的最坏情况估计相结合，以获得最坏情况时间复杂度的元定理。实施例1.2[续] 很容易证明，单个偶数约束的最坏情况时间复杂度在推导长度上是线性的，即，军衔如果将秩定义为各个约束的秩之和，则相同的观察结果适用于由几个基础偶数约束组成的查询FRU辉日3然而，当我们添加规则：even（s（X）），even（X）<=> false时，情况发生了变化。其中false是一个始终无法满足的内置约束。 此规则可以适用于查询中的所有偶约束对，并且在用其他两个规则之一来约简单个偶约束之后再次适用。当然，在大多数情况下，规则应用尝试（规则尝试）将是徒劳的。因此，在一个单一的推导步骤中的规则尝试的数量在最坏的情况下是查询中的偶数约束的数量的二次方由于偶数约束的秩至少为1，因此查询的秩是约束数量的界限。推导步骤的数量也受查询的等级限制。总的来说，这产生了一个在查询的排名中是立方的算法。相关工作。据我们所知，只有Ganzinger和McAllester [20，13，14]的工作与我们的工作密切相关，因为它给出了基于逻辑规则的语言的几个复杂性元定理。这些论文研究自底向上的逻辑编程作为一种形式主义表达静态分析和相关算法。[20]关注某些传播规则（在我们的术语中），而[13]通过删除原子公式和规则之间的静态优先级扩展了规则语言，[14]增加了动态优先级。这些规则对应于简化或简化规则[8]以文本顺序应用（可以实现动态优先级作为约束）。Ganzinger和McAllester证明了几个复杂性定理，在许多情况下，这些定理允许通过检查来确定自底向上逻辑程序的渐近运行时间。他们的工作和我们的论文之间的主要区别和互补之处在于，他们考虑了必须应用的规则地面公式在运行时，而我们考虑简化规则，涉及自由变量在运行时和任意内置的约束。他们处理的复杂性，最佳实施方案，使用巧妙的索引和结构共享，而我们的研究结果也适用于天真的实现CHR。在[13]的复杂度元定理中，复杂度是查询的语法大小与潜在前x的最坏数目之和环程序中的规则。前x环是可能出现在推导中的规则的lhs实例的基子公式。(The论文[14]补充道 具有动态优先级的规则的对数因子。）在这里，它是-忽略内置约束的成本-查询的排名和潜在的规则应用程序的数量之和。计算前x环的数量需要了解所有可执行的有效计算中的状态。一旦知道排名，就可以从程序文本本文是[12]的姊妹篇，是在[11]的基础上写成的。 在这里，我们通过允许更多FRU辉日4给出了排序函数的一般定义，并利用它分析了几个非平凡的基于规则的约束求解程序。论文概述。首 先 给出CHR的语法和语义。在第3节中，我们介绍了排名，并展示了如何使用它们来推导最坏情况下的推导长度的上限。 在下一节中，我们将展示如何使用这些推导长度来预测可重构程序的最坏情况复杂度。最 后，本节回顾了一些非线性约束求解程序。基于预测的最坏情况导出长度，根据我们的复杂度Meta定理计算最坏情况时间复杂度。 的预测进行了比较，初步的经验运行时的测量。最后，我们讨论所获得的结果2“”与“”的语义在这一节中，我们给出了语法和语义的，详细信息请参见[3]。 我们假设对（并发）约束（逻辑）编程有一定的了解[19，6]。约束是一阶逻辑中的谓词（原子公式）。我们区分内建（或预定义）约束和非内建（或用户定义）约束。内置约束是由给定约束求解器处理的约束约束条件是由约束程序定义的在下面的定义中，大写字母代表约束的连接。定义2.1一个化简程序是一组CHR。有两种类型的CHR。一个化简程序的形式如下：n @H=> GjB并且传播λ具有形式n @H ==> G jB其中规则具有可选的名称n，后跟符号@。LHS H（head）是一个约束条件的合取。可选的保护G后跟符号j是内置约束的合取。 rhs B（body）是内置约束和非内置约束的结合。通过一个状态转换系统给出了可编程逻辑程序的操作语义。通过推导步骤（转换、归约），可以从一个状态进行到下一个状态。定义2.2状态（或：目标）是内建约束和外建约束的结合。初始状态（或：查询）是一个任意状态。在最终状态（或：answer）中，要么内置约束不一致，要么不再可能有推导步骤推导是一系列推导步骤FRU辉日51nnS1！S2！ S3：。推导长度是推导中的推导步骤的数量定义2.3设P是一个随机程序，CT是一个内建约束的约束理论 过渡关系！ 具体如下：简化好啊！（H=H0）^G^B^C若（H<=>GjB）inP且CTj=C！9x（H=H0^G）传播好啊！（H=H0）^G^B^H0^C如果（H==>Gj B）i nP且CTj=C！9x（H=H0^G）当我们使用程序中的规则时，我们将使用新符号重命名它的变量，这些变量由序列x表示。在约束C的上下文中，具有lhs H和保护G的 规 则 适 用 于 非 线 性 约 束 H0 ， 其 中 条 件 成 立 CTj=C！ 9 x（H=H0^G）.任何适用的规则都可以适用，但这是一个承诺的选择，无法挽回如果一个适用的简化规则（H< => G| B）应用于状态约束H0，状态转移从状态中移除H0，将rhs B添加到状态中，还添加了等式H=H0和保护G。如果传播规则（H==>G|B）应用于H0，则该跃迁将B、H=H0和G相加，但不排除H0。本文最后对规则适用条件CTj = C作了较详细的讨论。 9x（H=H0^G）. 方程（H=H0）是使H和H0中出现的约束条件的乘积相等的一种符号速记法。更准确地说，通过（H^：：^H）=（H0^： ^H0），其中合取可以是1置换，我们的意思是（H1n1n=H0）^：^（H = H0）。 通过使两个约束相等，c（t 1;：; t n）= c（s 1;：; s n），我们的意思是（t 1 = s 1）^：^（t n=s n）. 符号=应被理解为语法相等的内置约束在操作上，规则适用性条件可以如下检查：给定C的内置约束，尝试求解内置约束（H=H0^G），而不进一步约束H0和C中的任何变量。这意味着我们首先检查H0与H匹配，然后检查该匹配下的保护G。因此，在一个可编程实现中，当应用一个规则时，有几个计算阶段：LHS匹配：必须找到当前状态下与规则的lhs约束相匹配的原子约束。保护检查：必须检查当前内置约束是否暗示规则的保护。RHS处理：添 加 了rhs的内置约束和RHS约束。在此之前，lhs的最大值约束被移除。FRU辉日6我在本文中，我们只关心简化规则。对于本文的其余部分，我们假设，可移植程序不包含任何传播规则。3排名和推导公式在这一节中，我们将介绍约束简化规则的排序，并展示如何使用排序来推导最坏情况下的可编程程序的推导长度的上界。排名是一个算术函数，它将术语和公式映射到整数。它是由功能符号、谓词符号和逻辑连接词（在我们的例子中，只有连接词）归纳定义的。公式上的结果阶是全阶。如果我们能证明它对于所考虑的公式是非负的，那么它就是有根据的。当然，我们正在寻找排名，允许决定顺序关系。特别感兴趣的是线性多项式的排名函数。它们很简单，但似乎足以涵盖常见的约束求解程序[9，10]。定义3.1设f是元数为n（n）的函数或谓词符号 0个）设ti（1i n）为项。一个（线性多项式） 秩（函数）定义一个项或约束原子f（t1;：;tn）的秩如下：rank（f（t;：;t））=a f+a frank（t）+：+a frank（t）1n0 11nn其中a，f是整数。 对于每个内置约束C，我们施加rank（C）=0. 合取的秩是其合取的秩之和：rank（（A^B））= rank（A）+rank（B）对于每个公式B，我们要求rank（B）0。该定义将[12]中的定义从自然数推广到整数，特别是不要求变量和约束具有非零的严格正秩。任何内置约束的秩都是0，因为我们假设它们的终止和时间复杂度是已知的。一个内置的约束可能意味着它的参数之间的顺序约束（参数间关系），比如s = t！ rank（s）= rank（t），其中s和t是项。注意，lhs上的=表示两个项s和t之间的语法相等，rhs上的=表示算术相等。这些顺序约束有助于建立终止性，因为它表明规则的lhs的秩总是严格大于规则的rhs的秩。定义3.2设rank是一个ranking函数。简化规则H => GjB的排序（条件）是公式8（啊！ 秩（H）>秩（B）），FRU辉日7其 中 O 是 规 则 中 内 置 约 束 所 隐 含 的 顺 序 约 束 的 合 取 ， 8（（G^B）！ O）。由于终止是不可判定的，一个合适的排名和合适的顺序约束不能完全自动地找到。为了证明终止，目标必须是明确的。定义3.3目标B是有界的，如果B的任何允许实例的秩从上到下由一个常数限定。允许实例的概念允许我们忽略某些实例，例如那些我们认为是病态类型的实例。当然，允许性应该是一个可决定的属性。有界目标不仅终止，它们的等级还提供了规则应用（推导步骤）数量的上限，即推导长度。定理3.4设P是一个只含单纯化规则的规划1. [9]如果排序条件对P中的每个规则都成立，则P对所有有界目标都是终止的。2. [10]如果排序条件对于P中的每个规则都成立，则 P中有界目标 B的最坏情况推导长度 D是 B的秩：D=等级（ B）请注意，引用的论文中的定理仅适用于自然数上的线性多项式排序，但可以推广到任意有根据的排序。4最坏情况时间复杂度我们首先考虑应用单个规则的最坏成本，它包括在当前状态下对所有约束条件尝试该规则的成本和将该规则应用于该状态下的一些约束条件的成本。然后，我们选择程序中最差的规则，并将其应用于推导的最差可能状态。将结果乘以最坏情况下的推导长度，我们就得到了最坏情况下时间复杂度的期望上限在下文中，我们假设一个没有任何优化的简单的ESTO实现。处理内置约束的复杂性由所使用的内置约束求解器预先确定。我们假设检查和添加内置约束的时间复杂度不依赖于推导过程中积累的约束。虽然这在一般情况下不是真的，但它适用于我们迄今为止考虑过的所有约束程序，因为出现在可编程逻辑控制器程序中的内置约束通常是简单的。引理4.1[12]设存在形式为H => GjC^B的简化规则S，其中H是n个约束的合取，G和C是内建约束，B是约束。最坏情况下的时间复杂度为FRU辉日8我我我MaxMaxMax在具有约束条件的状态下应用规则SO（Cn（OH+OG）+（OC+OB））;其中OH是匹配规则的lhsH的复杂度，OG是检查保护G的复杂度，OC是添加rhs内置约束C的复杂度，以及OB是移除lhs H约束和添加rhs H约束B的复杂度。现在我们准备给出关于简化规则程序时间复杂度的元定理。为了计算推导的时间复杂度，我们必须找到应用规则的最坏情况，即推导中任何状态的最大数量的约束条件cmax和可以尝试和应用的最昂贵的规则。我们知道，推导步骤的数量由秩D限定，因为每个推导步骤使D的值至少减少1。这个定理将[12]中的定理推广到了带约束条件的公式的秩可以为零的情形。因此，我们必须重新做（一部分）证明。定理4.2设P是一个只含约束单纯化规则的规划.给定一个查询，其最坏情况的派生长度为D。那么从给定查询开始的推导的最坏情况时间复杂度为：O（DX（（c+D）ni（OH+OG）+（OC+OB）;我其中索引i的范围在程序P中的规则上。证据在朴素实现的最坏情况下，在每个D推导步骤中，所有规则都在约束的最大可能数量cmax的所有组合上尝试，然后应用最昂贵的规则。由于规则应用尝试是相互独立的，我们可以扩展引理1.一套简单的规则时间复杂度为O（X （OHi+OGi）+Maxi（OCi +OBi））;我其中cmax 是从给定查询导出的最坏的约束数，Maxi取所有i中的最大值。由于功能在O-记法中，Max和+是等价的，我们可以用Pi来表示Max xi。这给了我们一个推导步骤的复杂性将得到的公式乘以推导长度D得到总体复杂度：O（D）X（cni（OHi+OGi）+（OCi +OBi）：我现在我们需要一个关于cni的基础它只依赖于查询的属性，即c，查询中约束的数量，以及D，推导长度的上限。在从查询开始的派生的任何状态中，不能有超过c+O（D）的约束，因为我们从c约束开始，最多有D个派生步骤，并且每个步骤都添加了FRU辉日9最多是由程序中的规则给出的某个固定数量的新约束（它也删除旧约束）在用界c+O（D）代替cmax之后，我们得到定理的公式。2注意，在许多情况下，D包含因子c，因此c+D简化为D（如[12]的相应定理从元定理可以看出，规则尝试的成本主导了CHR的朴素实现的复杂性最后，我们对简化规则的组成部分的复杂性作了一些一般性的语法匹配OH的代价由给定程序文本中lhs的语法大小决定因此，它的时间复杂度是恒定的。我们假设在一个简单的实现中，移除和添加约束的复杂度OB（不应用任何规则）是恒定的，例如，列表用于存储约束条件。至于内在的限制因素，我们只能作以下一般性评论。保护检查OG的复杂性通常最多与添加相应约束的复杂性一样高。添加内置约束OC的最坏情况时间复杂度通常是线性的，他们的大小。5约束求解器现在，我们从Sicstus Prolog [15，16]的RISK库中推导出采用弧一致性、采用可变消除和描述逻辑的线性多项式[8]的nite区间域正如在引言的例子中，我们将使用Prolog实现的具体语法，其中合取是由逗号分隔的合取序列。我们将这些结果与来自随机数据的初步测试运行的时间复杂度进行对比。我们希望经验结果比预测的结果更好，因为这种递归实现使用索引来计算规则的lhs匹配所需的约束组合用于测试运行的SicstusProlog和Prolog源代码可从www.informatik.uni-muenchen.de/fruehwir/chr/complexity.pl。该代码可以通过WWW-界面运行在线[23]。对于每个求解器，我们将给出一个排名，这是推导长度的上限。根据排名，我们计算了最差情况下的时间复杂度。我们用数字1表示常数时间复杂度，用0表示零时间复杂度（这意味着根本不执行计算）。我们将在表中总结测试运行的经验结果，例如参见图1。这些表包含以下各列：Goal为生成测试数据而运行的（缩写）目标Worst目标的预测最差情况推导长度D应用规则应用的实际数量，即派生长度。FRU辉日10尝试已尝试但不一定适用的规则的数量在中等工作负载的最新Linux PC上，使用Sicstus Prolog的JavaScript库运行目标的时间（以1.有限域FD有限域是约束逻辑编程的成功案例之一许多现实生活中的组合问题可以在这个约束系统中表达这个约束系统是自60年代后期以来人工智能研究中探索的逻辑编程和有限域约束网络的综合结果。在这个约束系统[25]中，变量被约束为从给定的集合中取其值。为值选择整数允许算术表达式作为约束。约束传播通过从可能值集中删除不参与任何解决方案的值来在这里，我们提出了一个整数区间约束的弧一致性算法的实现[24，5]（nite域约束的特殊情况弧一致性区分了一类特殊的一元约束，其形式为X2S，其中S是给定的nite值集。定义5.1一个原子约束c（X 1;：X n）对于一元约束X 1 2 S 1 ^：：^Xn2 S n的合取是（超）弧相容的，如果对所有i2f1; ：;ng和对Xi从其定义域S i导出的所有可能值，约束X 12 S 1^：：^X n2 S n^c（X 1;：Xn）是可满足的。换句话说，在弧一致原子约束中，每个变量域的每个值都参与原子约束的求解。原子约束可以通过从不参与约束的任何解的变量的域中删除那些值来使其一致 如果每个原子合取是弧一致的，则约束的合取是弧一致的。在我们的例子中，定义域是整数的区间，通过使区间变小，可以从定义域中删除值。在求解器Intv的以下规则中，A：B中的一元区间约束X代表X2fi 2Z jA i^i B g。 in、le、eq和add是内建约束，不等式<、=、>、>=、<>是内建算术约束，min、max、+、-是内建算术函数。整数的区间在只涉及这些函数的计算下是封闭的内置的pre x运算符不会对它的参数求反。这些规则只影响区间约束，约束le、eq和add保持不变。不一致@ XinA：B< => A>B|错误。交叉点@ XinA：B，XinC：D< => A=< B，C=< D|X in max（A，C）：min（B，D）.规则的不一致性和交集消除了一个区间约束FRU辉日11每个.在规则的保护中使用的内置不等式A= B和C= D守卫中剩余的内置不等式确保在每个规则中，至少有一个区间严格变小。这也适用于以下规则。下面的规则处理不平等：le @ Xle Y，A中的X：B，C中的Y：D< => A=< B，C=< D，B>D|X leY，X in A：D，Y in C：D.le @ Xle Y，XinA：B，Yin C：D< => A=< B，C=< D，C< A|X leY，X in A：B，Y in A：D.eq @ X eqY，A中的X：B，C中的Y：D< => A=< B，C=< D，A<>C|X eq Y，max（A，C）中的X：B，max（C，A）中的Y：D。eq @ X eqY，A中的X：B，C中的Y：D< => A=< B，C=< D，B<>D|X eq Y，A中的X：min（B，D），C中的Y：min（D，B）。下一个规则是加法。add@add（X，Y，Z），A中的X：B， C中的Y：D， E中的Z：F => A= B，C= D，not（A>=E-D，B=< F-C，C>=E-B，D=< F-A，E>=A+C，F=< B+D）|add（X，Y，Z），X in max（A，E-D）：min（B，F-C），Y in max（C，E-B）：min（D，F-A），Z 最大值（E，A+C）：最小值（F，B+D）。复杂性我们根据约束的间隔宽度（大小）对约束进行排序：rank（X inA：B）= 2 + width（A：B）rank（A）= 0，否则width（A： B）= B如果 ABwidth（ A： B）= 1否则对于排名，将2添加到区间宽度，使得空区间和单例区间也具有正排名。从排序中我们可以看出，任何给定区间的目标都是有界的。这对应于约束求解程序的预期用途。我们假设查询中的每个变量都与一个区间域约束相关联，并且在每个原子约束中，所有变量都是成对不同的。令w是查询中区间约束的最大秩，令v是查询中不同变量的数量。 则推导长度由DIntv=vw因为对于每个规则应用，至少一个间隔变小（或被移除）。我们进一步假设算术内置约束需要恒定的时间来计算。所有的警卫和所有的救援人员都需要固定的时间。只有数字FRU辉日12INTVINTV在LHS约束中，n的范围从1到4。因此，根据定理4.2，复杂度为O（vw（（c+vw）4（1 + 1）+（1 + 1）。 因为通过定义v c，我们可以用c代替v，并给出更简单的复杂度表达式O（c5 w5）这在变量没有或有几个区间约束的情况下也成立。实证结果。图1，使用tadd的查询采用v个不同变量的列表，并产生两个约束add（A2i;A2i+1; A2i+2），A2ileA2i+2，其中1 2i v。 因此，对于v个变量，产生了2个约束变量的区间域是随机生成的，它们是非负的，并且对于每隔一个变量，上限增加100，以增加存在约束A2i leA2i+2时的一致性概率。因此，最大区间域大小w为50v。查询len（L，v），genless。. .生成涉及v个变量的v个不相容加法约束的序列，所有域初始宽度为w= 200。该表显示随机问题实例的行为是相当稳定的。实际推导长度可能比预测的最差情况推导长度好得多，但最后一个条目表明，根据问题类型，随着问题大小的增加，最终可能达到最差情况。规则尝试的次数与规则应用程序tadd的数量大致呈线性关系，但对于genless则不然。时间与规则尝试次数大致呈线性关系。对于这个求解器，对于我们研究的初步示例集，变量v的数量与约束c的数量成线性关系，观察到的最差时间复杂度为：Oobs（c2 w）实证结果优于预测的，因为investi- gated的restriction实现使用索引计算的约束的组合所需的lhs匹配的规则。2.线性多项式方程<为了求解线性多项式方程，在现有的约束求解器中采用了变量消除的最小但强大的变体[17]定义5.2线性多项式方程的形式为p+b= 0，其中b是常数，多项式p是系数为ai6= 0的形式为aixi的单项式之和，xi是变量。常数和系数都是数字。FRU辉日13目标最糟糕适用尝试时间Len（L，60），：：：1224075496225117.87tadd（L，100）49019635218940.51tadd（L，100）49019635218940.50tadd（L，100）49019634018430.49tadd（L，100）49019633918310.50tadd（L，100）49019634918850.51tadd（L，200）198039671838691.04tadd（L，200）198039670237941.02tadd（L，200）198039670638091.03tadd（L，200）198039671538541.06tadd（L，200）198039671438481.03genless（U，L，Z），len（L，10），：204088437371.11len（L，20），：4080142072432.12Len（L，30），：61202308135693.96Len（L，40），：81603735249737.23Len（L，50），：1020054824096711.78Fig. 1.区间弧一致性约束下变量是完全有序的。在等式a1x1+：+an xn+b= 0中，变量严格按降序出现。在约束逻辑编程中，约束是递增地添加的。因此，我们不能同时消除所有其他方程中的一个变量，而是逐个考虑其他方程。一个简单的范式FRU辉日14可以表现出不一致性：如果每个方程的最左边的变量是这个变量唯一在最左边出现的，则它是不一致的。因此，下面的两个规则实现了一个求解线性方程的求解器，同时针对旋转点数（近似实数）和有理数。在实现中，我们写eq来表示多项式上的等式。消除@A1*X+P1 eq0，A2*X+P2 eq 0 =>归一化（P2-P1*A2/A1，P3），A1*X+P1 eq 0，P3 eq 0。empty @ B eq 0< => number（B）|B =0。消除规则执行变量消除。需要两个方程FRU辉日15以相同的变量开始。 第一个方程保持不变，它用于消除第二个方程中公共变量的出现。辅助的内建约束规格化将多项式算术表达式简化为新的多项式。空规则说，如果多项式不包含更多的变量，常数B必须为零。在求解器算法中，没有变量是显式的，即不执行枢转。 任何两个具有相同rst变量的方程都可以相互作用。因此，求解器是高度并发和分布式的。求解器可以通过一些规则进行扩展，以创建显式变量绑定，使变量之间的隐式等式显式，使用松弛变量或傅立叶算法处理不等式[23]。复杂性非正式地，规则消除的每次应用从一个等式中删除一个变量的单个出现，并可能引入排名中较小的新变量。更准确地说，排名被定义为：rank（P eq0）= arank（ P）+1;其中arank（E）是算术表达式E中出现的变量的最大秩。我们要求arank（X）1，如果X是变量，arank（e）= 0，如果e不包含任何变量（即，e是地）。我们依赖于以下顺序约束：a 1X 1 + P等式0！ arank（a 1X 1+ P）>arank（P）normalize（E; P）！ arank（E）arank（P）第一阶约束是等式中的单项式按其变量排序二阶约束之所以成立，是因为内置约束normalize不会引入新变量，但可能会消除某些变量的出现。从排序中我们可以看到，只要变量没有实例化到包含其他变量的表达式中（因为这可能会改变算术表达式的排序），目标就有界。换句话说，允许的实例仅通过基础表达式实例化变量。假设在一个给定的查询中有v个不同的变量，c个方程。那么最坏情况下的推导长度为D= O（ cv）;<因为我们可以选择一个arank函数，它将变量与从1到v的所有整数进行排序。对于复杂度，我们可以假设lhs匹配和归一化在v中是时间线性的，因此到达O（cv（（c+cv）2（v+0）+（v+1））），由此产生O（c3v4）：实证结果。在图2中，eqtest（N）生成N个方程，其中N个变量和99到99之间的随机整数系数。最差用途FRU辉日16目标最糟糕适用尝试时间81*21511510.40表示最坏情况推导长度的符号cv。在表中，我们展示了三个示例性测试用例。首先，方程组是稠密的，即每个系数都是非零的，概率为0：99。在第二个测试用例中，非零系数的概率为0： 5。规则尝试和应用的数量大约减半。绝对运行时间现在增加得更快。概率为0： 25和0： 10的测试运行显示了类似的行为。在第三个测试案例中，在每个方程中，只有两个随机选择的变量具有非零系数。N=10，当量试验（N）10*1044440.01N=20，当量试验（N）20*201901900.06.. .40*407797790.4880*80316031603.56N=10，当量试验（N）10*525250.01N=20，当量试验（N）20*1098980.04.. .40*204164160.4580*40157915794.82N=10，当量试验（N）10*21515>0.0N=20，当量试验（N）20*238380.02.. .40*283830.09图二.线性多项式方程约束条件下该表显示由于规则的结构简单（主规则中没有保护），规则尝试的次数与规则应用的次数相同。规则尝试的次数与问题的大小cv成线性关系。对于密集型问题，运行时的复杂度为cv2，因为每个规则应用程序必须考虑多达v个 变量。对于稀疏问题，运行时的复杂度高达c2v2，因为每个规则应用程序需要更多的时间来寻找伙伴约束。总之，对于我们调查的测试用例，观察到的最差时间复杂度为：FRU辉日17false.展开规则将概念名称替换为它们的定义。I：C，Cis S=>I：S， C isa S.I：nota C，C is S<=>I：nota S，C is S.合取规则生成两个新的、更小的断言：I：S和T < =>I：S，I：T。析取是通过带有连接词lazy or的lazy标签搜索来处理的，这在没有情况分裂的简化规则中是不能直接表达的[4]。因此，为了我们的分析目的，我们不得不忽略相应的规则。I：S或T =>>最大值 （I：S lazy or I：T）。exist-in限制生成一个充当见证服务器的新变量FRU辉日19对于限制：I：一些R是S< => （I，J）：R，J：S。必须使用传播规则将值限制传播到所有角色：I：每个R都是S，（I，J）：R ==>J：S。由于传播规则在本文中没有涉及，我们忽略了我们的复杂性分析的目的规则。最终简化规则将补运算符nota向下推到概念项的叶子：I：nota nota S< => I：S.I：nota（S或T）<=> I：nota S和nota T。I：nota（S和T）<=> I：nota S或nota T。I：nota（每个R都是S）<=>I：一些R不是S。 I：nota（someR is S）<=>I：everyRisnota S.复杂性对于复杂性分析，它只适用于简化规则，我们不得不忽略析取和值限制的处理。因此，这意味着我们分析了一个不完整的约束求解器。不完整性意味着求解器是正确的（声音），但不能在所有情况下检测出不满意的能力。此属性是约束求解器的常见现象。我们根据概念术语的大小对约束进行rank（I：s）= size（s）rank（A）= 0否则size（nota s）= 2 size（ s）size（some r is s）= 1 + size（ s）size（ every r is s）=1 + size（ s）size（c）= 1 + size（ s）if（ cisa s）exists否则，size e（f（t1; ：;tn））=1+size e（t1） +：+size e（tn）。从排名中我们可以看到，如果所有概念术语（如s和c）的排名已知，则查询是有界的。由于概念术语是基础，根据定义，它们的等级总是可以计算的。推导长度DDescr由目标中出现的概念项的大小之和限定。由于概念的大小取决于其定义，因此目标的句法大小并不能正确地反映最坏情况下的推导长度。设一个概念项的最大长度为一个常数k。对于不完全约束求解程序，我们有D描述0 =ck：实际上，析取和值限制都导致了指数级的最坏情况时间复杂度.FRU辉日20不完全求解器的复杂度为ODescr（ck（（ c+ ck）2（1 + 0）+
