{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T03:32:52Z","timestamp":1760239972077,"version":"build-2065373602"},"reference-count":33,"publisher":"MDPI AG","issue":"2","license":[{"start":{"date-parts":[[2019,2,11]],"date-time":"2019-02-11T00:00:00Z","timestamp":1549843200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Symmetry"],"abstract":"<jats:p>In mainstream conflict driven clause learning (CDCL) solvers, because of frequent restarts and phase saving, there exists a large proportion of duplicate assignment trails before and after restarts, resulting in unnecessary time wastage during solving. This paper proposes a new strategy\u2014identifying those duplicate assignments trails and dealing with them by changing the sort order. This approach\u2019s performance is compared with that of the Luby static restart scheme and a dynamic Glucose-restart strategy. We show that the number of solved instances is increased by 3.2% and 4.6%. We also make a compassion with the MapleCOMSPS solver by testing against application benchmarks from the SAT Competitions 2015 to 2017. These empirical results provide further evidence of the benefits of the proposed heuristic, having the advantage of managing duplicate assignments trails and choosing appropriate decision variables adaptively.<\/jats:p>","DOI":"10.3390\/sym11020197","type":"journal-article","created":{"date-parts":[[2019,2,12]],"date-time":"2019-02-12T03:18:20Z","timestamp":1549941500000},"page":"197","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["An Adaptive Strategy for Tuning Duplicate Trails in SAT Solvers"],"prefix":"10.3390","volume":"11","author":[{"given":"Wenjing","family":"Chang","sequence":"first","affiliation":[{"name":"School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, China"},{"name":"National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Chengdu 610031, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Xu","sequence":"additional","affiliation":[{"name":"National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Chengdu 610031, China"},{"name":"School of Mathematics, Southwest Jiaotong University, Chengdu 610031, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shuwei","family":"Chen","sequence":"additional","affiliation":[{"name":"National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Chengdu 610031, China"},{"name":"School of Mathematics, Southwest Jiaotong University, Chengdu 610031, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2019,2,11]]},"reference":[{"key":"ref_1","unstructured":"Barranco, M., and Cook, S.A. (1971, January 3\u20135). The complexity of theorem-proving procedures. Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, ShakerHeights, OH, USA."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/j.artint.2012.08.001","article-title":"Planning as satisfiabiIity: Heuristics","volume":"193","author":"Rintanen","year":"2012","journal-title":"Artif. Intell."},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1613\/jair.4231","article-title":"Property directed reachability for automated planning","volume":"50","author":"Suda","year":"2014","journal-title":"J. Artif. Intell. Res."},{"key":"ref_4","doi-asserted-by":"crossref","unstructured":"Konev, B., and Lisitsa, A. (2014, January 14\u201317). A SAT Attack on the Erd\u0151s Discrepancy Conjecture. Proceedings of the Theory and Applications of Satisfiability Testing-SAT 2014, Vienna, Austria.","DOI":"10.1007\/978-3-319-09284-3_17"},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Gutin, G., Kratsch, S., and Wahlstrom, M. (2014, January 10\u201312). Polynomial Kernels and User Reductions for the Workflow Satisfiability Problem. Proceedings of the International Symposium on Parameterized and Exact Computation, Wroclaw, Poland.","DOI":"10.1007\/978-3-319-13524-3_18"},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Goldberg, A., Wang, T.C., and Zimmerman, D. (1994, January 27\u201330). Applications of feasible path analysis to program testing. Proceedings of the ACM Sigsoft International Symposium on Software Testing and Analysis, Seattle, WA, USA.","DOI":"10.1145\/186258.186523"},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem-proving","volume":"5","author":"Davis","year":"1962","journal-title":"Commun. ACM"},{"key":"ref_8","unstructured":"Marques-Silva, J., and Sakallah, K.A. (1996, January 14\u201318). Grasp: A new search algorithm for satisfiability. Proceedings of the International Conference on Computer-Aided Design, Los Alamitos, CA, USA."},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Zhang, H. (1997, January 13\u201317). SATO: An efficient propositional prover. Proceedings of the 14th International Conference on Automated Deduction, Townsville, Australia.","DOI":"10.1007\/3-540-63104-6_28"},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Moskewiez, M., and Madigan, C. (2001, January 15\u201318). Chaff: Engineering an efficient SAT solver. Proceedings of the 38th ACM \/IEEE Design Automation Conference, Las Vegas, NV, USA.","DOI":"10.1145\/378239.379017"},{"key":"ref_11","unstructured":"Goldberg, E., and Novikov, Y. (2002, January 10\u201315). BerkMin: A fast and robust sat-solver. Proceedings of the Design Automation and Test, Acropolis, Europe."},{"key":"ref_12","doi-asserted-by":"crossref","unstructured":"Mahajan, Y.S., Fu, Z., and Malik, S. (2004, January 10\u201313). Zchaff2004: An efficient SAT solver. Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, Vancouver, BC, Canada.","DOI":"10.1007\/11527695_27"},{"key":"ref_13","unstructured":"E\u00e9n, N., and S\u00f6rensson, N. (2005, January 5\u20138). An extensible SAT solver. Proceedings of the 6th International Conference on the Theory and Applications of Satisfiability Testing, Portofino, Italy."},{"key":"ref_14","unstructured":"Audemard, G., and Simon, L. (2009, January 9\u201315). Predicting learnt clauses quality in modern SAT solvers. Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, CA, USA."},{"key":"ref_15","unstructured":"Biere, A. (2012, January 17\u201320). Lingeling and friends entering the SAT Challenge 2012. Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing, Trento, Italy."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., and Czarnecki, K. (2016, January 5\u20138). Learning rate based branching heuristic for SAT solvers. Proceedings of the 19th international conference on Theory and applications of satisfiability testing, Bordeaux, France.","DOI":"10.1007\/978-3-319-40970-2_9"},{"key":"ref_17","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., and Czarnecki, K. (September, January 28). An empirical study of branching heuristics through the lens of global learning rate. Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing, Melbourne, Australia."},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Luo, M., Li, C.M., Xiao, F., Many\u00e0, F., and L\u00fc, Z. (2017, January 19\u201325). An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers. Proceedings of the 26th international joint conference on artificial intelligence, Melbourne, Australia.","DOI":"10.24963\/ijcai.2017\/98"},{"key":"ref_19","unstructured":"Pipatsrisawat, K., and Darwiche, A. (2007, January 28\u201331). A lightweight component caching scheme for satisfiability solvers. Proceedings of the 10th international conference on Theory and applications of satisfiability testing, Lisbon, Portugal."},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Biere, A. (2008, January 25\u201328). Adaptive restart strategies for conflict driven sat solvers. Proceedings of the 11th international conference on Theory and applications of satisfiability testing, Guangzhou, China.","DOI":"10.1007\/978-3-540-79719-7_4"},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/978-3-642-21581-0_18","article-title":"Between restarts and backjumps","volume":"6695","author":"Ramos","year":"2011","journal-title":"Lect. Notes Comput. Sci."},{"key":"ref_22","first-page":"133","article-title":"Reusing the assignment trail in CDCL solvers","volume":"5","author":"Ramos","year":"2011","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Jiang, C., and Zhang, T. (2013, January 12\u201317). Partial backtracking in cdcl solvers. Proceedings of the 19th international conference on Logic for Programming, Artificial Intelligence, and Automated Reasoning, Stellenbosch, South Africa.","DOI":"10.1007\/978-3-642-45221-5_33"},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/j.entcs.2005.07.018","article-title":"Adaptive application of SAT solving techniques","volume":"144","author":"Shacham","year":"2006","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"ref_25","unstructured":"Siddqi, S., and Huang, J. (2015, January 24\u201327). Multi-SAT: An adaptive SAT solver. Proceedings of the 18th international conference on Theory and applications of satisfiability testing, Austin, TX, USA."},{"key":"ref_26","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.H., and Malik, S. (2001, January 4\u20138). Efficient conflict driven learning in a boolean satisfiability solver. Proceedings of the 2001 IEEE\/ACM International Conference on Computer-Aided Design, San Jose, CA, USA."},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Gomes, C.P., Selman, B., and Crato, N. (1997, January 4\u20137). Heavy-tailed distributions in combinatorial search. Proceedings of the International Conference on Principles and Practice of Constraint Programming, Linz, Austria.","DOI":"10.1007\/BFb0017434"},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1016\/0020-0190(93)90029-9","article-title":"Optimal speedup of las vegas algorithms","volume":"47","author":"Luby","year":"1993","journal-title":"Inf. Process. Lett."},{"key":"ref_29","unstructured":"Pipatsrisawat, K., and Darwiche, A. (2007). Rsat 2.0: Sat Solver Description, Automated Reasoning Group, Computer Science Department, UCLA. Technical Report D-153."},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Audemard, G., and Simon, L. (2012, January 14\u201318). Refining restarts strategies for SAT and UNSAT. Proceedings of the Principles and Practice of Constraint Programming, Qu\u00e9bec City, QC, Canada.","DOI":"10.1007\/978-3-642-33558-7_11"},{"key":"ref_31","unstructured":"Biere, A., and Fr\u00f6hlich, A. (2015, January 24\u201327). Evaluating cdcl restarts schemes. Proceedings of the Sixth Pargmatics of SAT workshop, Austin, TX, USA."},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"Nejati, S., Liang, J.H., and Ganesh, V. (2017, January 22\u201323). Adaptive restart and CEGAR-based solver for inverting cryptographic hash functions. Proceedings of the Working Conference on Verified Software: Theories, Tools, and Experiments, Heidelberg, Germany.","DOI":"10.1007\/978-3-319-72308-2_8"},{"key":"ref_33","unstructured":"Oh, C. (2016). Improving SAT Solvers by Exploiting Empirical Characteristics of CDCL. [Ph.D. Dissertation, New York University]."}],"container-title":["Symmetry"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-8994\/11\/2\/197\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T12:31:08Z","timestamp":1760185868000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-8994\/11\/2\/197"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,11]]},"references-count":33,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2019,2]]}},"alternative-id":["sym11020197"],"URL":"https:\/\/doi.org\/10.3390\/sym11020197","relation":{},"ISSN":["2073-8994"],"issn-type":[{"type":"electronic","value":"2073-8994"}],"subject":[],"published":{"date-parts":[[2019,2,11]]}}}