Journal of Northeastern University Natural Science ›› 2019, Vol. 40 ›› Issue (5): 630-635.DOI: 10.12068/j.issn.1005-3026.2019.05.005

• Information & Control • Previous Articles     Next Articles

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

LYU Shuai, ZHANG Tong-bo, WANG Qiang, LIU Lei   

  1. College of Computer Science and Technology, Jilin University, Changchun 130012, China.
  • Received:2018-03-26 Revised:2018-03-26 Online:2019-05-15 Published:2019-05-17
  • Contact: LIU Lei
  • About author:-
  • Supported by:
    -

Abstract: 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.

Key words: automated reasoning, extension rule, model counting, maxterm space, heuristic strategy

CLC Number: