计算机科学 ›› 2018, Vol. 45 ›› Issue (12): 137-141.doi: 10.11896／j.issn.1002-137X.2018.12.021
陈青山1,2, 徐扬2, 吴贯锋1,2
CHEN Qing-shan1,2, XU Yang2, WU Guan-feng1,2
摘要： 针对命题逻辑公式求解过程中难以有效评估学习子句是否有利于后续搜索的问题,提出了一种基于学习子句趋势强度的评估算法。该算法首先通过分析学习子句在生存期内参与冲突分析的时间分布特征,将随机、离散的时间分布转换为连续的累积趋势强度;然后在删除周期达到时,通过设定趋势强度阈值删除在后续搜索过程中“不大可能”被使用的子句,保留“可能”被使用的子句;最后采用2015年、2016年SAT问题国际竞赛实例,将该算法与经典的活跃度评估算法和文字块距离(LBD)评估算法进行对比。实验结果表明,趋势强度评估算法在效率上明显优于活跃度评估算法,且求解的实例更多,同时与LBD算法基本持平。
中图分类号:
| [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] | 李洁, 钟小梅. 命题逻辑中三元子句集的冗余文字 Redundant Literals of Ternary Clause Sets in Propositional Logic 计算机科学, 2022, 49(6A): 109-112. https://doi.org/10.11896/jsjkx.210700036 |
| [2] | 王钇杰, 徐扬, 吴贯锋. 基于学习子句删除策略的SAT求解器分支策略 Branching Heuristic Strategy Based on Learnt Clauses Deletion Strategy for SAT Solver 计算机科学, 2021, 48(11): 294-299. https://doi.org/10.11896/jsjkx.201000142 |
| [3] | 唐雷明, 白沐尘, 何星星, 黎兴玉. 基于命题逻辑的完全标准矛盾体及最小标准矛盾体 Complete Contradiction and Smallest Contradiction Based on Propositional Logic 计算机科学, 2020, 47(11A): 83-85. https://doi.org/10.11896/jsjkx.200400072 |
| [4] | 刘婷, 徐扬, 陈秀兰. 命题逻辑中单元子句及其负文字和冗余子句 Unit Clauses and Their Complementary Literals and Redundant Clauses in Propositional Logic 计算机科学, 2019, 46(8): 255-259. https://doi.org/10.11896/j.issn.1002-137X.2019.08.042 |
| [5] | 陈成,潘正华,吕永席. 一类具有3种否定的模糊模态命题逻辑 Fuzzy Modal Propositional Logic with Three Kinds of Negation 计算机科学, 2017, 44(4): 263-268. https://doi.org/10.11896/j.issn.1002-137X.2017.04.055 |
| [6] | 徐卫,李晓粉,刘端阳. 基于命题逻辑的关联规则挖掘算法L-Eclat Propositional Logic-based Association-rule Mining Algorithm L-Eclat 计算机科学, 2017, 44(12): 211-215. https://doi.org/10.11896/j.issn.1002-137X.2017.12.038 |
| [7] | 陈青山,徐扬,吴贯锋,何星星. 一种基于搜索路径识别的CDCL命题逻辑求解器延迟重启算法 Path Identification Based Delaying Restart Algorithm for CDCL SAT Solver 计算机科学, 2017, 44(11): 279-283. https://doi.org/10.11896/j.issn.1002-137X.2017.11.042 |
| [8] | 吴晓刚,潘正华. 基于模糊命题逻辑形式系统FLcom的模糊推理及应用 Fuzzy Reasoning and its Application Based on Fuzzy Propositonal Logic 计算机科学, 2015, 42(Z11): 100-103. |
| [9] | 刘 熠,徐 扬,贾海瑞. 基于格值命题逻辑系统LP(X)的多元α-归结原理的注记 Notes on Multi-ary α-Resolution Principle Based on Lattice-valued Logical System LP(X) 计算机科学, 2015, 42(4): 249-252. https://doi.org/10.11896/j.issn.1002-137X.2015.04.051 |
| [10] | 张家锋，徐扬,何星星. 格值语义归结推理方法 Lattice-valued Semantic Resolution Reasoning Method 计算机科学, 2011, 38(9): 201-203. |
| [11] | 刘宏岚,高庆狮,杨炳儒. 集合代数是经典命题演算形式系统的语义解释 Set Algebra is Semantic Interpretation for Classical Formal System of Propositional Calculus 计算机科学, 2010, 37(9): 194-197. |
| [12] | 谷文祥,赵晓威,殷明浩. 知识编译研究 Knowledge Compilation Survey 计算机科学, 2010, 37(7): 20-26. |
| [13] | 田聪,段振华,王小兵. Einstein谜的SAT求解 Solving Einstein's Puzzle with SAT 计算机科学, 2010, 37(5): 184-186. |
| [14] | . 基于语言真值格值命题逻辑系统lvpl的推理规则 计算机科学, 2008, 35(9): 230-232. |
| [15] | . 纤维逻辑 计算机科学, 2006, 33(1): 1-3. |
|
||
首页