Abstract
The Divide and Distribute Fixed Weights algorithm (ddfw) is a dynamic local search SAT-solving algorithm that transfers weight from satisfied to falsified clauses in local minima. ddfw is remarkably effective on several hard combinatorial instances. Yet, despite its success, it has received little study since its debut in 2005. In this paper, we propose three modifications to the base algorithm: a linear weight transfer method that moves a dynamic amount of weight between clauses in local minima, an adjustment to how satisfied clauses are chosen in local minima to give weight, and a weighted-random method of selecting variables to flip. We implemented our modifications to ddfw on top of the solver yalsat. Our experiments show that our modifications boost the performance compared to the original ddfw algorithm on multiple benchmarks, including those from the past three years of SAT competitions. Moreover, our improved solver exclusively solves hard combinatorial instances that refute a conjecture on the lower bound of two Van der Waerden numbers set forth by Ahmed et al. (2014), and it performs well on a hard graph-coloring instance that has been open for over three decades.
The authors were supported by NSF grant CCF-2006363. Md Solimul Chowdhury was partially supported by a NSERC Postdoctoral Fellowship.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
To the best of our knowledge, there is no official implementation or binary of original ddfw [16] available.
- 2.
Source code of our system are available at https://github.com/solimul/yal-lin
- 3.
- 4.
The PAR-2 score is defined as the average solving time, while taking 2 * timeout as the time for unsolved instances. A lower score is better.
- 5.
Results for additional experiments with a different seed is available at: https://github.com/solimul/additional-experiments-nfm23/blob/master/additional_results_nfm2023.pdf
References
Aaron Stump, Geoff Sutcliffe, C.T.: StarExec. https://www.starexec.org/starexec/public/about.jsp (2013)
Ahmed, T., Kullmann, O., Snevily, H.S.: On the van der Waerden numbers w(2; 3, t). Discrete Applied Mathematics 174, 27–51 (2014). https://doi.org/10.1016/j.dam.2014.05.007
Balint, A.: Engineering stochastic local search for the satisfiability problem. Ph.D. thesis, University of Ulm (2014)
Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, The Netherlands (2009)
Biere, A.: YalSAT Yet Another Local Search Solver. http://fmv.jku.at/yalsat/ (2010)
Brown, S., Buitrago, P., Hanna, E., Sanielevici, S., Scibek, R., Nystrom, N.: Bridges-2: A platform for rapidly-evolving and data intensive research. In: Association for Computing Machinery, New York, NY, USA. pp. 1–4 (2021)
Cai, S., Luo, C., Su, K.: CCAnr: A configuration checking based local search solver for non-random satisfiability. In: Heule, M., Weaver, S. (eds.) Theory and Applications of Satisfiability Testing - SAT 2015, pp. 1–8. Springer International Publishing, Cham (2015)
Cai, S., Zhang, X., Fleury, M., Biere, A.: Better Decision Heuristics in CDCL through Local Search and Target Phases. Journal of Artificial Intelligence Research 74, 1515–1563 (2022)
Codel, C.R., Heule, M.J.: A Study of Divide and Distribute Fixed Weights and its Variants. In: Pragmatics of SAT 2021 (2021)
Feng, N., Bacchus, F.: Clause size reduction with all-UIP learning. In: Pulina, L., Seidl, M. (eds.) Proceedings of SAT-2020. pp. 28–45 (2020)
Green, B.: New lower bounds for van der Waerden numbers (2021). https://doi.org/10.48550/ARXIV.2102.01543
Gupta, A., Ganai, M.K., Wang, C.: SAT-based verification methods and applications in hardware verification. In: Proceedings of SFM 2006. pp. 108–143 (2006)
Heule, M.J.H., Karahalios, A., van Hoeve, W.: From cliques to colorings and back again. In: Proceedings of CP-2022. pp. 26:1–26:10 (2022)
Heule, M.J.H., Kauers, M., Seidl, M.: New ways to multiply 3x3-matrices. J. Symb. Comput. 104, 899–916 (2019)
Hutter, F., Tompkins, D.A.D., Hoos, H.H.: Scaling and probabilistic smoothing: Efficient dynamic local search for SAT. In: Hentenryck, P.V. (ed.) Proceedings of CP 2002. pp. 233–248 (2002)
Ishtaiwi, A., Thornton, J., Sattar, A., Pham, D.N.: Neighbourhood clause weight redistribution in local search for SAT. In: Proceedings of CP-2005. pp. 772–776. Lecture Notes in Computer Science (2005)
Johnson, D.J., Trick, M.A.: Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, Workshop, October 11–13, 1993. American Mathematical Society, USA (1996)
Kautz, H., Selman, B.: Planning as satisfiability. In: Proceedings of the 10th European Conference on Artificial Intelligence. p. 359–363. ECAI ’92, John Wiley & Sons Inc, USA (1992)
Li, C.M., Li, Y.: Satisfying versus falsifying in local search for satisfiability. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing – SAT 2012. pp. 477–478. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of DAC 2001. pp. 530–535 (2001)
Ostrowski, J., Linderoth, J., Rossi, F., Smriglio, S.: Solving large steiner triple covering problems. Operations Research Letters 39(2), 127–131 (2011)
Schreiber, D., Sanders, P.: Scalable SAT solving in the cloud. In: Li, C.M., Manyà, F. (eds.) Theory and Applications of Satisfiability Testing – SAT 2021. pp. 518–534. Springer International Publishing, Cham (2021)
Selman, B., Kautz, H.A., Cohen, B.: Local search strategies for satisfiability testing. In: Cliques, Coloring, and Satisfiability, Proceedings of a DIMACS Workshop 1993. pp. 521–532 (1993)
Selman, B., Levesque, H.J., Mitchell, D.G.: A new method for solving hard satisfiability problems. In: Proceedings of AAAI 1992. pp. 440–446 (1992)
Silva, J.P.M., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers 48(5), 506–521 (1999)
Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Proceedings of SAT 2009. pp. 244–257 (2009)
Thornton, J., Pham, D.N., Bain, S., Jr., V.F.: Additive versus multiplicative clause weighting for SAT. In: McGuinness, D.L., Ferguson, G. (eds.) Proceedings of AAAI-2004. pp. 191–196 (2004)
Tompkins, D.: Dynamic Local Search for SAT: Design, Insights and Analysis. Ph.D. thesis, The University of British Columbia (2010)
Tompkins, D.: UBCSAT. http://ubcsat.dtompkins.com/home (2010)
van der Waerden, B.L.: Beweis einer baudet’schen vermutung. J. Symb. Comput. 15, 212–216 (1927)
Xindi Zhang, Shaowei Cai, Z.C.: Improving CDCL via Local Search. In: SAT Competition-2021. pp. 42–43 (2021)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Chowdhury, M.S., Codel, C.R., Heule, M.J.H. (2023). A Linear Weight Transfer Rule for Local Search. In: Rozier, K.Y., Chaudhuri, S. (eds) NASA Formal Methods. NFM 2023. Lecture Notes in Computer Science, vol 13903. Springer, Cham. https://doi.org/10.1007/978-3-031-33170-1_27
Download citation
DOI: https://doi.org/10.1007/978-3-031-33170-1_27
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-33169-5
Online ISBN: 978-3-031-33170-1
eBook Packages: Computer ScienceComputer Science (R0)