对称性约束下的有限模型搜索及反证研究

理论计算机科学电子笔记125（2005）149-164www.elsevier.com/locate/entcs减少对称性以生成更小的SAT1张健，黄卓2计算机科学中国科学院软件研究所，北京100080摘要寻找反模型是反驳错误理论的有效方法。在一阶谓词逻辑中，模型查找是一个不可判定的问题。 但如果存在一个有限模型， 可以通过穷举搜索来找到它。一阶逻辑中的有限模型生成问题也可以转化为命题逻辑中的可满足性问题。 但是直接翻译可能不是很有效。本文讨论了如何考虑对称性，使问题变得简单。提出了一种静态添加约束的方法，该方法可以看作是最小数目启发式算法（LNH）的一种近似。文中还描述了一种动态方法，它要求一个类似SEM的模型证明器生成一组部分模型，然后将每个部分模型交给一个命题证明器。对这两种方法进行了分析和比较。保留字：有限模型搜索，可满足性，对称性，最小数目启发式1介绍与定理证明相比，伪命题的证伪问题研究较少。但它实际上是非常重要的，因为对于开放问题，你不知道猜想是否成立。如果你给一个典型的基于解析的定理证明器一个错误的猜想，证明器要么永远运行，要么终止，不产生任何有用的信息。当这个1国家杰出青年科学基金资助项目（No.60125207）和K.C.黄氏教育基金会（香港）。2 电子邮件：zj@ios.ac.cn，hz@ios.ac.cn1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.07.023150J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）149如果你不知道这是因为猜想是假的，还是因为推理规则不够，或者证明者不是那么有效。一个有效的方法来反驳这样的命题是找到一个合适的反模型，即一个公理模型，其中所有的前提成立，但猜想不成立。然而，对于一阶谓词逻辑，确定模型的存在性通常是一个不可判定的问题。 幸运的是，在许多情况下，满足公式的有限模型是存在的，我们可以首先尝试找到一个有限模型。如果我们成功了，这个猜想就会被反模型反证;但是如果我们失败了，一般来说，我们不能说这个猜想是假的或真的。目前，在一阶逻辑中，近似有两种主要的方法来生成有限模型。第一种方法将问题转化为命题逻辑中的满足性（SAT）问题，并使用SAT算法（例如，DPLL算法）来求解它。例如，参见[6，8，1，5]。第二种方法将问题视为约束满足问题，并使用回溯搜索直接找到函数/谓词的解释像FINDER [11]、EQUIPCON [14]、SEM [16]和Mace4 [9]这样的工具都是基于这种方法的。Gandalf [13]实现了这两种方法。上述两种方法都有一些优点和缺点。例如，翻译方法可能生成太多的命题公式，并且约束求解（或直接搜索）方法在某些问题上可能不是那么有效。但是使用一阶子句直接导致了更大的推理步骤，也给了我们消除对称子空间的机会。我们一直在研究如何将这两种方法结合起来。一种方法是通过采用SAT社区开发的成功技术来改进直接搜索程序[4]。或者，我们也可以通过将其与一阶模型搜索器相结合来改进翻译方法[15]。本文比较了在问题具体化中利用对称性的不同方法，从而使得到的SAT问题实例更容易。文中给出了一些实例和实验结果本文的结构如下。在下一节中，我们将回顾一些基本概念和符号，以及两种模型发现方法在第3节中，我们给出了一个例子来说明减少对称性的重要性。然后，我们提出了两种方法来添加约束的原始问题，以获得更容易的命题问题的实例（S）。第一个是静态的，只生成一个实例;第二个是动态的，通常生成多个实例。并举例说明了它们的优缺点。J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）1491512有限模型搜索有限模型生成问题可以表述如下。给定一组一阶公式和一个非空的有限域，找到公式中出现的所有函数符号和谓词符号的解释，使得每个公式在这个解释下都是真的。这种解释被称为模型。通常我们还假设公式都是子句，并且子句中的每个变量都（隐式地）泛量化。本文不考虑多类公式。在 不失一般性的情况下，假设n元域为Dn={0，1，.，n−1}。 布尔域是{0，TRUE}。如果每个函数/谓词符号的arity最多为2，则有限模型可以方便地由一组乘法表表示，每个函数/谓词一个例如，子句f（x，x）=x的3元素模型如下所示F012001011102012这里f是一个二元函数符号，它的解释由上面的二维矩阵给出。矩阵中的每一项都称为一个单元格。有限模型生成问题可以转化为命题满足性问题。一个模型可以用一组命题变量的赋值来表示。假设有m个单元（c0，c1，...， cm−1）in函数的乘法表。 我们可以引入mn命题变量：p ij（0≤i< m，0≤j< n），其中p ij为真，当且仅当第i个单元格c i具有值j。此外，我们还需要为谓词乘法表中的每个单元格提供一个命题变量第一阶子句可以相应地翻译成命题子句。有关更多详细信息，请参见例如[6，8]。或者，我们也可以直接搜索单元格的值有限模型生成问题也可以被视为约束满足问题（CSP），这已经被许多研究人员在人工智能中研究CSP的变量是单元项，即，基础项如f（0， 0）和f（0， 1）。每个变量的定义域是Dn（谓词除外，其定义域是布尔定义域）。约束是输入子句的基础实例的集合目标是找到对单元格的一组分配f（0， 1）= 2），使得所有的基础子句成立。152J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）149通常使用回溯搜索来解决上述问题。搜索过程的基本思想大致如下：重复扩展部分模型（用P mod表示），直到它成为一个完整的模型（其中每个单元都得到一个值）。初始P mod为空。P mod通过选择一个未赋值的单元格并尝试为其找到一个值来扩展。当然，当没有适合该单元格的值时，需要回溯，Pmod会变小。这样的过程可以被描绘为搜索树。树的每条边对应于为某个单元格选择一个值如引言所述，翻译方法和直接搜索方法各有优缺点。命题满足性（SAT）问题已经研究了40多年。人们已经得到了许多理论结果，并设计了许多有效的算法近年来，越来越多的高效SAT求解器被开发出来，如zCha [10]和BerkMin [3]。另一方面，直接搜索方法适用于一阶子句，并且可能使用一些结构信息来加速搜索过程。一种已被证明非常有用的技术是所谓的最小数启发式（简称LNH）[14，16]。它是基于这样的观察，在典型的基准问题，大多数领域的元素是“等价”的因此，我们只需要选择几个代表性的值来分配给单元格，并且可以修剪搜索树的许多分支。LNH在搜索树的前几层更有效。在许多问题上，它可以显着减少搜索空间，但开销可以忽略不计。相反，很少有好的方法来发现和使用命题子句中的对称性。结合这两种方法的好处当然是可取的，这样就可以容易地解决更多的问题3一个激励的例子让我们看一个例子，即，求正交格[7]。公理（和引理）如下：m（x，y）= m（y，x）.j（x，y）=j（y，x）. j（j（x，y），z）=j（x，j（y，z））。c（c（x））=x.j（x，m（x，y））= x.m（x，y）= c（j（c（x），c（y）. m（x，x）=x.j（x，x）=x.J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）149153j（c（x），x）=1.m（c（x），x）= 0.j（1，x）=1.j（x，1）=1。m（1，x）= x.m（x，1）= x.m（0，x）= 0.m（x，0）= 0.j（0，x）=x.j（x，0）=x.当被要求找到上述公式的13元素模型时，MACE 2.2 [8]需要9.34秒才能得出这样的模型不存在的结论。大部分时间都花在SAT解题上，而不是获得命题子句（DPLL时间：9.09秒）。如果我们在输入中添加以下两个子句：c（0）= 1。 c（2）= 3。执行时间将是1.14秒（DPLL时间：0.89秒）。减少是很重要的。实验在戴尔台式计算机（Optiplex GX 270，Pentium 4，2.8GHz，2G存储器）上进行。上述两个条款代表SEM采取的最初两个步骤[16]。注意，在第一步中，只有一个分支，即，SEM决定只能将值1分配给c（0）。同样，在第二步中，也有一个选择。因此，增加这两个子句并不改变原问题的可满足性。4添加公式以消除对称性Fujita等人在解决拟群问题时， [2，12]增加了一些条款，消除了相当多的对称子空间。这大大缩短了搜索时间。但是附加的约束是特定于域的，也就是说，它们只能应用于拟群问题和其他类似的问题。MACE [8]有一个选项（这在寻找反例时很有帮助，因为对猜想的否定通常包含Skolem常数。例如，它在寻找非交换群时也很有用。但是，该选项可能会错过一些解决方案，其中两个常量被分配相同的域元素。例如，当使用此选项时，MACE未能找到一个10元素反模型，该模型表明某些方程（即，[7]中的方程E1）对于正交格不成立。MACE有另一个选项（154J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）149生成的命题公式。 但它只适用于常数。LNH是一种更通用的方法。我们可以通过添加某些约束来模拟它。这种静态对称性约简在Partial中实现。参见[1]的第6节。在SAGE中采用了类似的方法[5]。为了简单起见，我们假设输入中没有域元素，并且只有一个二元函数符号f。 SAGE增加了以下内容约束（用Cf表示）：f（0，0）=0|f（0，0）=1。f（0，1）=0|f（0，1）=1|f（0，1）=2.f（1，0）=0...|f（1，0）=1|f（1，0）=2|f（1，0）=3.它可以极大地修剪搜索树，因为我们现在只需要检查f（0，0）的2个（而不是n个）值，f（0，1）的3个（而不是n个）值，.为了理解它的有效性，让我们看看QG5问题。它只有一个二元函数符号除了这个属性，它还有以下公理：f（x，x）=x. f（f（y，x），y），y）=x.f（y，f（f（x，y），y））=x.f（f（y，f（x，y）），y）=x.假设我们试图找到它的所有模型。如果我们不使用任何消除同构的方法，则有120个尺寸为7的模型和720个尺寸为8的模型。如果我们将上述三个Cf公式添加到输入中，则有24个尺寸为7的模型和24个尺寸为8的模型。但是当我们使用LNH时，只有一个7号的模型和一个8号的模型从这个简单的例子中，我们可以看到，该方法是有帮助的，但它还不够好。4.1更精确的模拟Cf约束只是LNH的近似实际上不需要考虑某些例如，当f（0，0）= 0和f（0，1）= 1时，我们不需要考虑f（1，0）= 3的情况。最近，我们实现了一种新的策略，它为生成的SAT实例添加了更多的约束。有两种约束，分别用C1和C2表示。我们添加它们，同时对于一元函数g，我们按以下顺序访问单元格：g（0）， g（1）， g（2），.J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）14915544444int i（inti）/* 处理单元格ci */{更新集合S1和S2，计算集合S4和S5;J=S4;if（S5有多个元素）{/* 元素是对称的 */设v是S5中的最小元素;增加约束条件C1（i）;S3 {v}=S3{v};J=SJ<${v};}如果（S，J有多个元素）{增加约束条件sC2（i）;}}Fig. 1. 添加约束以缩小搜索空间对于二元函数f，我们按以下顺序访问单元格f（0，0），f（0，1），f（1，0），f（1，1），f（0，2），.假设我们正在访问单元格ci。 我们使用图1中的过程来添加约束。它涉及以下几组域元素：• S0：出现在输入公式中的域元素集。• S1 ={c k的参数|0 ≤k≤ i}。• S2=S0<$S1。它包含了被区分的元素（即，不与其它元件对称）。•S3：被选择作为“未使用”元素的代表的域元素的集合•S4= S3-S2 我们还使用了一个密切相关的集合SJ。• S5=Dn−（S2<$S3）。除S0外，其他集合都是动态变化初始i= 0，集合S3为空。C1（i）由以下约束组成：j∈S2< $S3<${v}（ci=j）;c i/= k，对于每个k∈S5− {v}。SS156J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）14944C2（i）由以下约束C2（i）（a，b）组成：（cjJ Iaabcjb）、 → c i/= b对于每一对a，b∈SJ（ab）.在该过程中，集合S5减小。当S5只有一个元素时或者它是空的，我们不添加C1约束。同样，当SJ没有超过1个元素，我们不添加C2约束。 当这两个如果发生，则可以终止该过程。在附录中，我们将证明该方法是正确的。4.2例如现在我们来看一个例子，即，找到一个6元素组。公理是以下子句：f（x，0）= xf（0，x）= xf（x，g（x））= 0f（g（x），x）= 0f（x，f（y，z））=f（f（x，y），z）其中0是特殊域元素（即，一个组的单位元素为了添加约束以消除对称子空间，SAGE按以下顺序访问单元：f（1，1），f（1，2），f（2，1），f（2，2），f（1，3），f（3，1），f（2，3），f（3，2），f（3，3），...注意，f前两个都已经被确定了（因为前两个公理）。以下是C1约束：f（1， 1）= 0<$f（1， 1）= 1<$f（1， 1）= 2; f（1， 1）/= 3; f（1， 1）/= 4; f（1， 1）/= 5;f（1， 2）= 0<$f（1， 2）= 1<$f（1， 2）= 2<$f（1， 2）= 3;f（1， 2）= 4;f（1，2）= 5;f（2， 1）= 0<$f（2， 1）= 1<$f（2， 1）= 2<$f（2， 1）= 3<$f（2， 1）= 4;f（2，1）/= 5;J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）149157f（2，2）= 0 <$f（2，2）= 1 <$f（2，2）= 2 <$f（2，2）= 3 <$f（2，2）= 4 <$f（2，2）= 5.158J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）149以下是C2约束：f（1， 2）/= 3 （1， 2）/= 4 → f（2， 1）/= 4f（1， 2）/= 3<$f（1， 2）/= 4<$f（2， 1）/= 3<$f（2， 1）= 4 → f（2， 2）/= 4f（1， 2）/= 3 （1， 2）/= 5 n（2， 1）/= 3 n（2， 1）/= 5 → f（2， 2）/= 5f（2， 1）/= 4<$f（2， 1）/= 5→ f（2， 2）= 5f（2， 1）/= 4<$f（2， 1）= 5<$f（2， 2）/= 4<$f（2， 2）/= 5 → f（1， 3）= 5f（2， 1）= 4<$f（2， 1）= 5<$f（2， 2）/= 4<$f（2， 2）/= 5<$f（1， 3）/= 4<$f（1， 3）/= 5→ f（3， 1）/= 5f（2， 1）/= 4<$f（2， 1）/= 5<$f（2， 2）/= 4<$f（2， 2）/= 5f（1， 3）= 4 → f（2， 3）/= 5f（2， 1）/= 4<$f（2， 1）/= 5<$f（2， 2）/= 4<$f（2， 2）/= 5（1， 3）/= 4 f（1， 3）/= 5f（2， 3）= 4f（2， 1）/= 4<$f（2， 1）/= 5<$f（2， 2）= 4<$f（2， 2）/= 5（1， 3）/= 4 f（1， 3）/= 5<$f（2， 3）/= 4<$f（2， 3）/= 5<$f（3， 2）/= 4<$f（3， 2）= 5→ f（3，3）= 5请注意，已经进行了一些优化例如，f（1， 1）/= 3不会出现在第一个公式中，因为C1约束将f（1， 1）的值限制在集合{0，1，2}中。如果我们不使用额外的约束来消除对称性，我们将找到80个模型。如果我们在生成命题分句时加入C1约束，则会得到16个模型，如果同时加入C1和C2约束，则只会得到9个模型。在这里，我们给出了两个模型的群论时产生的C1约束作为附加的约束，但不产生时，C1和C2约束都使用。第一个定义如下：F0123450 1 2 3 4 50012345G0 1 4 5 2 311032542235401332451044501325541023此模型被删除，因为C2包含约束：f（2，1）/= 4 <$f（2，1）= 5 → f（2，2）= 5。J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）149159第二个定义如下：F0123450 1 2 3 4 50012345G0 2 1 3 4 511205342201453334501244532015534120原因是C2包含约束：f（2，1）= 4 <$f（2，1）/= 5 <$f（2，2）= 4 <$f（2，2）/= 5 →f（1，3）= 5。现在我们将组的大小增加到10。如果我们只使用C1约束，则有近1000个模型;但是如果我们同时使用C1和C2约束，则模型的数量减少到11个。5动态生成多个SAT试题集如第2节所述，回溯搜索方法通过扩展部分模型来工作。还提到LNH在搜索树的前几层更有效。低于一定的水平，领域元素不再是“等价的”和启发式是无效的。另一方面，对于许多问题，命题推理在搜索树的大多数节点上更有效自然，人们可能会想到将一阶模型搜索与SAT求解相结合，如第3节中的示例所示。在[15]中，我们提出了一种结合这两种方法的方案，并报告了SEM和MACE的一些经验。该方案如下所示：/的。\// \/的。\中找到。/\/\.\中找到。 .. \中找到。坐在搜索的前几个级别，我们使用SEM和LNH。低于某些水平（例如，当每个域元素是不同的时），搜索被转移到SAT求解器。边界线可以由用户决定。160J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）149表1各种问题大小78910111213QG5115122670217OL23548496501>10000>10000>10000NCG716315779223210让我们再看看QG5的问题。它的公理在前一节中给出。对于这个问题，SEM搜索树的前3步如下：f（0，1）=2; f（2，0）=3; f（2，1）=4。在每一步，SEM使用LNH并通过各种推理得出结论，只有一个值可以分配给相应的细胞。如果我们将这三个方程添加到输入中，并要求SEM找到所有模型，而不使用LNH，SEM将发现有2个尺寸为7的模型，6个尺寸为8的模型。这与最佳数量（1个7号模型和1个8号模型因此，增加上述约束对于消除同构子空间是非常有帮助的。当然，我们可以要求SEM超越这三个步骤，可以消除更多的子空间。通常，使用这种方法生成多个SAT实例。有任何开销吗？是的主要的开销将是翻译时间（从一阶子句获得命题子句的时间），也许还有读/写文件。如果生成了许多SAT实例，这将是非常重要的。另一方面，如果问题是困难的，SEM的搜索树的节点不是那么多，并且大部分工作将被完成一个SAT solver。翻译的时间并不多，如果与搜索时间相比。在这种情况下，组合将非常有帮助。我们稍微修改了SEM，以便当LNH 不再有效（即，当没有域元素是“等价的”时）。我们要求修改后的程序计算它生成了多少个部分模型。表1给出了SEM在几个问题上生成的部分模型的数量除了前面提到的QG5和正交格（OL）之外，我们还在非交换群（NCG）问题上测试了该程序。表格的第一行给出了模型的大小，而其他行给出了部分模型的相应数量。我们可以看到，对于NCG和QG5，没有太多的部分模型。但是OL有很多部分模型。这可能是因为这个问题太简单，或者有太多的解决方案。J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）149161我们还尝试了其他几个问题。有些太容易，有些太难。例如，当模型的大小为6时，组合逻辑问题cl_BM对于SEM已经是相当困难的。因此，结果未包含在上表中。当大小为6时，生成1599个局部模型;当大小为7时，生成49438个局部模型减少部分模型数量的一种方法是要求SEM更早地当仍然存在一些“等效”域元素时）。但是这样一来，对称性就没有得到充分利用。另一种方法是要求SEM解决更简单的子问题，其中许多单元格都被赋值。如果我们只寻找一个模型，就没有必要生成所有的部分模型。在这种情况下，将SEM与SAT求解器更紧密地结合起来将是有益的，如[15]所做的那样。然后，一旦一个部分模型导致一个完整的模型，SEM可以被终止，并且不需要生成更多的部分模型。6总结发言由于近年来开发了许多高效的SAT求解器，使用它们来寻找一阶逻辑中的有限模型和反例变得更加有趣。如果我们在生成命题子句时考虑对称性，则可以获得更容易的SAT实例在本文中，我们讨论了两种不同的方法。第一个是静态的，它将一些公式添加到输入中，然后以传统的方式获得一组命题子句。只生成一个SAT实例。我们提出了一个程序添加的公式，这是一个近似的最少数量的启发式。它通常可以消除许多同构模型，并使生成的SAT实例更容易。第二种方法是动态的，它使用一阶模型迭代来导出一些部分模型，然后得到一些SAT实例（每个实例对应于一个部分模型）。相对而言，这种方法通常可以消除更多的同构模型。但对于某些问题，可能会有太多的局部模型。给出了一些例子，并报告了实验结果，使用现有的工具（或它们的变化）。我们相信，一阶模型搜索和SAT求解的结合对于寻找大型模型和反例非常有前途162J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）149引用[1] K. ClaessenandN. S？r en son，N ewtechniqu ethatim p r oveMACE-stylef it em od ef i n g.见：模型计算-[2] M. Fujita，J. Slaney和F. Bennett，自动生成有限代数中的一些结果，Proc. 13th[3] E. Goldberg 和 Y. Novikov ， BerkMin ： A fast and robust SAT solver ， Design ，Automation，and Test in Europe（Date[4] Z. Huang，H. Zhang和J. Zhang，通过命题推理和引理学习改进一阶模型搜索，Proc. 第七届 理论和应用的可接受性测试，2004年。[5] Z. Huang和J. Zhang，从一阶公式生成SAT实例，J. ofSoftware。[6] S. Kim和H.张文龙：基于模型生成的定理证明，第12届美国人工智能学会学术会议论文集，162[7] W. McCune，一些正交格恒等式的自动证明和反例Information Processing Letters，65（6）：285[8] W. McCune，MACE 2.0参考手册和指南，技术备忘录ANL/MCS-TM- 249，Argonne国家实验室，Argonne，IL，USA，2001年。[9] W. McCune，Mace4参考手册和指南，技术备忘录第264号，Argonne国家实验室，Argonne，IL，USA，2003年。[10] M.陈文辉，高智晟：一种新的计算机辅助设计方法，国立成功大学计算机工程研究所硕士论文，2001年[11] 林志荣，有限域计数器-[12] J. Slaney，M. Fujita 和M. Stickel ，Automated reasoning and exhaustive search：automatedreasoning and exhaustive search：群存在问题，计算机和数学与应用29（2）：115[13] T. Tammet，有限模型构建：改进和比较。见：模型计算-[14] J. Zhang ，Constructing finite algebras withJ. Automated Reasoning，17（1）：1-22，1996。[15] 张军，结合SAT的自动对称破缺方法，美国计算机学会学术会议论文集。应用计算机，17 -2 1 ， 2 0 0 1 。[16] J.Zhang和H.张文龙：一种用于模型计数的系统，第14届IJCAI会议论文集，298-303，1995。J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）149163阑尾静态方法我们将证明增加C1和C2约束不会改变满足性。让SC 1（m）= C 1（0） 1（m）SC2（m） = C 2（0）型... 2（m）我们用P表示原始问题，并试图证明以下引理：(a) 倘P_SC1（0）及P_SC2（0）均为满意，则P为满意。(b) 如果P_SC1（m+ 1）_SC2（m）满足，则P_SC1（m）_SC2（m）满足。(c) 如果PΔSC1（m+ 1）ΔSC2（m+ 1）满足，则PΔSC1（m+ 1）ΔSC2（m）满足。对于每个引理，我们只需要证明一个方向（即，“如果”部分）。我们假设集合C1（i）不是空的，对每一个i。（a）的证明：假设P是可满足的，并且有一个模型M。设v0是M中单元格c0的值。当访问c0时，S3和S4都是空的。C2（0）。因此，我们只需要考虑C1（0）。假设过程addCons（0）为c0选择值v。如果v0∈S2<$S3或v0=v，则M将满足C1（0）。 否则，我们可以将置换σ={v，v0<$}应用于M，并得到σ（M）。由于v和v0都不出现在P的输入规范中，所以σ（M）也是M的模型。在这个模型中，c0的值是v，并且满足C1（0）。 综上所述，P-SC1（0）-SC2（0）是令人满意的。证明（b）：假设P<$SC1（m）<$SC2（m）是可满足的，并且有一个模型M。设vm+1是M中单元cm+1的值。假设过程addCons（m+1）选择cm+1的值v。若vm+1∈S2<$S3或vm+1=v，则满足C1（m+ 1），且M是P<$SC1（m+1 ） <$SC2 （ m ） 的 模 型 . 否 则 ， 我 们 可 以 在 M 上 应 用 置 换 σ={v_v ，v_m+1_v}，得到σ（M）。由于v和 vm+1都不出现在P<$SC1（m）<$SC2（m）中，所以σ（M）也是P<$SC1（m）<$SC2（m）的模型。 在σ（M）中，cm+1的值为v。所以σ（M）是P<$SC1（m+1）<$SC2（m）的模型总的来说，P≤SC1（m+ 1）≤SC2（m）是令人满意的。证明（c）：假设P<$SC1（m+1）<$SC2（m）是可满足的。我们需要证明增加约束C2（m+1）不会改变可满足性。我们将约束条件C2（m +1）（a，b）按a，b的升序排序. 用cl0，cl1，.表示它们海峡令VC ={c ，j|0≤j≤m}，即， 已经处理过的细胞。我们试图证明以下几点：（c1）如果P<$SC1（m+1）<$SC2（m）满足，则P<$SC1（m+1）<$SC2（m）<$cl0是满意的。164J. Zhang，Z.Huang/Electronic Notes in Theoretical Computer Science 125（2005）14944(c2)对任意i≥ 0，若P<$SC 1（m + 1）<$SC 2（m）<$cl0<$. 满足，则P<$SC1（m + 1）<$SC 2（m）<$cl0<$.. cli证明（c1）。假设P<$SC1（m+1）<$SC2（m）是可满足的，并且它有一个模型M。令S6表示已经被分配给V C中的某个单元的域元素的集合，即， {c j在M中的值|0 ≤ j ≤ m}。假设cl0是C2（m+ 1）（a，b）：其中a，b∈SJ（c j/= a<$c j/= b）→ cm+1/=b，cj∈ V C和一个b。• 如果a∈S6或b∈S6，这意味着VC中的一个单元格被赋予了值a或b。所以cl0在M中成立。• 如果cm+1没有被赋值为b，则cl0也将在M中保持。• 以上两点都不正确。 然后我们可以应用置换σ={a，b}到M，得到σ（M）。置换不会改变V C中任何单元格的值。此外，a和b不出现在P的输入规格中，因此σ（M）是P<$SC1（m+1）<$SC2（m）的模型。 在这个模型中，cm+1的值是a，它不同于b.所以cl0成立。因此P≠SC1（m+ 1）CSC2（m）CSCl0是令人满意的。证明（C2）。设P<$SC 1（m+1）<$SC 2（m）<$cl0<$. i是满足的，它有一个模型M。令S6表示已经被分配给V C中的某个单元的域元素的集合，即，{c j在M中的值|0 ≤j≤m}。考虑约束cli+1：其中a，b∈SJ（cj/=acjcj∈ V C和一个b。b) →cm+1b，• 如果a∈S6或b∈S6，这意味着VC中的一个单元格被赋予了值a或b。所以cli+1在M中成立。• 如果cm+1没有被赋值为b，则cli+1也将在M中成立。• 以上两点都不正确。 然后我们可以应用置换σ={a，b}到M，得到σ（M）。置换不会改变V C中任何单元格的值。此外，a和b不出现在P的输入规格中，因此σ（M）是P<$SC1（m+ 1）<$SC2（m）的模型。在这个模型中，cm+1的值是a，它不同于b.所以cli+1成立。由于a

下载后可阅读完整内容，剩余1页未读，立即下载