Computer Science ›› 2017, Vol. 44 ›› Issue (11): 279-283.doi: 10.11896/j.issn.1002-137X.2017.11.042

Previous Articles     Next Articles

Path Identification Based Delaying Restart Algorithm for CDCL SAT Solver

CHEN Qing-shan, XU Yang, WU Guan-feng and HE Xing-xing   

  • Online:2018-12-01 Published:2018-12-01

Abstract: An appropriate restart is helpful for a solver to jump out of the local optimization,but more frequent restarts will significantly reduce the efficiency.To address the arbitrariness of triggering conditions for the restart of CDCL solver,the delaying restart algorithm based on path identification was proposed in this paper.Specifically,the Luby sequence is utilized to trigger the delaying restart decision,which converts current path and the searched paths to vector space models (VSMs) such that the similarity of VSMs is calculated to judge whether the current search process will get into the repetitive search space.Once the underlying similarity reaches a given threshold,the restart is triggered,otherwise it will be delayed.SAT international testing example and two state-of-the-art solvers were adopted for comparison purpose.The experimental results show that the proposed algorithm can not only effectively avoid the repetitive search space,but also obviously improve the solving efficiency.

Key words: Satisfiability problem,Propositional logic,Restart,Path identification,Vector space model

[1] COOK S A.The complexity of theorem-proving procedures[C]∥Proceedings of 3rd Annual ACM Symposium on Theory of Computing.New York:ACM,1971:151-158.
[2] DAVIS M,LOGEMANN G,LOVELAND D.A machine program for theorem proving[J].Communications of the ACM,1962,5(7):394-397.
[3] SILVA J P M,LYNCE I,MALIK S.Conflict-driven clauselearning SAT solvers [M]∥Handbook of Satisfiability.Amsterdam,IOS Press,2009:127-149.
[4] MOSKEWICZ M W,MADIGAN C F,ZHAO Y.Chaff:Engi-neering an efficient SAT solver [C]∥Proceedings of the 38th Annual Design Automation Conference.New York:ACM,2001:530-535.
[5] MARQUES-SILVA J P,SAKALLAH K A.Grasp:a newsearch algorithm for satisfiability [C]∥Proceedings of the 1996 IEEE/ACM International Conference on Computer-aided Design.Los Alamitos:IEEE Computer Society Press,1996:220-227.
[6] GOMES C P,SELMAN B,KAUTZ H.Boosting combinatorialsearch through randomization[C]∥Proceedings of AAAI’98.1998:431-437.
[7] GOLDBERG E,NOVIKOV Y.BerkMin:a fast and robust SAT solver [C]∥Proceedings of the symposium on Design,Automation and Test in Europe Conference.2002:142-149.
[8] GOMES C,SELMAN B,CRATAO N,et al.Heavy-tailed phenomena in satisfiability and constraint satisfaction problems [J].Journal of Automated Reasoning,2000,24(1/2):67-100.
[9] PIPATSRISAWAT P,DARWICHE A.A lightweight compo-nent caching scheme for satisfiability solvers [C]∥Proceedings of the International Conference on Theory and Applications of Satisfiability Testing-SAT 2007.Heidelberg:Springer,2007:294-299.
[10] VANDER TAK P,RAMOS A,HEULE M.Reusing the assignment trail in CDCL solvers [J].Journal on Satisfiability,Boolean Modeling and Computation,2011,7(4):133-138.
[11] EN N,SRENSSON N.An extensible SAT solver [C]∥Proceedings of the International Conference on Theory and Applications of Satisfiability Testing-SAT 2003.Heidelberg:Springer,2004:502-518.
[12] BIERE A.Adaptive restart strategies for conflict driven SATsolvers [C]∥Proceedings of the International Conference on Theory and Applications of Satisfiability Testing-SAT 2008.Heidelberg:Springer,2008:28-33.
[13] LUBY M,SINCLAIR A,ZUCKERMAN D.Optimal speedup of las vegas algorithms [J].Information Processing Letters,1993,47(4):173-180.
[14] HUANG J B.The effect of restarts on the efficiency of clause learning [C]∥Proceedings of the 20th International Joint Conference on Artificial Intelligence.Menlo Park:AAAI,2007:2318-2323.
[15] AUDEMARD G,SIMON L.Refining restarts strategies for SATand UNSAT [C]∥Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming.Heidelberg:Springer,2012:118-126.
[16] RYVCHIN V,STRICHMAN O.Local restarts [C]∥Procee-dings of the International Conference on Theory and Applications of Satisfiability Testing-SAT 2008.Heidelberg:Springer,2008:271-276.
[17] BIERE A,FRHLICH A.Evaluating CDCL Restart Schemes [C]∥Proceedings of the International Workshop on Pragmatics of SAT.2015.
[18] EN N,SRENSSON N.MiniSat:A SAT solver with conflict-clause minimization[C]∥SAT 2005 Competition.2005.
[19] SALTON G,WONG A,YANG C S.A vector space model for automatic indexing[J].Communications of the ACM,1975,18(11):613-620.
[20] RYAN L.Efficient algorithms for clause learning SAT solvers[D].Simon Fraser University,2004.
[21] BIERE A.PicoSAT essentials[J].Journal on Satisfiability Boo-lean Modeling and Computation,2008,4(2-4):75-97.
[22] WALSH T.Search in a small world[C]∥Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence.Stockholm,1999:1172-1177.
[23] BIERE A,HEULE M, MAAREN H V,et al.Handbook ofSatisfiability[M].IOS Press.2009.
[24] BIERE A.Yet another local searach solver and lingeling and friends entering the sat competition[C]∥Proceedings of SAT Competition 2014.2014:39-40.

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!