Heuristic Complete Algorithm for SAT Problem by Using Logical Deduction

被引：0
|
作者：
Chen Q. [1 ]
Xu Y. [2 ]
He X. [2 ]
机构：
[1] School of Information Science and Technology, Southwest Jiaotong University, Chengdu
[2] National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu
来源：
Xinan Jiaotong Daxue Xuebao/Journal of Southwest Jiaotong University | 2017年 / 52卷 / 06期
关键词：
Decision making; Deductive reasoning; Heuristic algorithms; Satisfiability problem; Searching algorithms;
D O I：
10.3969/j.issn.0258-2724.2017.06.025
中图分类号：
学科分类号：
摘要：
In order to address the issue of branch decision-making inefficiency in solving the satisfiability problem (SAT), a heuristic complete algorithm based on logical deduction group (LDG) is proposed. Specifically, the proposed algorithm chooses the remaining unsolved clauses to make the logical deduction such that an assignment sequence of partial satisfiability is obtained, further guiding the solver to first search its solution space. For the satisfiable problem, the partial assignment can be extended group by group to a complete assignment by iteratively utilizing the deductive process. For the unsatisfiable problem, it can be straightforward to judge whether there exists an empty clause. The international competition instance in SAT is adopted for comparison with the typical exponential variable state independent decaying sum (EVSIDS) decision heuristic. The experimental results demonstrate that LDG can solve 42 more problems than EVSIDS, and achieve 22.8% and 17.8% reductions in average solution time for the satisfiable and unsatisfiable problems, respectively, as well as a 20.1% reduction in total average time. © 2017, Editorial Department of Journal of Southwest Jiaotong University. All right reserved.
引用
收藏
页码：1224 / 1232
页数：8
相关论文
共 22 条
  • [1] Cook S.A., The complexity of theorem-proving procedures, 3rd Annual ACM Symposium on Theory of Computing, pp. 151-158, (1971)
  • [2] Davis M., Logemann G., Loveland D., A machine program for theoremproving, Communications of the ACM, 5, 7, pp. 394-397, (1962)
  • [3] Moskewicz M.W., Madigan C.F., Zhao Y., Chaff: engineering an efficient SAT solver, Proceedings of the 38th Annual Design Automation Conference, pp. 530-535, (2001)
  • [4] Een N., Soensson N., An extensible SAT solver, SAT 2003, pp. 502-518, (2015)
  • [5] Gomes C.P., Selman B., Kautz H., Boosting combinatorial search through randomization, Proceeding of the Fifteenth National Conference on Artificial Intelligence, pp. 431-437, (1998)
  • [6] Goldberg E., Novikov Y., BerkMin: a fast and robust SATsolver, Proceedings of Design, Automation and Test in Europe Conference, pp. 142-149, (2002)
  • [7] Lewis M.D.T., Schubert T., Becker B., Speedup techniques utilized in modern SAT solvers, International Conference in Theory and Applications of Satisfiability Testing, pp. 437-443, (2005)
  • [8] Ryan L., Efficient algorithms for clause-learning SAT solvers, (2004)
  • [9] Marques-Silva J.P., Lynce I., Malik S., Conflict-driven clause learning SAT solvers, In Handbook of Satisfiability, pp. 127-149, (2009)
  • [10] Marques-Silva J.P., Sakallah K.A., Grasp: a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM International Conference on Computer-aided Design, pp. 220-227, (1996)
123