可在www.sciencedirect.com在线获取理论计算机科学电子笔记315（2015）17-30www.elsevier.com/locate/entcs用二元模式统计合取形式的证伪次数吉列尔莫·德伊塔·卢纳FacultaddeCienciasdelaComputaci'onBenem'eritaUniversidadAut'onomadePueblaPuebla，M'exicoJ. Raymundo Marcial-Romero2，FacultaddeIngenier'ıaUniversidadAut'onomadelEstadodeM'exicoToloca，M'exicooPilar Pozos-Parra3Divisi'onAcad'emicadeInform'aticaySistemasUniversidadJu'areezAut'onomadeTabascoTabasco，M'exico乔是A。Herrna'ndez4FacultaddeIngenier'ıaUniversidadAut'onomadelEstadodeM'exicoToloca，M'exicoo摘要通过二元模式表示子句的伪造赋值集在以下方面是有用的：解决#FAL（计算合取形式（CF）的伪造赋值的数量）的算法设计。给定一个CF公式F作为输入，F由定义在n个变量上的m个子句表示，我们给出计算#FAL（F）的确定性算法。 原则上，我们的算法计算不相交的F的伪赋值的子集，直到由F定义的伪赋值的空间被覆盖。由于#SAT（F）= 2n-#FAL（F），关于#FAL的结果可以对偶地建立。 的时间计算#FAL（F）的建议的复杂性是根据F的子句数和变量数建立的。关键词：#SAT，#FAL，二元模式，枚举组合学。1电子邮件：deita@cs.buap.mx2电子邮件：jrmarcialr@uaemex.mx3电子邮件：pilar. ujat.mx4电子邮件：xoseahernandez@uaemex.mxhttp://dx.doi.org/10.1016/j.entcs.2015.06.0031571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。18G. De Ita Luna等人/理论计算机科学电子笔记315（2015）171介绍布尔公式的模型计数问题（#SAT问题）可以归结为近似推理中的几个问题例如，估计命题理论的置信度，生成命题查询的解释，修复不一致的数据库，贝叶斯推理和真值维护系统[4，12，13，14]。上述问题来源于规划、专家系统、近似推理等人工智能应用。有许多现实生活中的问题可以抽象为计算图上的组合对象例如，可靠性网络问题通常等同于图上的连通组件问题，例如，图保持连通的概率由每条边的故障概率给出，这基本上与计算边在不失去连通性的情况下可能发生故障的方式的数量相同[13]。本文讨论的组合问题是合取形式（CF）中布尔公式的模型数和伪赋值的计算，分别记为#SAT和#FAL。这两个问题（#SAT和#FAL）是经典的#P-完全问题，即使是单调和霍恩公式的限制情况。我们还表明，字符串模式可以被用来作为一个简洁的表示的一组伪造的分配合取公式。在一类P-完全问题中，SAT被认为是一个基本的例子，因为它在演绎问题中的应用，以及它在建立有效和棘手计数问题之间的边界方面1.1文献综述给定一个具有n个变量和m个子句的2-CFF，通常会分析求解关于n或m或两者的任何组合的#SAT的算法的计算复杂度[14，15]。用于解决#SAT的标准策略来自经典的Davis和Putnam（DP）方法的变体，特别是用于解决SAT问题。在这种情况下，主变式产生于在公式的赋值集上检查整个搜索树;例如，不仅当部分赋值伪造子公式时必须应用回溯过程，而且对于满足子公式的赋值也必须应用回溯过程。然而，现在d，来自D P的每个变式都具有指数时间复杂度[4，14]。在文献[6]中，考虑到F的约束图的图拓扑结构，给出了在多项式时间内计算#SAT（F）的一些情况。此外，在[5]中，提出了一种新的方法来衡量解决#SAT的困难程度。它表明，有一个阈值，由相同数量的模型，其中#SAT是在多项式时间计算事实上，由于#SAT（F）= 2n- #FAL（F），那么#SAT（F）也可以基于#FAL（F）的计算来计算。对于#SAT（F）和#FAL（F）也可以证明类似的结果。G. De Ita Luna等人/理论计算机科学电子笔记315（2015）1719i=1Mi=1I ji j ki=1计算#FAL的第一个工作是由Dubois提出的[8]。Dubois#FAL（C i<$C j）= #FAL（C i）+ #FAL（C j）− #FAL（C i<$C j）。给定2-CF F ={C1，...，C m}，基于包含-排除公式，上述用于计数不满足赋值的公式可以扩展为：#FAL（F）= |m A i|，其中每个A i是来自总数的分配的子集公式证伪Ci，则推导出以下公式：M m#FAL=|A我| −Σ|AiAj|+的 Σ|AiAjAk|+. . . +−1m−1|A我|（一）然而，最后一个包含-排除公式表示了对输入m（子句数）的指数已经设计了几个算法作为（1）的更精细或更短的版本来计算#FAL [1，2，8，3，10，11]。例如，Lozinskii [11]分析了（1）中的项集，以减少要执行的操作的数量。他发现，两个条款与oppo-现场文字确定不相交的集合伪造转让，因此他的建议包括工作的子集条款的F没有相反的文字。90年代出现的一条主线是通过计算有限的容斥公式项例如，Linial和Khan [10，3]已经表明，当仅计算（1）中的并集的某一部分的大小时，可以精确地近似已知一组交叉点。假设所有包含最多k个集合的子族的交集大小已知，如果k≥Ω（Ωm），则并集大小可以是近似的加性误差为O（exp（−（k）。Bonferroni不等式推广了包含-排除原理，证明了例如，大小至多为k的子集上的包含-排除和在k为奇数时产生总和的上界，在k为偶数时产生下界。对Bonferroni不等式的改进从这些先驱工作开始，到现在为止，还没有简洁的算法或方法来确定何时可以基于包含-排除公式的应用在多项式时间内计算#FAL。在[1]中，（1）中的项通过树探索进行排序，其中每个子集S2m都有一个节点。包含-排除公式是通过在树上搜索来执行的，对每个节点的贡献求和。对这种搜索的改进来自于观察到具有冲突子句的节点S对和没有贡献，并且S的后代永远不会对总和做出贡献。因此，通过修剪根具有冲突子句（空交集）的任何子树来优化求和。Bennett [1]寻找具有相同基数但不同符号的项的标识;因此，它们对和的相互贡献为零，这意味着20G. De Ita Luna等人/理论计算机科学电子笔记315（2015）17我我这两项都将被取消。他还将包含应用于修剪大型子树的子句中。他通过经验分析表明，包容可以大大提高基于包容-排除的模型计数的平均情况性能为了增加具有相反文字的子句对，Dubois引入了两个子句之间独立性的约化[8]。正如他所建议的，这个过程的效率取决于连续子句集之间的顺序，因为独立性约简不是交换操作。本文提出了一种关于F中子句集的增量式计算#FAL（F）的方法。我们对公式的子句进行排序，利用表示一组子句的伪造赋值的二进制字符串。为了加速#FAL（F）的计算，我们通过在子句之间应用一些约简来约简子句集合的基数;例如，独立约简规则与包含子句规则相结合的应用。我们的建议还建议应用原始对偶程序计算#SAT（F）的可能性，类似于包含-排除公式的Bonferroni不等本文的结构如下。在第2节中，我们给出了基本的符号以及几个定义。在第3节中，我们描述了基于二进制模式的方法2-CF的情况下，我们扩展这种方法CF的情况下。第4节提供了与我们的建议相关的算法。在第5节中，我们提出了工作的结论。2预赛令X ={x1，...， xn}是n个布尔变量的集合。一个文字要么是一个变量x i或取反变量x i。通常，对于每个xi∈X，x0=xi和x1=xi。子句是不同和非互补文字的析取（有时，我们也认为子句是文字的集合，例如x1<$x2={x1，x2}）。请注意，我们放弃了重言式从句的情况对于k∈IN，k-子句是由恰好k个文字组成的子句一个变量x∈X出现在子句c中，如果x或x是c的元素。一个连接形式（CF）F是一个连接的非重言式的条款。 我们说F是单调正CF，如果它的所有变量都以非负形式出现。k-CF是只包含k-子句的CF.（≤k）-CF表示一个CF包含至多k个文字的子句。一个2-CF公式F被称为严格的，只有当F的每个子句由两个文字组成。公式F的大小被定义为F的子句和变量的数量之和。我们使用Xvr（X）来表示对象X中涉及的变量，其中X可以是文字，子句或CF。例如，对于子句c={x1，x2}，则f（c）={x1，x2}。Lit（F）是F中涉及的文字的集合，即如果X=F，G. De Ita Luna等人/理论计算机科学电子笔记315（2015）1721Σnni=1n则 Lit （ F ） = X <$X ={x1 ， x1 ， . ， xn ， xn} 。我 们 表 示 {1 ， 2 ， ... ，[10][11][12][13][14][15][16][17][18][19][19][1|一|.对F的赋值s是一个函数s：n（F）→ {0，1}。赋值s也可以被认为是一组没有互补文字对的文字，例如，如果l∈s，则l/∈s，换句话说，s使l为真，l为假，反之亦然。 设c是条款和转让，如果c被满足，则c被满足，如果c被满足，则o被满足。在那另一方面，如果对所有l∈c，l∈s，则s伪c。 如果n =|（女）|，则有2可能的赋值定义在F上。设S（F）是定义在n（F）上的2个赋值的集合。设F是CF，F被赋值s满足，如果F中的每个子句都被s满足。如果F中的任何子句被s证伪，则F与s矛盾。F的一个模型是满足F的对f（F）的赋值。F的一个伪赋值是一个与F相矛盾的对F的赋值。SAT问题包括确定F是否有模型。SAT（F）表示F的模型集，则SAT（F）<$S（F）。集合FAL（F）=S（F）\SAT（F）由S（F）中证伪F的赋值组成。#SAT问题（或#SAT（F）问题）包括计算F在F上定义的模型的数量，而#FAL（F）表示F的伪造赋值的数量。因此，#FAL（F）= 2n- #SAT（F），并且#2SAT表示2-CF公式的#SAT。一个2-CFF可以用一个无向图来表示，称为F的约束图，并确定为：GF=（V（F），E（F）），其中V（F）=（F）且E（F）={{（x），（y）}：{x，y}∈F}。即GF的顶点是F的变量，并且对于F中的每个子句{x，y}都有一条边{n（x），n（y）}∈E（F）.x∈V（F）的邻域是N（x）={y∈V（F）：{x，y} ∈E（F）}，其闭邻域是N（x）<${x}，记为N[x]。变量x的次数，记为δ（x），|N（x）|F的阶为Δ（F）=max{δ（x）：x∈V（F）}. x的邻域的大小δ（N（x））为δ（N（x））=y∈N（x）δ（y）。计算#SAT（F）的算法考虑连通分量它的约束图GF。证明了约束图的连通部分集可以在线性时间内关于公式中子句因此，#SAT（F）=#SAT（G F）= k#SAT（G i），其中{G1，.，G k}是GF的连通分支集[12]。GF的连通分支集符合F的一个划分.从现在开始，我们将研究一个公式F，它只由一个连通分量表示.3通过二进制模式设F ={C1，C2，...，C m}是严格2-CF（每个子句的长度为2），令n=|（女）|.F的大小是n+m。设k是一个正整数参数，使得k2 .k的值，其中#SAT（F）=k可以在多项式时间内确定，由以下情况给出如果k= 0或k= 1，则可以应用[9]中提出的传递闭包过程22G. De Ita Luna等人/理论计算机科学电子笔记315（2015）17≥−n−2用于确定是否#SAT（F）=k。这样的过程在2-CF的大小上具有线性时间复杂度。如果k的上界是n上的一个多项式函数，例如k≤p（n），则在[5]中给出了一个精确的算法来确定何时SAT（F）=k，并且这种算法在F的大小上具有多项式时间复杂度。因此，当k > p（n）时，给出了回答#SAT（F）=k的困难情况。 在[7]中，确定了求解#SAT（F）的几种困难情况。这种识别依赖于它的子句数（m）和实例F的变量（n）之间的关系。例如，一些已证实的案例是：如果F ={C1，C2，...，Cm}是2-CF，其中n =|（女）|当m>n时，给出了SAT（F）= k的 困 难 情 形 [7]。引理3.1设F={C1，...，Cm}是2-CF，并且n =|（女）|如果F不是重言式，则#FAL（F）2或伪造赋值的个数至少为2n-2。证据设C=（li，lj）是F的子句，s是C的伪赋值.如果我们假设C不是重言式，那么<$i（li）=/<$i（lj），并且ass伪C，那么li∈s和lj∈s。因此，赋值中的n个位置中有两个位置具有固定值，并且有n2个不同的变量可以被赋予任何真值。这意味着有2n-2个可能的赋值使C证伪。因此，从2n个赋值中，2n-2被C证伪。 因此，#SAT（F）不大于2n− 2n−2。Q众所周知，对于一对子句Ci和Cj，it成立：#F AL（Ci <$Cj）=#FAL（Ci）+#FAL（Cj）− #FAL（Ci <$Cj）[8]。下面的引理显示了模型的数量何时可以减少。引理3.2设F是2-CF，n =|（女）|. 如果Ci ∈F且Cj∈ F，则ij有非互补对，但它们共享一个片（例如，Ci<$Cj/=），则S（F）证伪Ci<$Cj正好有2 n−2+ 2 n−3个赋值。证据 由于C i<$C j/=<$，因此元素A i和A j在公共文字中具有相同的值（例如，A i<$A j=<$. 100... 100... 100... n =2 ，n=3。这意味着S（F）的2n−2 + 2n−2−2n−3 = 2n−1− 2n−3个赋值是假的。Q在我们的算法建议中，我们使用了二进制模式来表示定义在n个变量上的任何子句的伪造赋值集这些模式允许我们设计计算#FAL（F）的过程令F ={C1，...，Cm}是2-CF，并且n =|（女）|.假设对f（F）的变量进行枚举，例如x1，x2，.，x n. 对于每个子句Ci={xj，xk}，设Ai是一组长度为n的二进制字符串，使得每个字符串的第j和第k位置的值，1≤jk≤n，表示xj和xk的真值，该真值伪造了Ci。 例如，在一个示例中，如果xj∈Ci，则Ai的第j个元素被设置为0。 另一方面如果xj∈Ci则Ai的第j个元素设为1。 同样的道理也适用于xk。 很容易证明，如果Ci={xj，xk}，则xj和xk在Ai的每个字符串都是F的伪造赋值。这些变量不G. De Ita Luna等人/理论计算机科学电子笔记315（2015）1723` 阿姆斯壮子句中包含的值可以取任何真值，因为子句已经被证伪了。例3.3设F ={C1，C2}是2-CF，|（女）|= 3。 如果C1={x1，x2}，C2={x2，x3}则A1={ 000， 001}且A2={ 000， 100}。我们将使用符号来表示可以在集合A i中取任何真值的变量，例如，如果F={C1，...，C m}是2-CF，n =|（女）|，C1 ={x1，x2}和C2={x2，x3}，则我们将写A1=0`0.。 . x和A2=` . 你好这是nn符号的滥用将使我们能够在本文的其余部分，考虑字符串Ai作为一个模式形成的{0， 1，}符号，并给出了一个简洁的符号表示的集合伪造转让的任何条款Ci。我们定义一个伪造字符串为一个二进制模式Ai，它表示集合伪造C i的任务。令F ={C1，...，Cm}是2-CF，n =|（女）|我们用Fals String（C i）表示构造C i的伪串（n个符号）的过程。给定一个伪字符串Ai，在Ai中出现0或1的位置称为字符串的固定值，而在A i中出现0或1的位置称为字符串的固定值。字符串中出现的符号“空”被称为字符串的自由值。我们将表示null子句的字符串定义为完整字符串：null。. .-是的n引理3.4[7]设F是2-CF，n=|（女）|.如果Ci ∈F和Cj∈F，i/= j包含一个互补的文字对，即x k∈ Ci和x k∈ Cj，则Ci和Cj的伪赋值集Ai和Aj分别形成一个不相交的伪赋值集。因此，这两个子句都恰好抑制了来自S（F）的2 n−2+ 2 n−2= 2 n−1个赋值。我们建议将以前的定义和结果推广到任何CF，然后考虑一般CF公式的#SAT和#FAL问题，而不仅仅是2-CF情况。我们现在考虑任何不限制其条款长度的CF。定义3.5[8]给定两个子句Ci和Cj，如果它们至少有一个互补文字，则称它们具有独立性。否则，我们说这两个子句都是从属的。定义3.5可以用如下的字符串伪造来表示：定义3.6给定两个长度相同的伪字符串A和B，如果存在一个i使得A[i] =x和B[i] =1−x，x∈ {0， 1}，则称它们具有独立性。否则，我们说这两个字符串是依赖的。定义3.7设F={C1，C2，···Cm}是CF。F称为独立，如果每个子句对Ci，Cj∈F，i称为依赖。j，具有独立性，否则F为24G. De Ita Luna等人/理论计算机科学电子笔记315（2015）17设F ={C1，C2，···Cm}为CF，n =|（女）|. 设C是F中的子句，x∈f（F）\f（C）是任何变量，我们有，C=（Cx）（Cx）（2）此外，这种约简保留了C相对于F的伪赋值的数量，因为#FAL（C）= 2 n-|C|2016 - 05 - 22 00：00：00（|C|01 - 02 |C|+1）= #FAL（（C<$x）<$（C <$x）），因为（C <$x）<$（C <$x）是两个独立的子句。 在伪造字符串方面，令F={C1，C2，. C m}，n =|（女）|，如果A是子句C j的伪造字符串，使得存在索引i，A [i]= 1，则伪造字符串A可以被两个伪造字符串A1和A2替换，如下所示：(i) 如果ji，则A1[j] =A[j]，如果j=i，则A1[j] = 1。(ii) 如果ji，则A2[j] =A[j]，如果j=i，则A2[j] = 0。很容易证明，由A表示的关于到F等于由A1和A2表示的伪造赋值之和相对于F.给出一对从句C1和C2.让我们假设在C1中存在不在C2中的文字，设x1，x2，.，x p是这些文字。存在一个将C2变换为与C1无关的约化，我们称这种变换为独立约化，其工作原理如下：由（2）我们可以写为：C1<$C2=C1<$（C2 <$$>x1）<$（C2<$x1）。现在C1和（C2x1）是独立的。将（2）应用于（C2x1）：C1x1）x2）x2）前三条是独立的。重复最后一个子句与前一个子句之间的独立过程，直到xp被考虑，我们有C1<$C2可以写为：C1（C2<$x1）（C2x1<$x2）. （C2 <$x p）x p）。最后一个子句包含C1的所有文字，因此可以删除它，因为它被C1包含，然后C1<$C2= C1<$（C2<$$>x1）<$（C2<$x1<$$>x2）<$. （C2 （3）第二节我们在（3）的右边得到一个独立的p+ 1子句集。让我们用伪造字符串来表示独立归约变换。给定一对伪造字符串A和B。假设有指数x1，x2，.，x p使得A [x i] = 1或A [x i] = 0且B [x i] = 0，对所有i∈ [[p]]。存在一个将B变换为独立于A的约简，我们称这个变换为独立约简，它的工作原理是用p个伪造字符串，比如B1，B2，.，来替换伪造字符串B。 B p如下：• 如果i=x1，则B1[i] =B[i]，如果i = x1，则B1[i] = 1−A [i]。• B2[i] =B[i]如果i/=x1且i/=x2，B2[i] =A[i]如果i=x1且B1[i] = 1−A [i]如果i=x2。• ···G. De Ita Luna等人/理论计算机科学电子笔记315（2015）1725Σ• Bp[i]=B[i]，如果i xj，j∈[[p]]和Bp[i]=A[i]，如果i=xj，j∈[[p−1]]，以及Bp[i] = 1−A [i]，如果i=xp。我们将两个子句C1和C2之间或它们对应的伪造串A和B之间的独立归约分别表示为：reduc（C1，C2）或reduc（A，B注意，独立归约不是可交换的，在这个意义上，reduc（C2，C1）构建了一个独立的|Lit（C2）−（Lit（C1）Lit（C2））|子句，而reduc（C1，C2）构建一个独立的|Lit（C1）−（Lit（C1）Lit（C1））|条文然而，reduc（C1，C2）和reduc（C2，C1）在逻辑上是等价的，因为它们确定了同一组伪造赋值。此外，当（Lit（C1）-（Lit（C1）<$Lit（C2）=0时，则C2的伪造赋值集是C1的伪造赋值集的子集，即FAL（C2）<$FAL（C1），然后reduc（C1，C2）=C1。包含最小子句数的独立性约简可以通过计算|Lit（C1）−（Lit（C1）Lit（C2））|和|Lit（C2）−（Lit（C1）Lit（C2））|或者如果我们通过计算索引集合{i}来伪造字符串，|A [i]= 1或A [i] = 0且B [i] = 0}且{i|B [i] = 1或B [i] = 0且A [i] = 0}。 可以选择具有最小基数的集合进行约简。对于CF中的公式，一对依赖子句至少有一个公共文本或没有公共变量设Ci，Cj是n个变量的CFF中至少有一个共同文字的两个依赖子句。设A和B是Ci和C j的伪造字符串。A和B是至少有一个公共文字的依赖项，这意味着以下条件成立：(i) 如果A[i] =x，则B[i]/= 1−x，对于所有i∈[[n]]，(ii) 存在指数xj的非空集合，使得A[xj]=B[xj]且d(iii) 有一组指数xj，使得（A[xj]=0或A[xj]=1和B[xj]=0）或（B[xj]=0或B[xj]=1和A[xj]=0）。例3.8下表显示了两个伪字符串，它们由两个具有共同文字的X1X2X3···XK···xn−1Xn伪造字符串C11**···1···**1**... 1... - -一C2*1*···1···***1*... 1... - -B应用reduc（A，B）修改字符串B如下X1X2X3···XK···xn−1Xn伪造字符串C11**···1···**1**... 1... - -一C201*···1···**01*... 1... - -B引理3.9设C i，C j是一个n元公式F中两个没有公共文字的依赖子句。这对子句的伪造赋值的数量是：|Ci|2n−|Ci|+2n−|CJ|−ii=126G. De Ita Luna等人/理论计算机科学电子笔记315（2015）17i=1i=1J证据 通过应用|C i|- 乘以C i和C j上的独立约简。Q例3.10设C i，C j∈F，其中C i=（x1<$x2）和C j=（x3<$x4）是从属子句.根据引理3.9，#F AL（Ci<$Cj）= 2n−2 + 2n−3 + 2n−4。获得独立子句的变换可以应用于 Cj 为 （ x1<$x2 ） <$ （ x3<$x4 ） = （ x1<$x2 ） <$ （ x1<$x3<$x4 ）<$（x1<$x2<$x3<$x4）。引理3.11对于任意独立公式F ={C1，.， C m}，涉及n个变量，表格，#FAL（F）=m2n−|Ci|.推论3.12如果F是独立的k-CF，则#FAL（F）=m2n-k。当FAL（F）=2n时，F是矛盾的，则所有含有至少2k个独立子句的k-CF都是矛盾的.此外，设F是CF，n =|（女）|并且F不一定是独立的公式。设C是与F的每个子句独立的子句，基于引理3.4的迭代应用，#FAL（FC）= #FAL（F）+2 n−|C|（四）然后，当已经计算了#FAL（F）时，独立约简确定计算#FAL（FC）该过程包括在C上应用独立约化以及在F中涉及变量C（C）的子句，直到我们建立一组新的子句CJ，其将与每个子句独立 Ci∈F.其中，f（C）f ff（Ci）/=f，则#FAL（FfC）=#FAL（FfCJ）= #FAL（F）+ #FAL（C）。例如，设F={{x1，x2}，{x3，x2}，{x4，x3}，{x4，x5}，{x5，x6}}。#FAL（F）可以使用F的子句的伪造字符串递增地计算。表1的矩阵表示每个子句的伪造字符串。X1 X2X3X4X5X6C111****C2*01***C3**01**C4***00*C5****00表1F中子句的伪造字符串条款C1和C2是独立的，因此这些条款之间不需要减少。子句C3与C1并不独立，甚至这对子句没有共同的文字，因此独立的归约必须应用于C1或C3。将 其 应 用 于 C 3 ，我 们 得 到 表 2 中 的 字 符 串 .现在，这四个条款是相互独立的。现在考虑C4，其伪造字符串是00。同样，它与C1不独立，应用G. De Ita Luna等人/理论计算机科学电子笔记315（2015）1727i=1X1X2X3X4X5X6C111****C2*01***C3−110*01**C3−121001**表2应用C1和C3之间的独立归约后的伪造字符串。X1X2X3X4X5X6C111****C2*01***C3−110*01**C3−121001**C4−110**00*C4−1210*00*表3应用C1和C4之间的独立归约后的伪造字符串。独立约简规则，我们得到表3的字符串。C4−11和C4−12都与C1无关。必须检查新子句是否独立于其余子句。可以注意到，新的子句C4−11与子句C2并不独立，所以重复这个过程，直到F中的每个子句都彼此独立。独立还原应用给出了表4中所示的结果。From引理3.11，#FAL（F）=102n−|Ci|=24+24+23+22+22+20+20+20+20+20= 53. 那么，#SAT（F）= 2n− #FAL（F）= 64− 53 = 11。3.1缩小CF的尺寸CF的公式的大小减少为了在应用独立减少原则的同时减少条款的数量，可以应用以下规则。包含条款规则。给定CFF的两个子句Ci和Cj，如果Lit（Ci）≠Lit（Cj），则Cj被Ci包含，然后Cj可以从F中删除。也就是说，Cj的所有满足的指派都是Ci的满足的指派：SAT（Cj）SAT（Ci）. 因此，在CF中保留Ci（包含的子句）就足够了在28G. De Ita Luna等人/理论计算机科学电子笔记315（2015）17X1X2X3X4X5X6C111****C2*01***C30*01**C41001**C501*00*C6000001颈7100001C8011100C9000000C10100*00表4应用C1和C4之间的独立归约后的伪造字符串。伪造字符串的术语。定义3.13设A和B是两个长度为n的伪造字符串。 可以说，如果存在一组索引I={i1，.，i k}{1，.，n}，使得以下条件成立：• i∈I，（A[i] = 0或A[i] = 1）且B[i]=• 其中，n∈I，j∈[n]，A[j]=B[j].包含子句规则要求将每个伪造字符串与伪造字符串表中的其余字符串进行比较，以便找到包含子句（如果存在）。这意味着在最坏的情况下O（n·m2）基本操作的顺序4#FAL的增量计算给定F（n，m）CF，算法1基于#FAL（F）的计算来计算#SAT（F）。我们从第一个子句C1∈F开始，并继续添加下面的子句，使其与前面处理的子句无关，直到F中的所有原始子句都被处理。此外，如果我们知道#SAT（F）的值，那么我们也可以确定F是否可满足。过程fixing（Ti）作用于一组伪造字符串Ti，查找表示包含子句的字符串对，以便删除对应于包含子句的字符串。过程（Ti）保持或减少字符串集合Ti的基数。由于Ti（Ti）涉及将每个伪造字符串A与Ti中的后续字符串进行比较，因此其时间复杂度为O（n·|我不是|2）。G. De Ita Luna等人/理论计算机科学电子笔记315（2015）1729∈--−----------||--∅算法1程序#伪造（F）输入：具有m个子句和n个变量的CFF输出：（True/False）=（SAT（F）=或不）（F）;删除所有包含的子句m= F; 计算新条款对于所有Ci F，inti=int i（i）;端T1=A1; 开始F的伪造字符串表对于所有i= 2到m，Ti=reduc（Ai，Ti−1）; 应用索引缩减Simplify（Ti）; 删除所有包含的子句如果（Ti有一个完整的字符串），则返回0（F如果结束，则结束Ct=证伪计数（Tm）; 计算伪造作业如果（（2nCt）>0），则返回Ct（F其他返回0（Fend if过程Count Falsifyings（Tm）计算由伪造字符串Tm的集合表示的独立子句集合的伪造赋值的数目。 计算时间为O（|T m|）.此外，函数Count Falsifyings可以在过程#Falsifying（F）的主循环的主体中执行，以检测F的子句的任何最小不可满足子集。我们的提案的总时间复杂度是关于n和大小的多项式伪造表Ti。然后，当每个新的伪造字符串Aj被处理到#Falsifying（F）的循环中时，我们必须计算集合Ti的增长大小。当然，对于|T m|是#FAL（F）本身，因为每个伪造字符串最多可以有n个固定值，并且T m中最多有#FAL（F）伪造字符串。然而，每个FAL（Ci），Ci∈F的伪串表示保证了不需要以穷举的方式表示集合FAL（Ci）。对于公式F，其伪造赋值的数量由F的大小的多项式限定，我们的算法以F的大小的多项式时间复杂度计算#FAL（F）;因此，值#SAT（F）= 2n− #FAL（F）。此外，计数证伪是一个有效的过程，当F的证伪赋值的子集由减少数量的固定变量表示到F（F）的变量集合中时，以这种方式，该子集的编码通过证伪字符串是有效的。我们的建议提出了使用原始-对偶方法计算#SAT（F）的可能性，其中#SAT（F）的计算从模型的数量到F的子句子集的伪赋值的数量振荡，根据它们之间的较小值。5结论给定一个CFF作为输入，它由定义在n个变量上的m个子句表示，我们已经给出了计算#FAL（F）的确定性算法。我们的方法是递增的，30G. De Ita Luna等人/理论计算机科学电子笔记315（2015）17F.我们使用一个简短的符号来表示使用字符串模式的子句的伪造赋值的集合。我们展示了如何操纵这样的字符串，以形成一个合取公式的伪造赋值集我们开始计算F的伪造赋值的排除子集，直到覆盖由F定义的整个伪造赋值空间。由于#SAT（F）= 2n-#FAL（F），关于#FAL的结果可以对偶地建立。为了加快#FAL（F）的计算速度，我们使用了一些约简，如包含子句和包含依赖子句的独立引用[1] 班尼特·H可满足性问题的推广结果，硕士学位论文，计算机科学。部门，科罗拉多大学，（2012年）。[2] K. Dohmen ， Improved Bonferroni Inequalities via Abstract Tubes ： Inclusion-Exclusion Type 的Inequalities and Identities，Lecture Notes in Mathematics，Springer-Verlag，（2003）.[3] 卡恩·J，Linial N.，Samorodnitsky A.，包含-排除：精确和近似，Combinatorica，卷。号164，（1996），pp.465-477[4] DahléofV.， JonssonP.， 我是M.， 用于2S AT和3S AT的计算模型，《计算机科学》，332（1-3），（2005），第265-291。[5] DeItaG.， Marcial-RomeroR.， Hern'andezJ.A.，#2SAT的P多项式解的阈值Fundamenta Informaticae，113：1（2011），pp. 63比77[6] DeItaG.，BelloP.，ContrerasM.，新多项式类为#2SAT建立通过Graph-TopologicalStructure，EngineeringLetters，Vol.15;2，Int.Assoc.ofEngineers，www.engineeringletters.com，（2007），pp. 250-258[7] De Ita G.，Marcial-Romero J.R.，Computing #2SAT and #2UNSAT by Binary Patterns，LNCS，Vol.7329 - 4th Mexican Conf. on Pattern Recognition，（2012），pp. 273-282。[8] Dubois Olivier，计数满足实例的解的数量，Theor。Comp.Sc.81，（1991），49-64.[9] 格斯菲尔德D.，皮特湖，A bounded approximation for the minimum cost 2-Sat problem，《最小成本2-Sat问题的有界近似》，《计算机科学》8，（1992），103-117。[10] Linial N.，Nisan N.近似包含-排除。Combinatorica，Vol. 10，No. 4，（1990），pp. 349-365[11] Lozinskii E.， 计数命题模型，Inf. Proc. Letters 41，（1992），pp. 327-332.[12] 罗斯·D关于近似推理的困难，Arti Ficial Intelligence 82，（1996），pp.273-302[13] Vadhan Salil P.，稀疏，规则和平面图中计数的复杂性，SIAM计算，卷。31，No.2，（2001），pp.398-427.[14] WahlströomM.， 计算2S T，LNCS，Vol.最大加权解的一个严格界5018 -参数化和精确计算：第三届国际研讨会，（2008），pp。202-213[15] 周俊平，尹明浩，周C.，以子句数为参数的#2-SAT和#3-SAT的新大小写上界，Proc.AAAI，（2010），pp.217-222
