人工智能基础：可满足问题中的模型计数

第7卷第1期 智能系统学报 Vol.7 No.1 2012年2月 CAAI Transactions on Intelligent Systems Feh.2012 D0I:10.3969/i.issn.16734785.201107008 网络出版t地址：htp://www.cnki.net/kcma/detail/23.1538.TP.20120217.1520.001.html 可满足问题中的模型计数 谷文祥，朱磊，黄平，殷明浩 (东北师范大学计算机科学与信息技术学院，吉林长春130117) 摘要：模型计数问题是指计算给定问题的解的个数，这是一类比决策更困难的问题，也是人工智能领域研究的一 个热点问题.对模型计数问题的研究不仅可以提高算法的求解效率，更能促进对问题困难本质的了解.以可满足问 题（命题可满足(SAT)和约束可满足问题(CSP))为例，从精确算法和近似求解两方面综述了模型计数问题的研究现 状，重点介绍了相关概念以及各个算法之间的优缺点，并提出了有待解决的开放性问题，对模型计数问题的研究予 以了总结和展望. 关键词：人工智能：约束可满足问题：命题可满足问题：模型计数 中图分类号：TP18文献标识码：A文章编号：16734785(2012)01003307 The model counting of a satisfiability problem GU Wenxiang,ZHU Lei,HUANG Ping,YIN Minghao (School of Computer Science and Information Technology,Northeast Normal University,Changchun 130117,China) Abstract:A model counting problem refers to computing the number of solutions for a given problem which is har- der than the decision-making problem.Model counting problems are also a hot topic in the field of artificial intelli- gence.Research on model counting problems can not only improve the efficiency of an algorithm,but also enhance the understanding of the nature of hard problems.Taking a satisfiability problem in propositional logic,known as an SAT,and a constraint satisfaction problem (CSP)as an example,a model counting problem was reviewed from two aspects:an exact algorithm and approximate algorithm.For each aspect,the development and related concepts a- long with the advantages and disadvantages were emphasized.Moreover,this paper proposed some unsolved ques- tions of the model counting and gave a summary and outlook of the research on model counting. Keywords:artificial intelligence;constraint satisfaction problem;propositional satisfiability problem;model counting 命题可满足问题(propositional satisfiability prob- 问题对人工智能的很多领域都有着深远的影响，许 lem,SAT)的求解是近年来人工智能领域研究的热 多的概率推理如贝叶斯网络推理)]等都可以转换 点问题，这类问题的计算复杂度是属于NP完全 为模型计数问题2].另一个应用是组合问题，计算 的山，也即意味着如果P≠NP成立，即无法在多项 解的个数能够更深入地了解问题的本质.对于组合 式时间内解决SAT问题.而模型计数问题是比这类 这样的问题，即使找到一个解都是困难的，搜索整个 决策问题更难解决的问题，它的计算复杂度是属于 解空间的模型计数问题的时间复杂度更是巨大的. #P完全的.一些原本是多项式时间的决策问题的模 这也就使得目前模型计数算法能解决问题的规模与 型计数也是属于#P完全的，例如2SAT21.模型计数 决策性算法相比相差了好几个数量级.对于模型计 问题是指计算给定问题的解的个数，即使得公式值 数问题，目前确定性算法能够解决的问题的变量数 为真的不同的变量的赋值数.高效地解决模型计数 约为几百个，近似算法能解决的问题的变量数约为 1000个. 收稿日期：201107-25.网络出版时间：2012-02-17 基金项目：国家自然科学基金资助项目(61070084,60573067,60803102) 约束可满足问题(constraint satisfaction problem, 通信作者：黄平.E-mail:huan218@nenu.edu.cm. CSP)是SAT问题的一种泛化，当CSP问题中变量

·34 智能系统学报 第7卷 的取值为布尔值时，CSP问题就退化为普通的SAT 定义5（约束图，Gx)给定一个命题逻辑公式 问题.CSP问题的多值使得其在实际生活中有着更 F,F的约束图Gp的定义如下： 加广泛的应用，如图着色问题就是一种特殊的CSP 1)G中的顶点为F中的变量； 问题，而规划问题也可以转换为动态CSP问题求 2)若F中的2个变量出现在同一个子句中，则 解.CSP问题的模型计数(#CSP)方法大部分都是由 在这2个变量所对应的顶点连上边， 求解SAT问题的模型计数(#SAT)方法扩展而来 约束图中的顶点表示原问题中的变量，而边表 的，因此CSP问题的求解也可分为2类：精确算法 示变量之间的约束，问题的约束越多，则图的结构越 和近似求解.精确算法主要是以DPLL算法和局部 紧密 搜索为基础，与决策问题只要找到一个可满足解不 同，模型计数问题需要搜索整个解空间，因此算法的 2SAT中的模型计数 时间复杂度是巨大的.近似求解一般采用采样的方 SAT问题是CSP问题的特殊实例，即SAT问题 法来避免搜索整个解空间，利用局部解的数目来估 是域大小为2的CSP问题，相较于一般的CSP问 计整个空间解的个数.这样使得算法的时间复杂度 题，SAT问题的模型计数比较简单，下面首先介绍有 有了很大的改善，但是所得到解的数目却不再是精 关SAT问题的模型计数方法， 确的.本文将从以上2个方面分别介绍#SAT和 2.1精确算法 CSP问题求解算法的发展、相关概念以及算法的优 目前求解模型计数的方法有2种，即精确算法 缺点，并对模型计数问题的求解方向进行展望. 和近似求解.本文先介绍#SAT中主要的精确算法， 然后给出典型的近似求解方法， 1 相关概念 2.1.1CDP算法 本文讨论的模型计数问题都是基于SAT问题 Valiant在1979年证明了模型计数问题是属于 和CSP问题的.在介绍具体的算法之前，首先介绍 P完全的2]，即这是一类比NP问题更困难的问 一些与模型计数有关的定义 题.Dubois在1991年给出了一种求解SAT问题模 定义1（命题可满足问题，SAT) 给定一个命 型个数的方法，并且证明了时间复杂度为O(m@), 题逻辑公式F,其变量集为V=var(F),是否存在对 其中n为变量数，m为子句数，a是多项式y- 其变量集V的一个真值赋值，使命题公式F成立 y-1-…-1的正根，k为子句的长度4.Zhag在 (可满足)，如果成立则返回这些变量真值赋值. 1996年也给出了基于类似思想的算法，时间复杂度 定义2（命题可满足问题的模型计数，#SAT) 也近似相等5).虽然他们的算法都能够得到问题的 给定一个命题逻辑公式F,其变量集为V=var(F), 解的数目，但是当问题规模增大时，算法的时间复杂 计算使得公式值为真的变量集V的赋值的个数，并 度几乎是呈指数级增长，当k趋于无穷的时候， 返回这个值， ak=2.Birnbaum和Lozinskii在1999年提出了基于 定义3（约束可满足问题，CSP)CSP问题可以 SAT求解器DPP的CDP6,该方法不论是算法的复 描述为一个三元组P(X,D,C),其中X是有限变量 杂度还是时间复杂度上较前面的2个方法都有很大 集合{X1,X2,…,X.},D为与X中变量对应的域值 的改善.CDP(F,n)算法的基本框架如图1. 集合{D1,D2,…,Dn},C是有限约束的集合，用于限 F1={C-}1C∈F,lC}, 制变量的取值.一个CSP问题就是找到一个满足约 F2={C-{x}IC∈F,x年C}, 束C的变量集X的取值 F3={C-{x}|C∈F,x使C}. 定义4（约束可满足问题的模型计数，#CSP) 式中：l为单元文字，x为分支变量. 给定一个CSP问题P,计算所有使得P中约束满足 算法的输入参数为公式F和变量数n.首先判 的变量集的取值数目，并返回这个值。 断公式是否为空，如果是，则表示公式已经被满足， 由上面的定义可知，决策性问题可以看作模型 所以返回解的个数为2”；反之公式若包含了空子 计数问题的一种特殊情况.决策性问题只需找到一 句，则肯定不满足，返回0；若公式中有单元子句，则 个可满足的解，而模型计数问题则要求找到问题的 先对单元子句进行处理以简化公式，否则随机选释 所有解。 个变量进行分支，分支后公式求得模型的总个数 在实际问题求解的过程中，一般将问题转换为 为原公式的模型数 图的结构 SAT求解器DPP找到一个可满足解就结束搜

第1期 谷文祥，等：可满足问题中的模型计数 ·35 索，而CDP则需要搜索整个解空间，直到找到所有 的效率，在组件的选择上，作者提出了2个优化的启 可满足的解，算法才结束.算法的时间复杂度为 发式在计算组件的模型时，优先选择最约束的组 0(mn),其中，m为子句数，n为变量数， 件，并且在计算中进行动态的跳转；同时为了防止出 -1 现模型为0而浪费搜索时间，每次在计算组件的模 d=「b(1-p, 型之前，先检查组件的可满足性。 P为一个文字出现在一个子句中的概率由于纯文 2.1.3 Cachet算法 字规则在模型计数中不能使用，因此分支变量的选 在Relsat算法中，主要是通过分别计算各个组 择直接影响了算法的时间复杂度.作者提出了2种 件的模型数来得到公式的模型个数，如果在计算的 选择分支变量的方法，一是使得m2+m的值尽可 过程中，出现了前面已经计算过的组件，利用Relsat 能小，m2、m3分别为F2、F3中的子句数，另外一种是 求解算法则需重新计算一次，如果能在第1次计算 使max(m2,m3)尽量小.通过实验得出，分支变量的 时记录这个结果，在后续的搜索过程中得到同样的 选择使用第1种方法得到的效果明显比第2种方法 组件时，便可以直接使用缓存里面存储的结果.这和 好，但当这样的变量有多个时，可以用第2种方法确 SAT求解器中的子句学习类似，利用空间换时间的 定下一个分支变量的摆选择。 方法.在Cachet算法中，同时使用了这2种方法：组 件缓存和子句学习[8] 输人 Cachet算法主要是基于SAT求解器zchaff,直 接应用组件缓存和子句学习使得算法求解出来的模 公式F为空 返回2" 型可能是实际问题模型的一个下界.为了避免这种 情况，作者提出了用Routine remove siblings的方法 N 来避免两者之间不必要的交叉. 包含空子可 返回0 Thurley在Cachet算法上利用不同的存储方式 提高了算法的空间利用率.如算法存储的组件的子 N 句至少有2个没有被赋值的变量，不显示存储原公 > 返CDP(F,n-1) 式中的二元子句，并且存储的是组件中变量的索引 以及属于组件的原始子句的索引.另外，在搜索时还 N 加入了前向的搜索机制9].Davies和Bacchus在搜 分支，返回 索中的每个节点加入了更多的推理，如超二元归结 CDP(F2.n-1)+CDP(FR-1) 和等式约简，也使得算法的效率有了很大的提 图1CDP算法框架 高.笔者还提出了利用归结的逆（扩展规则）来 Fig.1 Framework of CDP 求解问题的模型数， 2.1.2 Relsat算法 2.1.4cnf2 ddnnf算法 在CDP算法中，如果当前的赋值使得公式的值 前面提到的算法都是用不同的方法来直接求解 为真，那么剩下变量的赋值则不会影响公式的真值， 给定的问题，而Darwiche在2004年改进了以前的 若当前已赋值的变量数为t,则模型的个数为2”- 知识编译算法，在SAT求解器zchaff的基础上提出 虽然这样可以加快算法的速度，但是算法的主要时 了cn2 ddnnf算法[2].算法的主要思想是将CNF公 间还是花费在分支计算上，如果能同时计算多个分 式转换为确定的、可分解的否定范式的形式(ddn- 支的模型个数，算法的速度便可以得到很大的提 n).在转换之前，首先要为原CNF公式F构造1棵 高.由于CNF公式可以用约束图来表示，而各个独 分解树，这是一棵每个节点只有2个后代的二元树， 立的约束图可以看成是相互独立的组件，多个组件 叶子节点是F中的子句，每个节点都保存了一个称 可以同步计算其模型的个数，因此可以将组件的思 为separator变量集，里面存储的是左子树和右子树 想应用于模型计数中，即算法Relsat)] 相同的变量.算法的主要思想是为separator变量集 Relsat算法也是基于DPP算法的思想，与CDP 中的变量赋值，使得左右子树变量的交集为空，然后 算法最大的不同是Relsat中加入了组件思想，即若 递归地构造分解树并将其转换为ddnnf的形式 F包含了k个组件，则M(F)=:-夏（Fm),其中 2.2近似求解 M(F)表示公式F的模型数.为了进一步提高算法 模型计数的时间复杂度是属于#P完全的，这是

·36 智能系统学报 第7卷 比NP完全问题（如SAT问题的可满足性）更困难的 2.2.2 SampleCount算法 一类问题.目前确定性算法能求解的问题的变量数 ApproxCount算法虽然能快速地估计问题的模 约为几百个，对于更大规模的问题，这样的求解器是 型数，但是算法要求采样是均匀的，而进行均匀采样 无能为力的.另一方面，在某些领域，并不一定要求 的复杂度是NP的，且算法对得到的结果没有保证 得到问题精确的模型数，而只需要一个大概的估计. Gomes等在IJCAIO7会议上提出的SampleCount算 近似求解便能很好地满足这样的问题，近似求解算 法避免了这样的问题5) 法不仅在时间复杂度上比确定性算法要低很多，而 SampleCount算法主要是先为一些变量设定初 且能解决更大规模的问题 值，直到化解后的子公式能够使用exact count算法 2.2.1 ApproxCount算法 进行求解，该算法与采样的质量（即是否为均匀采 近似求解算法主要是基于采样的思想，在Ap 样)没有任何关系.主要是用SampleSAT4]作为启 proxCount算法[a]中，用SampleSAT4]来进行采样. 发式来指导设定初值的变量的选择，一般选择平衡 由于在采样的过程中使用随机行走算法，出现频率 变量，如果没有，则使用等价变量化解公式.该算法 最高的解与出现频率最低的解相差了几个数量级； 得到的公式的模型数为M(F)=2-“M(G),s为设 因此在SampleSAT算法中加入了MCMC(Markov 定初值的变量数，是松弛因子，M(G)为exact chain Monte Carlo)来平衡随机行走，使得采样尽量 count计算出的子公式确定的模型数.SampleCount 均匀 算法不仅能保证得到的下界的正确率，而且即使采 首先从公式F的解空间中进行K次采样（一个 样是不均匀的也不会影响结果.算法精确度为1 采样是公式的一个可满足的解)，K的值由算法的精 2,t为迭代次数，a是松弛因子，且α>0. 确度决定.由于采样是均匀的，所以有 2.2.3 MBound算法 MBound的主要思想是在原始的公式中加入 MF)≈=4)M(FA): (1) XOR子句，对加入后的公式直接用SAT求解器进行 式中：#(x,=41)是在K次采样中，x1取61值的赋值 求解1.由于在最好的情况下，加入XOR子句可以 数，设t1=true,M(F)为公式F的模型数.定义变量 消减一半的解空间，即当加入s个X0R子句后，公 x1的乘数因子： 式仍是可满足的，因此原公式至少有2个模型.因 M(F) M,=M(F∧)≈#（年，=） (2) 为XOR约束可以有效地提供一个将解基本平分的 hash函数，所以算法的求解与解在解空间中的分布 由式(1)和(2)，通过递归计算，可得公式F的模型 没有关系.算法迭代t次，每次迭代中都加入s个 数为 XOR子句.若每次迭代的结果公式都是可满足的， M(F) M(F=） M(）=(F, 则算法的下界为2-“，其中α是松弛因子，且α>0. ”X·…X 上界2+a也是类似得到的.如果在算法中将SAT求 M(F4=42=h“1-） 解器改为模型计数的求解器，算法的求解精度能进 1 =M×M2×…×M 一步提高 式中：F,为FAx单元归结后的子公式，其他类似 根据相变的原理，当C/V(子句数/变量数)小 3CSP中的模型计数 于某个值时，模型数很多，因此理论上搜索的时间也 约束可满足问题是SAT问题的一种泛化，当 多，但是ApproxCount算法的搜索时间与C/基本 CSP问题中变量的取值为布尔值时，CSP问题就变 无关 为了普通的SAT问题.CSP问题的多值使得其在实 近似求解时会出现由于小误差的积累而导致大 际生活中有着更加广泛的应用，如图着色问题和规 的误差，但是这种情况在ApproxCount算法中没有 划问题.目前求解CSP的模型计数问题的算法只能 出现，因为有50%的时间步过高估计了乘数因子， 求解变量数在100以内的问题，且要花费大量时间. 而另外的50%过低估计了乘数因子，从而使得整个 由此，设计一个好的求解CSP模型的算法就成为了 过程的求解偏差并不大.该算法是递增式进行的，每 一个急需解决的问题， 次设置一个变量的值，并且在每一步计算乘数因子. 3.1精确求解 ApproxCount时间复杂度是关于问题规模的多项式 目前关于#CSP精确求解的研究成果并不多，以 时间的。 下是主要的求解方法

第1期 谷文祥，等：可满足问题中的模型计数 ·37 3.1.1CSP2SAT算法 composition)的搜索方法来求解CSP问题的模型数， Angelsmark等在2002年给出了一种求解#CSP 树分解的本质是对c:∩c(c是c:的儿子)的赋值能 的方法，这种方法的主要思想是将原问题转换为相 够把初始问题分成2个能独立求解的问题.树搜索 对简单的问题(2SAT),通过求解转换后的问题的模 中假定簇c:中变量的赋值总是先于c:儿子中变量 型数来得到原问题的模型数] 的赋值，这样的变量排序可以利用树分解的性质.对 给定变量数为n,值域为d的二元CSP实例P. 于树中的簇c:,逐一对变量赋值，若出现冲突，则进 将P转换为多个2SAT实例I,I1,…,Im,使得P的 行回退，直到c:中所有的变量都已经赋值.然后通 模型数与转换后的1。，L1,…,Im模型总数相同，其中 过BTD算法计算c:的第1个儿子c引导的子问题 m的大小与n、d的值均有关，每个实例I,(k=0,1, 在赋值c:∩c下的模型数，将c:在当前赋值下的模 …,m)中的变量对应P中变量的值，即I中的变量 型的乘积返回，c:中所有赋值的模型数的和作为c x。表示P中变量x取值为e,对于给定的变量x∈ 的模型数.最后得到c1的模型数即为要求解的问题 var(P),e∈Dom(x),则x。∈var(I)取值为真当且 的模型数9].该算法的时间复杂度是O(mnd+l), 仅当变量x的赋值为e.实例I主要由两部分组成： 其中，w为树宽， 1)与原问题中的约束对应的子句，即若P中有约束 3.2近似求解 x≠y,则对所有的e,有(xVy.).2)剩下的子句将 3.2.1CSP+X0R算法 由原问题中变量的域分对构成.如x∈var(P),e1, 2006年，Gomes等将XOR应用于求解SAT问 e2∈Dom(x),则加人子句(x。Vx2)和(x。V 题的模型计数中，使得算法不仅能给出问题模型的 7x),对于其他e∈Dom(x)且e≠e1,e≠e2,则添加 上下界，还能对给定的结果进行评估16.2007年， x。,由此来保证x只能取e1或者e2中的一个.若d 他们扩展了这一思想，将XOR应用到求解CSP问 为偶数，则有(d/2)”个实例，并且覆盖了原问题P; 题模型数20] 若d为奇数，作者给出了一种比较复杂的域的分法. 作者提出了2种实现方法.一是将CSP问题转 整个算法的时间复杂度为：当d为奇数时，分2种情 换成SAT问题，然后直接加人二值的XOR,求解的 况考虑，当d=4k+1,时间复杂度为0(0(#2SAT)× 过程和MBound算法相同.算法得到的模型个数的 (d+d+2)/4));当d=4k+3,时间复杂度为 上下界和值的准确度也和MBound算法相同.另外 0(0(2SAT)((d2+d)/4)2),其中0(#2SAT)是 一种是不需要转换，直接加人更一般的XOR约束到 目前#2SAT问题最好的求解器所用的时间复杂度. CSP问题中，算法得到的模型数的下界为-“，准确 3.1.2CSP2wSAT算法 度为1-d,其中，s是问题中加入的XOR约束的数 算法的主要思想是将CSP问题转换为weigh- 目，t是算法迭代的次数，心就是一个松弛因子 ted-2SAT问题，但要根据不同的d值，采用不同的方 3.2.2 ApproxBTD算法 式.当d≤5时，问题直接转换，然后利用求解 前面介绍的BTD算法只能解决树宽比较小的 #weighted-2SAT模型个数的方法来求解原问题的模 问题，当问题的树宽比较大，且为稀疏图时，BTD算 型个数；当d>5时，将d分为小于5且不相交的集 法会因为超时而不能给出问题的模型数.而Approx- 合，不同的集合代表不同的问题实例，然后分别将这 BTD算法能够快速地给出更大规模问题的模型数 些问题实例转换为weighted-2SAT问题，以这些实例 近似值， 的复杂度基底的和作为原问题复杂度的基底，由此 该算法主要思想是将图拆分成没有公共边的子 得到了原问题的时间复杂度] 图，且每个子图都是chordal的.对于每一个这样的 该算法的时间复杂度为： 子图，调用BTD求解，然后利用这些子图的模型数 0((d/4·a)"), d%4=0: 来估计原问题的模型个数「。 0((a3+Ld/4-1」·a)), d%4=1; 3.2.3AE-count算法 0((a+ld/4」·a4)"), d%4=2; 许可等证明了用RB模型生成的随机CSP问题 0((a+a3+Ld/4-1」·a)),d9%4=3. 存在确定的相变点21，因此笔者也提出了一种近似 式中：a是#weighted-.2SAT算法时间复杂度的上界基 求解RB模型生成随机CSP实例的算法一AE- 数，即O(#weighted-2SAT)=O(a") count2].该算法主要利用了一阶矩和二阶矩在证明 3.1.3BTD算法 相变点位置时的特殊作用，证明了算法AE-cout的 Favier等利用BTD(backtracking with tree-de 时间复杂度是线性的，并且随着问题规模的增大，算

·38 智能系统学报 第7卷 法的精确度越高.定理1是该算法的主要的思想， [3]DARWICHE A.The quest for efficient probabilistic infer- 定理1[】给定用RB模型生成的CSP实例I、 ence[R].Edinburgh,UK:IJCAI,2005 k、a和r满足不等式e≥1(k≥1/(1-p)和 [4]DUBOIS O.Counting the number of solutions for instances a>1/k,则当n→o且满足p<1-ea(或r<-a of satisfiability[J].Theoretical Computer Science,1991, 81(1):4964. ln(1-p)时， [5]ZHANG Wenhui.Number of models and satisfiability of sets lim(P((1-6)E()< of clauses[J].Theoretical Computer Science,1996,155 (1+6)E(X))≈1. (1):277-288 式中：X表示实例I解的数目，E(Xa)表示实例1 [6]BIRNBAUM E,LOZINSKII E L.The good old Davis-Put- 解数的期望值，δ为任意的实数，P为概率分布函数 nam procedure helps counting models[J].Journal of Artifi- cial Intelligence Research,1999,10(1):457-477. 4未解决的问题 [7]BAYARDO R J Jr,PEHOUSHEK J D.Counting models u- sing connected components[C]//Proceedings of the Seven- 模型计数问题是目前人工智能领域的研究热点 teenth National Conference on Artificial Intelligence and 之一，但还存在如下一些开放性的问题， Twelfth Conference on Innovative Applications of Artificial 1)在SAT问题中，模型计数的确定性算法能解 Intelligence.Austin,USA,2000:157-162. 决的问题的变量数约为几百个，这与决策问题能解 [8]SANG T,BACCHUS F,BEAME P,et al.Combining com- 决的问题规模相差了好几个数量级.能否设计出计 ponent caching and clause learning for effective model 算大规模问题的确定性算法便成为一个亟需解决的 counting C/OL].[2011-07-20 ]http://cs.rochester. 难题 edu/~kautz/papers/modelcount-sat04.pdf. 2)相较于SAT问题，CSP问题结构更加复杂， [9]THURLEY M.SharpSAT:counting models with advanced component caching and implicit BCP M]//BIERE A, 所以求解时更加得困难.针对CSP问题本身的结构 GOMES C P.Theory and Applications of Satisfiability Tes- 设计算法，以提高算法的求解效率，则是另一个需要 ting.Seattle,USA:Springer,2006:424-429. 进一步研究的问题。 [10]DAVIES J,BACCHUS F.Using more reasoning to im- prove #SAT solving[C]//Proceedings of the 22nd National 5结束语 Conference on Artificial Intelligence.Vancouver,Canada, 本文给出了SAT和CSP问题目前主要的模型 2007:185-190. 计数方法，并对算法的优缺点进行了评价.模型计数 [11]YIN Minghao,LIN Hai,SUN Jigui.Counting models u- 的精确算法只能解决小规模的问题，并且算法的时 sing extension rules[C]//Proceedings of the 22nd National Conference on Artificial Intelligence.Vancouver,Canada, 间复杂度随着问题规模增大呈指数级增长.将更多 2007:1916-1917. 的规则应用到算法中，以减小解空间，从而快速地求 [12]DARWICHE A.New advances in compiling CNF into de- 出解数是该类算法的一个发展方向.近似求解能解 composable negation normal form[C]//Proceedings of the 决较大规模的问题，但是算法的复杂度随着算法的 16th Eureopean Conference on Artificial Intelligence.Va- 精度的提高和规模的增大而增大，AE-count算法不 lencia,Spain,2004:328-332. 仅简单，而且当变量的值趋于无穷时，算法的精度为 [13 ]WEI W,SELMAN B.A new approach to model counting 100%,可以作为精确算法.将AE-count应用于一般 [M]//FAHIEM B,WALSH T.Theory and Applications 的SAT和CSP是下一步的工作重点，最后希望本 of Satisfiability Testing.St.Andrews,UK:Springer, 2005:324-339. 文的工作能对相关人员的研究提供帮助。 [14]WEI W,ERENRICH J,SELMAN B.Towards efficient 参考文献： sampling:exploiting random walk strategies C]//Pro- ceedings of the 19th National Conference on Artificial In- [1]COOK S A.The complexity of theorem-proving procedures telligence,Sixteenth Conference on Innovative Applica- [C]//Proceedings of the Third Annual ACM Symposium on tions of Artificial Intelligence.San Jose,USA,2004: Theory of Computing.New York,USA:ACM,1971:151- 670-676. 158. [15]GOMES C P,HOFFMANN J,SABHARWAL A,et al. [2]VALIANT L G.The complexity of computing the permanent From sampling to model counting[C]//Proceedings of the [J].Theoretical Computer Science,1979,8(2):189- 20th International Joint Conference on Artificial Intelli- 201. gence.San Francisco,USA:Morgan Kaufmann Publishers

第1期 谷文祥，等：可满足问题中的模型计数 ·39 Inc,2007:2293-2299 straint satisfaction problems[J].Journal of Artificial Intel- [16 GOMES C P,SABHARWAL A,SELMAN B.Model ligence Research,2000,12:93-103. counting:a new strategy for obtaining good bounds[C]/ [22]HUANG Ping,YIN Minghao,XU Ke.Exact phase transi- Proceedings of the Twenty-First National Conference on tions and approximate algorithm of #CSP[C/OL].[2011- Artificial Intelligence and the Eighteenth Innovative Appli- 07-20 ]http://www.aaai.org/ocs/index.php/AAAI cations of Artificial Intelligence Conference.Boston, AAAI11/paper/view/3508/4142. USA,2006:54-61. 作者简介： [17]ANGELSMARK O,JONSSON P,LINUSSON S,et al. 谷文祥，男，1947年生，教授，博士 Determining the number of solutions to binary CSP in- 生导师，主要研究方向为智能规划与规 stances[C]//Proceedings of the 8th Intemational Confer- 划识别、形式语言与自动机、模糊数学 ence on Principles and Practice of Constraint Program- 及其应用.参与或承担多项国家自然科 ming.Ithaca,USA,2002:327-340. 学基金项目、教育部重点项目、省科委 [18]ANGELSMARK O,JONSSON P.Improved algorithms for 项目，发表学术论文100余篇。 counting solutions in constraint satisfaction problems[C]/ Proceedings of the 8th Interational Conference on Princi- 朱磊，男，1987年生，硕士研究生，主 ples and Practice of Constraint Programming.Kinsale,Ire- 要研究方向为智能规划、智能信息处理 land,2003:81-95. [19]FAVIER A,GIVRY S D,JEGOU P.Exploiting problem structure for solution counting[C]//Proceedings of the 15th Intemational Conference on Principles and Practice of Constraint Programming.Lisbon,Portugal,2009:335- 343. 黄平，女，1986年生，硕士研究生， [20]GOMES C P,Van HOEVE W J,SABHARWAL A,et al. 主要研究方向为智能规划与规划识别. Counting CSP solutions using generalized XOR constraints [C]//Proceedings of the 22nd National Conference on Ar- tificial Intelligence.Vancouver,Canada,2007:204-209. [21]XU Ke,LI Wei.Exact phase transitions in random con- 《智能系统学报》2012年再获国家自然科学基金资助 《智能系统学报》申报的国家自然科学基金项目“着力加强基金成果报道，打造智能科学精品期刊”获得 批准立项，得到国家自然科学基金资助，这是该刊继2011年获得国家自然科学基金资助后取得的又一重要 成绩 为提升科技期刊的核心竞争力，积极推动科研发展和科技创新，国家自然科学基金委遴选出对学科发展 起到积极促进作用、具有较高学术影响力和知名度的期刊给予基金支持，通过加大国家自然科学基金论文的 刊发力度，促进期刊综合竞争实力的整体提升，实现国家自然科学基金项目研究与期刊高水平发展的良性互 动通过该基金项目的建设，必将极大地促进《智能系统学报》综合竞争实力的全面提升，加快推进精品期刊 建设进程，并在科技进步与社会发展中发挥更为重要的作用