Computer Science ›› 2018, Vol. 45 ›› Issue (12): 137-141.doi: 10.11896/j.issn.1002-137X.2018.12.021

• Artificial Intelligence • Previous Articles     Next Articles

Learnt Clause Evaluation Algorithm of SAT Problem Based on Trend Strength

CHEN Qing-shan1,2, XU Yang2, WU Guan-feng1,2   

  1. (School of Information Science and Technology,Southwest Jiaotong University,Chengdu 611756,China)1
    (National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Chengdu 610031,China)2
  • Received:2017-11-07 Online:2018-12-15 Published:2019-02-25

Abstract: For the problem that it is difficult to effectively evaluate whether the learnt clause is beneficial to the follo-wing search in the solving process of propositional logic equation,a clause evaluation algorithm was proposed based on the trend strength.First of all,the distribution characteristic of time involved in conflict analysis for the learnt clauses during the lifecycle is analyzed,and the random,discrete time distribution is transformed into the continuous cumulative trend strength.Then,when the deletion period arrives,the clauses with little possibility of being used in the subsequent search process will be deleted by setting the threshold of trend strength,while the clauses of high probability will be kept.Lastly,by using SAT international testing examples in 2015 and 2016,two state-of-the-art algorithms (i.e.,activi-ty evaluation algorithm and literal block distance (LBD) algorithm) are adopted for comparison purpose.The experimental results show that the proposed evaluation algorithm with trend strength can significantly outperform the activity evaluation algorithm in efficiency and can obtain more solving instances,and has the comparable performance with the LBD algorithm.

Key words: Clause evaluation, Learnt clause, Periodical deletion, Propositional logic, Trend strength

CLC Number: 

  • TP301.6
[1]COOK S A.The complexity of theorem-proving procedures [C]∥3rd Annual ACM Symposium on Theory of Computing.New York:ACM,1971:151-158.
[2]BIERE A,HEULE M,VAN MAAREN H,et al.Conflict-driven clause learning SAT solvers [M]∥Handbook of Satisfiability,Frontiers in Artificial Intelligence and Applications.Amsterdam:IOS Press,2009:131-153.
[3]VAN DER 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.
[4]SILVA J P M,SAKALLAH K A.GRASP—a new search algorithm for satisfiability [C]∥Proceedings of the 1996 IEEE/ACM International Conference on Computeraided Design.Los Alamitos:IEEE Computer Society Press,1996:220-227.
[5]BAYARDO J R R J,SCHRAG R.Using CSP look-back techniques to solve real-world SAT instances [C]∥Proceedings of the 14th National Conference on Artificial Intelligence.Menlo Park:AAAI Press,1997:203-208.
[6]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.
[7]GOLDBERG E,NOVIKOV Y.BerkMin:A Fast and RobustSat-Solver [C]∥Proceedings of the Conference on Design,Automation and Test in Europe (DATE 2002).Los Alamitos:IEEE Computer Society Press,2002:142-149.
[8]SÖRENSSONN,EÉN N.MiniSat v1.13-A SAT solver withconflict-clause minimization [C]∥Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing.Berlin:Springer,2005:502-518.
[9]SIMON L,AUDEMARD G.Predicting learnt clauses quality in modern sat solver [C]∥Proceedings of the Twenty-first International Joint Conference on Artificial Intelligence (IJCAI’09).Menlo Park:AAAI Press,2009:399-404.
[10]AUDEMARD G,LAGNIEZ J-M,MAZURE B,et al.On free-zing and reactivating learnt clauses [C]∥Proceedings of the International Conference on Theory and Applications of Satisfia-bility Testing.Berlin:Springer,2011:188-200.
[11]GUO L,JABBOUR S,LONLAC J,et al.Diversification by clauses deletion strategies in portfolio parallel SAT solving [C]∥Proceedings of 2014 IEEE 26th International Conference on Tools with Artificial Intelligence (ICTAI 2014).Los Alamitos:IEEE Computer Society Press,2014:701-708.
[12]JABBOUR S,LONLAC J,SAIS L,et al.Revisiting the learned clauses database reduction strategies [OL].
[2016-10-20].https://arxiv.org/pdf/1402.1956.
[13]ANSÓTEGUI C,GIRÁLDEZ-CRU J,LEVY J,et al.Usingcommunity structure to detect relevant learnt clauses [C]∥Proceedings of the International Conference on Theory and Applications of Satisfiability Testing.Switzerland:Springer,2015:238-254.
[14]LONLAC J,NGUIFO E M.Towards Learned Clauses Database Reduction Strategies Based on Dominance Relationship[OL].
[2016-10-20].https://arxiv.org/pdf/1705.10898.
[15]LUBY M,SINCLAIR A,ZUCKERMAN D.Optimal speedup of Las Vegas algorithms [J].Information Processing Letters,1993,47(4):173-180.
[1] LI Jie, ZHONG Xiao-mei. Redundant Literals of Ternary Clause Sets in Propositional Logic [J]. Computer Science, 2022, 49(6A): 109-112.
[2] WANG Yi-jie, XU Yang, WU Guan-feng. Branching Heuristic Strategy Based on Learnt Clauses Deletion Strategy for SAT Solver [J]. Computer Science, 2021, 48(11): 294-299.
[3] TANG Lei-ming, BAI Mu-chen, HE Xing-xing, LI Xing-yu. Complete Contradiction and Smallest Contradiction Based on Propositional Logic [J]. Computer Science, 2020, 47(11A): 83-85.
[4] LIU Ting, XU Yang, CHEN Xiu-lan. Unit Clauses and Their Complementary Literals and Redundant Clauses in Propositional Logic [J]. Computer Science, 2019, 46(8): 255-259.
[5] CHEN Cheng, PAN Zheng-hua and LV Yong-xi. Fuzzy Modal Propositional Logic with Three Kinds of Negation [J]. Computer Science, 2017, 44(4): 263-268.
[6] XU Wei, LI Xiao-fen and LIU Duan-yang. Propositional Logic-based Association-rule Mining Algorithm L-Eclat [J]. Computer Science, 2017, 44(12): 211-215.
[7] CHEN Qing-shan, XU Yang, WU Guan-feng and HE Xing-xing. Path Identification Based Delaying Restart Algorithm for CDCL SAT Solver [J]. Computer Science, 2017, 44(11): 279-283.
[8] WU Xiao-gang and PAN Zheng-hua. Fuzzy Reasoning and its Application Based on Fuzzy Propositonal Logic [J]. Computer Science, 2015, 42(Z11): 100-103.
[9] LIU Yi, XU Yang and JIA Hai-rui. Notes on Multi-ary α-Resolution Principle Based on Lattice-valued Logical System LP(X) [J]. Computer Science, 2015, 42(4): 249-252.
[10] GHANG Jia-feng,XU Yang,HE Xing-xing. Lattice-valued Semantic Resolution Reasoning Method [J]. Computer Science, 2011, 38(9): 201-203.
[11] LIU Hong-lan,GAO Qing-sh,YANG Bing-ru. Set Algebra is Semantic Interpretation for Classical Formal System of Propositional Calculus [J]. Computer Science, 2010, 37(9): 194-197.
[12] TIAN Cong,DUAN Zhen-hua,WANG Xiao-bing. Solving Einstein's Puzzle with SAT [J]. Computer Science, 2010, 37(5): 184-186.
[13] . [J]. Computer Science, 2008, 35(9): 230-232.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!