两种新的基于扩展规则#SAT问题求解算法

Two Novel Algorithms Based on Extension Rule for Solving #SAT Problem

提出一种新的基于扩展规则的#SAT求解算法NCER,该算法在#ER的基础上加入启发式策略.该策略每次选择当前子句集的最长子句来减小极大项空间,使得递归调用的次数减少,从而加快求解效率.为解决基于扩展规则的#SAT求解器在互补因子较小的样例上的不良表现,结合NCER和CDP的优点提出混合#SAT求解算法NCDPER.实验结果表明:NCER较先前的#ER在所有85个随机SAT测试用例上有了显著的提高.通过与目前最好的基于扩展规则的#SAT求解器的比较,该求解器具有更好的性能.

A novel #SAT solver NCER based on extension rule is proposed,which adds heuristic strategy on #ER algorithm.The heuristic strategy chooses the longest clause in current set of clauses every calling procedure to reduce the maxterm space,and it helps decrease the frequency of recursive invocation to enhance the efficiency of solving.Besides,a mixed model counting algorithm called NCDPER is proposed by combining NCER algorithm and CDP algorithm,to overcome the poor performance on instances where complementary factor of the #SAT solvers is small using the extension rule.NCDPER integrates advantages of NCER algorithm and CDP algorithm.According to the experimental results,NCER has a significant improvement over previous #SAT solvers on all 85 random SAT instances.The #SAT solvers proposed are compared with state-of-the-art #SAT solvers using extension rule,and the results show that the proposed #SAT solvers have better performances.