计算机科学 ›› 2017, Vol. 44 ›› Issue (11): 279-283.doi: 10.11896/j.issn.1002-137X.2017.11.042
陈青山,徐扬,吴贯锋,何星星
CHEN Qing-shan, XU Yang, WU Guan-feng and HE Xing-xing
摘要： 适当的重启有助于求解器跳出局部最优,但频繁重启会严重降低效率。为解决CDCL求解器重启触发条件随意性大的问题,提出一种基于搜索路径识别的延迟重启算法。该算法使用Luby序列触发延时重启判断,将当前搜索路径和已搜索路径转换为向量空间模型,通过计算向量空间相似度来判断当前搜索过程是否会进入重复搜索空间。若向量空间相似度达到设定阈值,则触发重启,否则延迟重启。采用SAT国际竞赛的实例,与两个主流的求解器进行了对比实验。结果表明,所提算法能够有效规避重复搜索空间问题,并显著提高求解效率。
| [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] EN N,SRENSSON 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,FRHLICH A.Evaluating CDCL Restart Schemes [C]∥Proceedings of the International Workshop on Pragmatics of SAT.2015. [18] EN N,SRENSSON 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! |
|
||
首页