Learnt Clauses Optimize Method Based on Restart Strategy

doi:10.12068/j.issn.1005-3026.2020.01.008

Abstract

Abstract: With the background of optimization of the learnt clauses database， a new optimization method for learnt clauses based on the original MiniSAT solver was proposed. Based on game theory， this method adjusts the growth parameters after several restarts on the basis of the real-time feedback of the current solver， in order to be as close as possible to the balance point of clauses in the learnt clauses database. This makes the storage capacity of the learnt clause database reach the Pareto optimality as much as possible. Experiments showed that the proposed method is effective and outperforms existing optimization methods in random SAT problems. This method neither affects the speed of unit propagation because of too many clauses in the learnt clause database， nor destroys the integrity of learning because of too few clauses in the learnt clause database.

Key words: DPLL(Davis-Putnam-Logemann-Loveland), clause learning, learnt clauses database, MiniSAT solver, Pareto optimality

CLC Number:

TP181

LI Zhuang， LIU Lei， ZHANG Tong-bo， LYU Shuai. Learnt Clauses Optimize Method Based on Restart Strategy[J]. Journal of Northeastern University Natural Science, 2020, 41(1): 44-48.

References

[1]Beame P，Kautz H，Sabharwal A.Towards understanding and harnessing the potential of clause learning［J］.Journal of Artificial Intelligence Research，2004，22:319-351.
[2]Silva J，Sakallah K.Grasp—a new search algorithm for satisfiability［C］//IEEE/ACM International Conference on Computer-aided Design(CAD 1996).Ann Arbor，1996:220-227.
[3]Audemard G，Simon L.Predicting learnt clauses quality in modern SAT solvers［C］//International Joint Conference on Artificial Intelligence(IJCAI 2009).Pasadena，2009:399-404.
[4]Luo M，Li C，Xiao F，et al.An effective learnt clause minimization approach for CDCL SAT solvers［C］//Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence(IJCAI 2017).Melbourne，2017:703-711.
[5]Moskewicz M，Madigan C，Zhao Y，et al.Chaff:engineering an efficient SAT solver［C］//Proceedings of Design Automation Conference(DAC 2001).Las Vegas，2001:530-535.
[6]Audemard G，Lagniez J M，Mazure B，et al.On freezing and reactivating learnt clauses［C］//Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing(SAT 2011).Ann Arbor，2011:188-200.
[7]Hamadi Y，Jabbour S，Sas L.What we can learn from conflicts in propositional satisfiability［J］.Annals of Operations Research，2016，240(1):13-37.
[8]Luo M，Xiao F，Li C，et al.Maple_CM，Maple_CM_Dist，Maple_CM_ordUIP and Maple_CM_ordUIP+ in the SAT competition 2018［C］//Proceedings of SAT Competition 2018—Solver and Benchmark Descriptions.Oxford，2018:44-46.
[9]Atserias A，Fichte J K，Thurley M.Clause-learning algorithms with many restarts and bounded-width resolution［J］.Journal of Artificial Intelligence Research，2011，40:353-373.
[10]Dixon H E，Ginsberg M L，Parkes A J.Generalizing boolean satisfiability I:background and existing work［J］.Journal of Artificial Intelligence Research，2004，21:193-243.
[15]关守平，房少纯.一种新型的区间-粒子群优化算法［J］.东北大学学报(自然科学版)，2012，33(10):1381-1384.(Guan Shou-ping，Fang Shao-chun.A new particle swarm optimization algorithm［J］.Journal of Northeastern University(Natural Science)，2012，33(10):1381-1384.)

[1]	LI Chan， QU Lu-xuan， XIN Jun-chang， WANG Zhi-qiong. High-Order Dynamic Bayesian Network Modelling Method Based on Potential Regulatory Factors Screening [J]. Journal of Northeastern University(Natural Science), 2023, 44(3): 323-330.
[2]	QU Lu-xuan， GUO Shang-hui， WANG Zhi-qiong， XIN Jun-chang. Modelling of Gene Regulatory Networks by Parent Node Screening-Based Bayesian Method [J]. Journal of Northeastern University Natural Science, 2020, 41(2): 158-162.
[3]	MA Tie-min， ZHOU Fu-cai， WANG Shuang. Social Network Event Recommendation Algorithms Based on User Similarity Random Walk [J]. Journal of Northeastern University Natural Science, 2019, 40(11): 1533-1538.
[4]	LIU Peng， DU Jia-zhi， LYU Wei-gang， DOU Ming-wu. A Modified KNN Classifier for Unbalanced Dataset [J]. Journal of Northeastern University Natural Science, 2019, 40(7): 932-936.
[5]	LYU Shuai， ZHANG Tong-bo， WANG Qiang， LIU Lei. Two Novel Algorithms Based on Extension Rule for Solving #SAT Problem [J]. Journal of Northeastern University Natural Science, 2019, 40(5): 630-635.
[6]	WANG Jue， QIAO Jian-zhong， LIN Shu-kuan. Hierarchical Granular Support Vector Regression Based on Distance and Temporal [J]. Journal of Northeastern University Natural Science, 2016, 37(7): 942-946.
[7]	GU De-ying， WANG Na， LI Wen-chao， CHEN Long. Method of Lane Line Detection in Low Illumination Environment Based on Model Fusion [J]. Journal of Northeastern University(Natural Science), 2021, 42(3): 305-309.
[8]	WANG Shu， GUAN Zhan-xu， WANG Jing， SUN Xiao-hui. Bayesian Network Parameter Learning Method Based on Transfer Learning [J]. Journal of Northeastern University(Natural Science), 2021, 42(4): 509-515.
[9]	WANG Shu， REN Yu， GUAN Zhan-xu， WANG Jing. Multi-source Data Fusion Method Based on Difference Information [J]. Journal of Northeastern University(Natural Science), 2021, 42(9): 1246-1253.
[10]	CHANG Yu-qing， ZHAO Wei-wei， LIU Le-yuan， KANG Xiao-yun. Modeling of Coal Mill Process Monitoring Based on Instance-based Transfer Learning [J]. Journal of Northeastern University(Natural Science), 2021, 42(10): 1369-1375.
[11]	GU De-ying， ZHANG Song， MENG Fan-wei. Vehicle 3D Space Detection Method Based on Monocular Vision [J]. Journal of Northeastern University(Natural Science), 2022, 43(3): 328-334.
[12]	DING Lai-xu， LIU Hong-juan. Recommendation Algorithm Based on Multi-dimensional Feature Representation Learning in Complex Networks [J]. Journal of Northeastern University(Natural Science), 2022, 43(3): 359-367.
[13]	ZHAO Hai， CHEN Jia-wei， SHI Han， WANG Xiang. A Transfer Learning Algorithm Applied to Human Activity Recognition [J]. Journal of Northeastern University(Natural Science), 2022, 43(6): 776-782.
[14]	LIU Yang， YAN Dong-mei， MENG Fan-wei. Improved Two-Branch Person Re-identification Algorithm Based on Transformer [J]. Journal of Northeastern University(Natural Science), 2023, 44(1): 26-32.
[15]	WANG Ying， WANG Ze-hao， LI Hong， HUANG Wen-jun. Named Entity Recognition in Threat Intelligence Domain Based on Deep Learning [J]. Journal of Northeastern University(Natural Science), 2023, 44(1): 33-39.