#SAT在人工智能领域取得了广泛应用,很多现实问题可以规约成#SAT进行求解,得到命题理论的模型个数。扩展规则是与归结互补的一种高效推理方法,在处理互补因子较高的子句集有明显的优势,自提出以来受到了国内外广泛的关注。本文旨在提高基于扩展规则的#SAT算法求解效率与求解能力,其中求解能力用规定时间内可以求解问题的规模来衡量。通过对基于扩展规则的#SAT求解器的深入研究,本文提出一种新的基于扩展规则的#SAT求解算法NCER（Novel algorithm for Counting models using Extension Rule）,该算法在#ER的基础上加入启发式策略。该策略每次选择当前子句集的最长子句来减小极大项空间,使得递归调用的次数减少,从而加快求解效率。为解决基于扩展规则的#SAT求解器在互补因子较小的样例上的不良表现,结合NCER和CDP（Counting models using Davis-Putnam procedure）的优点提出混合#SAT求解算法NCDPER（Novel algorithm for Counting models using Davis-Putnam procedure and Extension Rule）。NCER较先前的#ER在所有85个随机SAT测试用例上有了显著的提高。为进一步提高基于扩展规则的#SAT求解器的求解效率,本文提出两种加速#SAT求解的启发式策略:MW和LC&MW。MW每次选择权值最大的子句作为规约子句;LC&MW每次选择最长子句作为规约子句,若最长子句存在多个,则在多个最长子句中选择权值最大的子句作为规约子句。本文利用MW策略设计了算法CERMW,利用LC&MW策略设计了算法CERLC&MW。实验结果表明:CERMW和CERLC&MW较先前的#SAT求解算法在求解效率和求解能力上都有显著提高。在求解效率方面,CERMW和CERLC&MW的求解速度是其它算法的1.4～100倍。在求解能力方面,CERMW和CERLC&MW在限定时间内可解的测试用例更多。本文提出的四种#SAT求解算法较原有的基于扩展则的#SAT,无论是在求解效率还是求解能力方面,都有了较为明显的提高。将扩展规则的应用范围进一步提高,使其适用于一些更大规模的测试用例。
近年来，相变现象已成为人工智能领域的一个研究热点。对NP完全问题相变的研究可以帮助我们理解问题困难的本质，从而提出更有效的求解算法。相变现象指的是随着某个参数的变化，问题的属性出现突变的情况。比如，对于SAT问题，随着r(子句数/变量数)的增大，问题实例的可满足性发生从几乎都可满足到几乎都不可满足的相变现象。目前有很多关于SAT问题相变的研究，但是除了k=2（k为子句的长度）相变点是确定的，当k>2时，随机可满足问题的相变点都是不确定的，只能给出其上下界。
CSP问题是SAT问题的一种泛化形式，目前也有许多从实验和理论两方面介绍关于CSP问题相变的研究。在这些工作中，(Xu and Li2000)是少数证明CSP问题有相变且相变点确定的工作。他们提出了一种新的模型，RB模型。RB模型是B模型的一种变形，但是却有一些特殊的性质。首先，证明了用RB模型生成的CSP问题存在相变现象，且相变点是确定的。其次，无论实验角度还是理论的角度都证明了RB模型可以生成困难的实例（Xu et al2007）。
相变现象不仅发生在NP-hard和NP-complete问题中，也出现在更困难的问题中，如QSAT和规划，组合问题的模型计数也成为近年来的一个研究热点。最近研究表明，SAT问题和CSP模型计数的复杂度相当于一致图规划问题和一些概率问题的求解，即为#P完全的。Bailey等人首次证明了SAT的模型计数问题存在相变现象。本文将其扩展为求解CSP模型计数的相变现象，即#CSP的决策问题是存在相变的，#CSP(dn/t)：给定一个CSP实例，是否存在至少dn/t个解。我们证明对于RB模型生成的CSP实例，其相变现象是确切存在的，且相变点也是确定的。
对于组合问题的模型计数问题，另一个研究方向为设计算法从而快速求解出问题模型的个数。1999年，Birnbaum等人设计出第一个求解#SAT问题的确定算法CDP，这是求解SAT可满足性算法DP的扩展。随后出现了如组件缓存和子句学习等方法来提高求解#SAT问题的求解效率。由于算法的时间和空间代价一般是随着问题规模的增大而呈指数级的增长，近似算法应运而生，如Approx-count, Sample-count和Sample-Minisat等。对于#CSP问题，Gomes等人在2007通过加入XOR约束的方法近似问题的模型数。本文提出了一个近似CSP问题模型数的新方法，使用我们提出的方法不仅可以高效的求解问题，而且问题的规模越大，算法的精度越高。
暂无评论