理论计算机科学电子笔记267（2010）127-138www.elsevier.com/locate/entcs通过识别公共约束加速多面体分析阿克塞尔西蒙1，2德国慕尼黑理工大学信息学院，邮编：85478摘要线性不等式集是一种表达推理工具，用于近似程序的可达状态。然而，连接两个状态的最精确方法是计算由不等式集表示的两个多面体的凸包，这是一种在维度上呈指数的操作的多面体。 我们研究如何在两个输入多面体的相似性可以利用，以提高这一昂贵的操作的性能。特别是，我们讨论了如何共同的等式和某些不等式可以从计算中省略，而不排除的结果。我们揭露了最大的常见等式和不等式转换成一个正常的形式多面体，并给出实验证据的优点，我们的方法。关键词：抽象解释，多面体分析，凸壳，因式分解。1介绍程序中的数值不变量对于优化和验证很重要。在这种情况下，推断这些不变量的最有趣的抽象域之一是凸多面体（简称多面体），它能够推断变量之间的线性关系[5]。线性关系使得表达符号界限成为可能，这些符号界限足以证明，例如，在C程序中不存在buffer溢出，即使终止零字符不固定[14，13]。此外，可以表示函数的输入/输出关系[7]。然而，凸多面体的定义域的连接操作的可扩展性差。最精确的连接是两个多面体的凸包，其结果可以是输入大小的指数。 虽然指数输出是相当罕见的，瓶颈是指数中间表示1这项工作得到了Emmy Noether赠款和CNRS和ENS的INRIA项目“抽象”的支持2电子邮件：Axel. in.tum.de1571-0661 © 2010 Elsevier B.V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.09.011128A. Simon/Electronic Notes in Theoretical Computer Science 267（2010）127⎪⎨`xx+4x=0X14x2X5+x3−x4+x7=−1+x3−x4= 4=零67等式partition1partition 2分区2x3−x4−x8≤8−x3+x4+x8≤ − 4x8≤1−x8≤0x7≤1−x7≤0图1.一、约束集的规范化形式用于计算凸包[15]：给定两个n维多面体作为输入，双重描述方法从通常是n的指数的输入约束计算一组生成元（顶点、射线和线）。类似地，通过投影计算凸壳需要n+1个Fourier-Motzkin变量消元步骤，每一步中的不等式都是二次增长的。这些不平等大多是多余的，必须消除。由于输出通常是可管理的大小，无论如何，我们建议省略两个输入多面体共同的约束，这可以大大减少中间表示的大小。我们通过将一个多面体存储在一个范式[10]中来找到一个最大的公共约束，该范式是通过将多面体中的每个等式代入所有剩余的约束中来获得的，从而得到如图1所示的系统。众所周知，在计算两个多面体的连接时，可以忽略两个多面体共有的等式[4]。我们发现，省略共同的等式确实产生了加速。这与[ 8 ]中的观察相反，[8]中的观察仅识别并移除指数中间表示上的公共等式。我们还表明，不与其他不等式共享变量的常见不等式集可以省略。考虑将图1中的正规化多面体与其中只有x7上的不等式不同的多面体连接起来：首先，公共等式x1+x3−x4+x7=− 1被省略，从而将变量x7从x3，x4，x8中分离出来。其次，表示为“分区1”的公共不等式集合总之，我们的工作做出了以下三个贡献：它证明了共同的等式和条纹（形式为a·x=[l，u]的约束）可以省略;它证明了共同的，不重叠的不等式集可以省略;它给出了这种因式分解的有效性的实验证据在引入规范形式之后，第3节使用投影定义凸壳，第4节使用投影来证明因式分解的正确性。业绩改进情况见第二节。5、在Sect之前6结束A. Simon/Electronic Notes in Theoretical Computer Science 267（2010）1271292x2x25 521x2 ≥112 5821X112 5 8x1图二、 同一凸多面体可以有几种表示2多面体的一个正规形为了识别连接输入中的常见约束，我们首先定义一个多面体的范式，当它被表示为一组等式和不等式时。关于符号，我们将约束写为a·x<$c ∈ I，其中<$i ∈{≤，=}且[a·x <$c]] ∈ P <$Q|X|表示满足约束的点的集合。 我们将[·]提升到与[I]的集合]={[i]]|I∈I}。 最后，我们用Polyn表示所有多面体P∈Polyn在n个变量上的集合.设H：Polyn×Polyn→Polyn表示两个n维多面体的并。图2显示了表示同一个多面体的两组不等式。尽管PHP=P，但是必须明确地计算两个所描绘的多面体的连接，因为从不等式表示中不清楚两个多面体实际上相等。注意，这两个不等式集都是非冗余的，也就是说，在不改变多面体的情况下，没有一个不等式可以被省略。因此，为了使这两个多面体的表示规范化，需要对不等式集进行变换。多面体标准形的第一步是以规范的方式表达约束（等式和不等式）。因此，我们假设系数a∈Zn和常数c∈Z是它们的最低形式。然而，图2中的不等式已经是规范的了。矛盾表示仍然是可能的，因为P嵌入在可由不同的不等式限定的a-logne空间[{2x1 = 3x2 +1}]中我们从约束集中消除等式，通过将每次出现的x1替换为3x2+ 1，并适当地缩放不等式，得到{1≤x2≤5}在示例中。我们说x1在P中被分解。重复因式分解等式中的最小变量，最终得到一个全维的多面体P∈Poly m，即存在m个线性无关的点c1，.。c m∈P. 由此产生的系统由一组等式组成，其矩阵为三角形形式，如图1所示。事实上，Lassez等人[10]证明了上述变换会导致正规形式。为了计算具有不同等式集的两个多面体的连接，每个等式a·x=c只存在于一个多面体中，在不等式集上计算连接之前，将其转换为两个相反的不等式a·x≤c和−a·x≤ −c要替换所有在多面体P∈Polyn中成立的等式，首先需要找到所有等式。许多等式可以通过识别形式为a·x≤c和−a·x≤ −c的不等式对来找到。这自然形成了一种平等，x1c8130A. Simon/Electronic Notes in Theoretical Computer Science 267（2010）127能让人想起很多事一个系统su c has{x+y≤0，−x+y≤0，−y≤0}具有隐式等式，可以使用单纯形来检测。一般来说，给定一组不等式I，单纯形可以用来检验一个不等式a·x ≤ c ∈ I是否也作为等式成立：每当在P中最小化a·x得到最小c时，a·x =c在P中成立并且可以被替换。测试所有不等式的任务可以通过适当的实现技术来细化[12]。下一节介绍多面体上连接操作的一个实现，即使用傅里叶-莫茨金消元计算两个多面体的凸包。我们在这里介绍这种方法，因为它为我们提供了一种方法来讨论两个输入系统中的共同约束3通过投影计算凸壳本节简要回顾了使用Fourier-Motzkin投影[3]计算两个多面体的凸包的原理，该投影已被提出作为当前实现中使用的经典双重描述方法的替代方案[2]。它构成了分解常见约束的基础考虑P12=P1HP2的计算，其可以定义为取每个点x1∈P1与每个点x2∈P2的凸组合：P12 = cl（{x∈Qn|x =（1 −λ）x1 + λx2<$0 ≤λ≤ 1 <$x1∈P1<$x2∈P2}）这里，函数cl表示结果的拓扑闭包，它是nec-这是必要的，因为封闭但有限空间的凸组合可能不是封闭的。见[14]。假设现在Pi=[[Aix≤ci]]，其中i= 1， 2，其中Aix≤ci是矩阵它表示定义Pi的非冗余不等式集合。我们代入这个定义，得到不等式系统的结果P12= cl（{x∈ Qn|x = （ 1 − λ ）x1+ λx2<$0 ≤ λ ≤ 1 <$A1x1≤ c1<$A2x2≤c2}）代入z：=（1 − λ）x1和y：= λx2去除乘法，得到：zP= cl（{x ∈ Qn|x = z + y <$0 ≤ λ ≤ 1 <$A≤cyA≤c}）12 11 −λ1 2λ2由于1−λ和λ是正数，我们可以将不等式组乘以这些因子而不改变≤-关系。然而，这一步增加了λ= 1和λ= 0的新解，其中除法使上一个表达式中的不等式系统的结果不满足。事实上，所得到的系统只包含非严格的不等式，因此是拓扑封闭的。因此，我们可以省略闭包运算，给出：P12={x ∈ Qn|x = z + y <$0 ≤ λ ≤ 1 <$A1z ≤（1 − λ）c1<$A2y ≤ λc2}A. Simon/Electronic Notes in Theoretical Computer Science 267（2010）1271311A′1c′1在上面，很容易看到⎜⎟≤⎝⎜≤现在通过设置z=x−y并将变量λ放在左边来简化P12={x∈Qn|0≤λ≤1<$A1x−A1y+c1λ≤c1<$A2y−c2λ≤0}因此，由连接[A1x≤c1]]H[[A2x≤c2]]满足的点x∈Qn是那些满足以下矩阵的点，对于某些y∈Qn和λ∈Q：好吧x cλ⎝⎜⎟⎠y0⎝0⎠为了计算x上的一组不等式，变量y和λ是亲-这就构成了通过投影计算凸包的思想除了给出一种构造性的方法来计算凸壳外，上述特征还表现出一些有趣的性质。使用傅里叶-莫茨金消去法消去v ∈ { y，λ }将计算矩阵的行的正组合，使得v的系数为零。因此，一旦所有变量y、λ被消除，结果中的每个不等式i是矩阵的行的正线性组合，使得y和λ上的项加起来为零。因此，每个i都是不等式A1x≤c1加上由−1和1项产生的常数的正线性组合从凸壳的这种表示可以导出一些有趣的性质例如，考虑在两个输入多面体中都存在的不等式a·x≤c需要凸包（即P1HP2[[a·x≤c]]）。这可以通过考虑以下系统直接证明，其中AJi和cJi表示没有a·x≤c的输入系统：埃克塞特，c好吧 Σ⎜c′1⎟⎜ ⎟ ⎜,0,⎟y⎝⎜⎟⎠λ0⎟⎠01给定系统，顶部系统的第一行可以被添加到中间系统的第一行，导致输出系统中的a·x≤c。注意，这个不等式可能是多余的。在下一节中，我们将使用凸壳的上述特征来推导某些不等式可以省略而不需要检查结果。由于上面的表示是从凸包的定义导出的，下面的结果同样适用于双重描述方法。4分解出常见约束这一节说明了连接输入中的某些常见不等式可以通过基于上一节中凸包计算的矩阵特征进行论证而省略。X的1−A1C10一个2 −c20··· 00··· 0−10··· 00··· 01，a， ，−a，−A′1，c，0，a，A′2，−c，−c′20··· 00··· 00··· 00··· 0−11132A. Simon/Electronic Notes in Theoretical Computer Science 267（2010）1270A′1c′1⎜⎞⎟⎛⎛ ⎞ ⎞⎝⎠- 是的Σ−c⎜⎠4.1省略常见的等式和条纹通过把一个多面体变换成第2节所描述的正规形，多面体所嵌入的空间在它的等式集合中是显式的。此外，由于等式集合的左手边是对角线形式，所以很容易识别两个多面体共有的等式。给定两个多面体P1，P2∈Polyn中的m个公共不等式，可以将其凸包的计算限制在（n-m）维子空间中，并将省略的公共不等式加回结果而不改变结果[4，p. 84]。这种方法的正确性可以通过假设两个多面体都是归一化的并且包含两个对应于等式1，.的相反不等式来证明。a n=x = c，其中a1/= 0，导致以下系统：⎛好吧 X轴yλC⎜⎜⎝−c⎟⎠⎟⎜ ⎟≤⎜⎝c′1001这里，aJ= a2，. a nj表示没有a 1的等式约束的系数，并且AJ1、AJ2、cJ1、cJ2表示输入多面体的剩余系数。如前所述，凸包由投影变量y，λ产生的不等式定义，即，中间的柱子。特别是，消除y1只能组合每个子系统的第一和第二行。因此，系数在y S= 10y2，. y n和λ抵消，产生以下矩阵：100万美元1999年，⎜ ⎟⎜⎜⎝y′⎠⎟λ≤⎜⎝c′1001除了说明最终系统中的x1由输入多面体的两个相反的不等式定义之外，上述系统还表明，消除剩余变量yJ，λ不能将任何其他不等式与两个相反的不等式结合起来，因为它们对yJ和λ的系数为零。Imbert证明了Fourier-Motzkin投影的结果与消除变量的序列无关[9]。因此，选择首先消除y1并不影响上述观察的一般性。因此，等式可以从凸包计算中省略，而无需检查结果。这一观察结果自然可以归结为几个等式。上述结果的一个有趣的概括是，省略由两个常数不相等的相反不等式定义的维度;所谓的条纹。例如，如果两个输入多面体都包含⎟⎠⎟⎛⎜a1a′′−a1− a0 A′1⎛⎜−a1−a′⎞⎟a1a′⎝ ⎠⎛⎜c−c0−⎛⎜a1a′′⎟−a1− a0 A′2⎛⎜ −cC−c′20··· 00··· 01，a1a′，−a1−a′，0，0，0，0A′1−A′1c′10A′2−c′20··· 00··· 00··· 00··· 0−11A. Simon/Electronic Notes in Theoretical Computer Science 267（2010）1271335≤x1+x2≤ 10，并且输入多面体中没有其他不等式提到x1，则两个相反的不等式x1+x2≤10和−x1−x2≤ −5将触发与相反的不等式约束10≤x1 +x2≤ 10相同的运算。通过完全去除上界，可以得出，两个输入多面体共有的一个不等式a·x≤c也可以省略，如果它包含一个在任何其他不等式中不存在的变量。分解出相等和条带如何提高性能？假设两个输入多面体中的公共等式没有被移除，但是多面体仍然被归一化，使得每个等式中的最小变量不会出现在任何其他约束中。通过使用首先选择最小变量的投影算法，常见的等式或条纹在任何其他变量被投影出来之前消失因此，相等和条带只会产生很小的管理开销。为了评估双重描述方法的好处，设Vi表示多面体Pi= [[Aix≤ci]]的顶点集，i= 1， 2。 设x1=一个J·x2，. xn <$+ c在P i中成立，由此得出v1 = AJ·<$v2，. v n nn + c对每个顶点成立v1，.v n <$∈Vi，i = 1，2. 从凸外壳计算将生成顶点Vi，J={Vi，j，2，.. v n| 1号线，. v n <$∈ V i}。特别要注意的是，|V iJ|为|V i|因此，我们可以分解出约束不会减少顶点数。 由于运行时间的双重描述方法由生成器表示中的顶点的（通常是指数）数目支配，在N维上分解出公共等式将仅使执行时间减少1/N。然而，当以标准形式存储多面体时，识别公共等式是廉价的，并且可能值得不断减少。一个更有前途的加速凸壳计算的方法是省略常见的不等式，这是下一节的主题4.2省略不等式凸多面体的域可以涉及任何数量的变量，从而创建具有非常复杂的线性关系的状态。在程序分析的上下文中，线性关系通常来自于循环分析。一旦分析了一个循环，任何在循环后保持不变的线性不变量都会被传递到下一个循环的分析中。因此，计算下一个循环的循环不变量对来自前一个循环不变量的不等式和源于当前循环的分析的不等式进行因此，在第一循环中推断的不等式可能会减慢第二循环中的凸包计算。因此，分解出不变化且其变量与变化的不等式Bixb≤ci，i= 1， 2不重叠的不等式Axa≤c的集合这样的系统的凸包可以通过投影y = ya|yb和λ，来自以下矩阵：134A. Simon/Electronic Notes in Theoretical Computer Science 267（2010）1270B1一B1我C1XB⎛⎞1⎝巴塞里湾⎝⎠⎝⎠≤⎝和01⎠≤⎝⎠0112我我我1212巴塞里湾⎝⎠⎜⎟2001年，λ01⎛ ⎞⎛x⎞XB1999年，一⎜ ⎟ ⎜⎟λC10，000美元⎜ ⎟⎜ya⎟≤ ⎜0⎟将ya投影出去将把不等式Axa−Aya+cλ≤c与Aya−cλ≤0结合起来，而忽略yb上非零项的不等式。类似地，投影出剩余的变量yb不会影响投影出ya的结果，因为所有这些不等式对yb的系数都为零。因此，凸壳计算可以分为两个问题：好吧X轴一yaλ⎛c⎞ ⎛- 是的X轴B黄蓝λ1000万美元⎜ ⎟ ⎜0 ⎟ ⎜ ⎟ ⎜0 ⎟由于PHP=P，从左系统投影ya，λ将仅精确地产生系统Ax≤c，除此之外，仅产生冗余不等式。 避免该系统的计算是有益的，因为在投影期间产生的冗余不等式必须通过运行线性程序来测试每个不等式来去除。此外，避免了在投影出yb时处理这些不等式的开销关于双重描述方法，情况变得更糟：假设计算系统Axa≤c和Bixb≤ci，i= 1， 2的顶点分别得到顶点VA和VB，i= 1， 2。 因此，当将系统Axa≤c识别为在两个多面体中相等时，计算输出约束所需的顶点数为|五号B|+的|五号B|. 在相比之下，为每个参数生成顶点，包括为Ax a ≤ c生成的顶点，结果是V AB={Ax a≤ c}|v B |v A∈ V A<$v B∈ V B}，因此，整个框架包含|+的|VAB|为|V A|（|五号B|+的|五号B|）顶点。|) vertices. 因此，生成器表示系统Axa≤c只需要由两个或多个顶点组成，以使省略常见的不等式是有价值的。略正交于省略公共约束的是观察到一组仅出现在一个多面体中的不等式Axa≤c可以省略，只要它不与其他不等式共享任何变量。为了论证的简单，假设这个不等式集存在于第二个多面体中。在这种情况下，矩阵采用以下形式：⎛ ⎞ ⎛xa⎞⎜ ⎟ ⎜⎟C，0，⎜⎝⎟⎜ya⎟≤⎜0⎟投影出ya将移除A的所有系数，而不合并包含yb变量的任何行。因此，Axa≤c对最终结果没有影响，01，A0，，−A0，0−B1，c，C10，A0，0B2，−c，−c2−AC0一−c0··· 00··· 00··· 00··· 0−11−B1C10B2−c20··· 00··· 00··· 00··· 0−110B10−B10，A0，0B2，−c，−c20··· 00··· 00··· 00··· 0−11A. Simon/Electronic Notes in Theoretical Computer Science 267（2010）127135因此可以从凸包计算中省略。在系统中不省略Axa≤c的情况下，通过投影计算凸壳的开销相当于从Axa≤c投影出所有变量，这导致所有被丢弃的双描述方法的开销是计算Axa≤c，B2xb≤c2的顶点，而不是计算B2xb≤c2的顶点，这与一般不等式集的情况类似。因此，省略Axa≤c总是值得的。利用更便宜的凸包的好处的能力取决于上述不等式集合可以多快地被找到。识别不与其他不等式共享变量的不等式集合可以通过使用union-find数据结构在近线性时间内执行[6]：对于任一多面体中的每个不等式i，强制在i中出现的具有非零系数的所有变量处于相同的等价类中在第二个线性过程中，根据等价类划分每个多面体中的不等式。在至少一个多面体中没有与它们相关联的不等式的等价类对于所有其他等价类，每个多面体的不等式都使用可变指数和系数的全序进行排序。两个不等式集合的相等现在可以在线性时间内检测到。每个相等集都可以直接移动到结果集。其余的不等式被传递到凸壳算法。给定一个有效的不等式预处理，下一节将经验地评估这种预处理对凸包计算的好处5实验评价我们评估的影响，建议的因子分解通过计算凸包通过双描述方法和通过投影方法对两个基准套件。特别是，我们生成一个C++和一个Haskell程序，计算每个基准中的所有凸包。 C++程序调用Parma Polyhedra Library（PPL）[2]，版本0.10，以便通过双重描述方法计算凸壳。结果被转换回最小约束表示。Haskell程序通过第3节中描述的投影方法计算凸包。报告的时间不包括解析和翻译成正常形式。我们不报告归一化的时间，因为我们假设等式的检测是在满足操作期间完成的（即，当来自程序的条件的不等式被添加时）。特别地，当满足操作执行约束集的最小化时，可以在最短时间内检测等式[12]。在双重描述方法中，从约束表示和到约束表示的转换可能看起来不公平，因为如果一个或两个输入已经是生成器形式，则不必进行转换。然而，由于每个循环体通常包括某种形式的线性测试，需要约束表示，双重描述方法转换来回两个表示之间至少一次，每个连接点，因此，我们认为假设的输入和输出是在约束形式是现实的。136A. Simon/Electronic Notes in Theoretical Computer Science 267（2010）127基准：保理双描述符双描述符†投影dims伊内克斯没有一1.68s百分百2.51s百分百5.24s百分百8.60百分百10.45百分百asym1.42s百分之八十五2.18s百分之八十七4.94s百分之九十二7.25百分之八十四9.45百分之九十等式1.06s百分之六十三1.50s百分之六十4.63s百分之八十八5.63百分之六十五6.66百分之六十四不平等0.93s百分之五十五1.35s百分之五十四3.72s百分之七十一4.53百分之五十三5.48百分之五十二条纹0.91s百分之五十四1.33s百分之五十三3.72s百分之七十一4.49百分之五十二5.43百分之五十二基准：保理双描述符双描述符†投影dims伊内克斯没有一1.01s百分百1.37s百分百5.31s百分百9.12百分百10.21百分百asym0.82s百分之八十一1.12s百分之八十二4.99s百分之九十四7.41百分之八十一9.04百分之八十九等式0.67s百分之六十六0.84s百分之六十一4.84s 百分之九十一6.02百分之六十六6.68百分之六十五不平等0.54s百分之五十三0.71s百分之五十二3.98s百分之七十五4.40百分之四十八5.06百分之五十条纹0.53s百分之五十二0.70s百分之五十一3.94s百分之七十四4.36百分之四十八5.00百分之四十九每个等式都作为一对相反的不等式传递给图书馆。表1不同因式分解的运行时间。这些时间是使用在Fedora Linux下的2.4 GHz Core 2 Duo计算机这两个基准测试套件取自PIPS项目[1]，该项目分析循环索引之间的关系，以确定如何自动并行化或向量化Fortran循环。虽然测量只能暗示因式分解如何加速凸包计算而不是完整的分析器，但基准测试仍然具有代表性，因为它们呈现了各种程序的真实程序不变量。“PerfectClub”套件由3867个凸壳问题（简称“输入”）组成，而“Spec 95”套件由2415个输入组成。其中，由于GLPK LP工具包[11]中的精确线性规划算法进入无限循环，投影方法未能在3秒内终止，因此从我们的基准测试中省略了4个和10个样本。其余的输入需要4.28s（然而，基准套件包含144个输入，这些输入在归一化后为空。此外，当省略不对称不等式时，即那些包含仅存在于一个参数中的变量的不等式时，空输入的数量总共增加到715。一种可能的解释是，变量被添加到循环体中，使得在循环头处的凸壳的计算连接了活动变量集合所在的边。是不同的。当省略空约束集和非对称不等式时，双重描述方法仅需1.68 s和1.01 s（“双重描述”中的行“无”）。 表1的列）。 虽然这似乎是一个强有力的论据，在A. Simon/Electronic Notes in Theoretical Computer Science 267（2010）127137规范化的过程中，可以通过在循环头识别（和删除）死程序变量来这些约束集表示凸壳算法的参考输入表1中标记为“asym”的行其余的行显示了在省略越来越多的常见约束时的运行时间。我们发现帕尔马多面体库不会自动组合op-138A. Simon/Electronic Notes in Theoretical Computer Science 267（2010）127201510511 5 10 1520输入中的尺寸图三.输入中没有不对称不等式的尺寸与排除常见约束后的尺寸。每个点的面积与样本数量成正比。未显示尺寸在26和88之间的将不等式转化为等式，从而对于每个等式，可能生成比单个等式多两倍插入等式作为 等 式 约 束 导 致 了 大 约 24% 的 加 速 。 虽 然 省 略 常 见 等 式 的 增 益 现 在 较 小（ “PerfectClub” 从 1.42 秒 到 1.06 秒 ， “Spec 95” 从 0.82 秒 到 0.67 秒 ） ， 但 与Halbwachs等人相比，它仍然很重要。[8]他在识别生成器表示上的等式时没有观察到 显著 的加 速预 测 “PerfectClub” （ 从4.94s 到 4.63s ） 和 “Spec 95” （ 从 4.99s 到4.84s）的改进分别为不到7%和4%，证实了投影法分解出等式的预测是不重要的省略共同的不等式集对两种算法都是值得的，尽管双重描述方法受益更多。这种差异的原因可能在于双重描述方法中顶点集的指数增长总体而言，所提出的因子，torings的速度高达50%的凸壳算法。列观察到所有考虑的凸壳问题在投影或双描述方法中都不会导致指数爆炸，因为这些计算在原始分析器中被超时中止这导致一方面不等式和维数的数量与另一方面运行时间之间惊人的图3描述了在两个基准测试的列“asym”和“stripes”之间分解了多少变量结果表明，大多数凸壳计算都是在低维多面体上进行的。此外，保理的效率似乎差别很大凸包维数A. Simon/Electronic Notes in Theoretical Computer Science 267（2010）1271396结论我们建议以标准形式存储多面体，这使我们能够识别在连接操作期间可以省略的常见约束。我们证明了省略这些常见的约束可以加快连接操作。未来的工作应该解决其他操作是否以及如何从规范化表示中受益。例如，如果两个归一化输入多面体的等式集相同，则加宽减少到约束集的交集[4]。作者希望感谢Duong Nguyen Que使基准测试套件变得可行;也感谢LiqianChen和AntoineMin′e进行了有益的讨论，并感谢EneaZa Zaghanella对该论文早期版本的深刻评论。引用[1] Ancourt，C.，F. Coelho，F. Irigoin和R. Keryell，A Linear Algebra Framework for Static HighPerformance Fortran Code Distribution，Scienti fic Programming6（1997）。3-27号。[2] 巴尼亚拉河P. M. Hill和E. Za Zaghanella，不一定闭合凸多面体和双重描述方法，计算的形式方面17（2005），pp.222-257[3] Balas，E.，离散优化问题的析取规划和松弛族，J。代数和离散方法6（1985），pp.466-486[4] Benoy，F.，“逻辑程序设计中抽象解释的多面体域”，博士论文，计算实验室，肯特大学，坎特伯雷，联合王国（2002年）。[5] Cousot，P. and N. Halbwachs，自动发现程序变量之间的线性约束，在：程序设计语言的原则（1978年），pp。84比97[6] Galil，Z.和G. F.刘晓波，数据结构与算法，北京大学出版社，2001。监视器23（1991），pp.319-344[7] Gulwani，S.， T. Lev-Ami和M.Sagiv，A Combination Framework for Tracking Partition Sizes，在：编程语言原理（2009）。[8] Halbwachs，N.，D. Merchat和L. Gonnord，在多面体计算中减少空间维数的一些方法，形式。方法系统Des. 29（2006），pp.79比95[9] Imbert，J. L.，傅立叶消元法：选择哪一种？，在：约束编程的原则和实践，1993年，pp。117比129[10] Lassez，J.- L.和K. McCarnegie，A Canonical Form for Generalized Linear Constraints，Journal ofSymbolic Computation13（1993），pp. 1-24[11] Makhorin，A.，GLPK（GNU Linear Programming Kit）（2008），4.32版。网址http://www.gnu.org/software/glpk/[12] Refalo，P.，Approaches to the Incremental Detection of Implicit Equalities with the Revised SimplexMethod，in：Principles of Declarative Programming，LNCS1490（1998），pp. 481-496.[13] Simon，A.，[14] Simon，A. 和A. 王，分析C中的String Buffer，in：H。 Kirchner和C. 林盖森，编辑们，代数方法学和软件技术，LNCS2422（2002），pp。365-379[15] Simon，A.和A.王，利用稀疏多面体分析，在：C。汉金和我。 Siveroni，editors，Static AnalysisSymposium，LNCS3672（2005），pp. 336-351.
我的内容管理
展开
