{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,14]],"date-time":"2025-10-14T00:50:34Z","timestamp":1760403034168,"version":"build-2065373602"},"reference-count":43,"publisher":"MDPI AG","issue":"4","license":[{"start":{"date-parts":[[2021,3,31]],"date-time":"2021-03-31T00:00:00Z","timestamp":1617148800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Algorithms"],"abstract":"<jats:p>The Maximum Satisfiability (Maximum Satisfiability (MaxSAT)) approach is the choice, and perhaps the only one, to deal with most real-world problems as most of them are unsatisfiable. Thus, the search for a complete and consistent solution to a real-world problem is impractical due to computational and time constraints. As a result, MaxSAT problems and solving techniques are of exceptional interest in the domain of Satisfiability (Satisfiability (SAT)). Our research experimentally investigated the performance gains of extending the most recently developed SAT dynamic Initial Weight assignment technique (InitWeight) to handle the MaxSAT problems. Specifically, we first investigated the performance gains of dynamically assigning the initial weights in the Divide and Distribute Fixed Weights solver (DDFW+Initial Weight for Maximum Satisfiability (DDFW+InitMaxSAT)) over Divide and Distribute Fixed Weights solver (DDFW) when applied to solve a wide range of well-known unweighted MaxSAT problems obtained from DIMACS. Secondly, we compared DDFW+InitMaxSAT\u2019s performance against three known state-of-the-art SAT solving techniques: YalSAT, ProbSAT, and Sparrow. We showed that the assignment of dynamic initial weights increased the performance of DDFW+InitMaxSAT against DDFW by an order of magnitude on the majority of problems and performed similarly otherwise. Furthermore, we showed that the performance of DDFW+InitMaxSAT was superior to the other state-of-the-art algorithms. Eventually, we showed that the InitWeight technique could be extended to handling partial MaxSAT with minor modifications.<\/jats:p>","DOI":"10.3390\/a14040115","type":"journal-article","created":{"date-parts":[[2021,3,31]],"date-time":"2021-03-31T10:24:33Z","timestamp":1617186273000},"page":"115","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Dynamic Initial Weight Assignment for MaxSAT"],"prefix":"10.3390","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8013-7151","authenticated-orcid":false,"given":"Abdelraouf","family":"Ishtaiwi","sequence":"first","affiliation":[{"name":"Department of Data Science and Artificial Intelligence, Faculty of Information Technology, University of Petra, Amman 317, Jordan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2422-0297","authenticated-orcid":false,"given":"Qasem","family":"Abu Al-Haija","sequence":"additional","affiliation":[{"name":"Department of Data Science and Artificial Intelligence, Faculty of Information Technology, University of Petra, Amman 317, Jordan"}]}],"member":"1968","published-online":{"date-parts":[[2021,3,31]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/1811129.1811130","article-title":"A Terminological Proposal","volume":"6","author":"Knuth","year":"1974","journal-title":"SIGACT News"},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Cook, S.A. (1971). The Complexity of Theorem-proving Procedures. Proceedings of the Third Annual ACM Symposium on Theory of Computing, ACM.","DOI":"10.1145\/800157.805047"},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/BF02241270","article-title":"Algorithms for the maximum satisiability problem","volume":"44","author":"Hansen","year":"1990","journal-title":"Computing"},{"key":"ref_4","unstructured":"Selman, B., and Kautz, H.A. (1993, January 11\u201315). An Empirical Study of Greedy Local Search for Satisfiability Testing. Proceedings of the Eleventh National Conference on Artificial Intelligence, Washington, DC, USA."},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Barrere, M., and Hankin, C. (2020). MaxSAT Evaluation 2020\u2014Benchmark: Identifying Maximum Probability Minimal Cut Sets in Fault Trees. arXiv.","DOI":"10.1109\/DSN-S50200.2020.00029"},{"key":"ref_6","first-page":"129","article-title":"MSCG: Robust Core-Guided MaxSAT Solving","volume":"9","author":"Morgado","year":"2014","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"ref_7","first-page":"53","article-title":"RC2: An Efficient MaxSAT Solver","volume":"11","author":"Ignatiev","year":"2019","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1287\/ijoc.1.3.190","article-title":"Tabu Search\u2014Part I","volume":"1","author":"Glover","year":"1989","journal-title":"ORSA J. Comput."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1016\/0305-0548(86)90048-1","article-title":"Future paths for integer programming and links to artificial intelligence","volume":"13","author":"Glover","year":"1986","journal-title":"Comput. Oper. Res."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1111\/j.1540-5915.1977.tb01074.x","article-title":"Heuristics for integer programming using surrogate constraints","volume":"8","author":"Glover","year":"1977","journal-title":"Decis. Sci."},{"key":"ref_11","unstructured":"Goldberg, D.E. (1989). Genetic Algorithms in Search, Optimization and Machine Learning, Addison-Wesley Longman Publishing Co., Inc.. [1st ed.]."},{"key":"ref_12","doi-asserted-by":"crossref","unstructured":"Amin, S., and Fernandez-Villacanas, J.L. (1997, January 2\u20134). Dynamic local search. Proceedings of the Second International Conference On Genetic Algorithms In Engineering Systems: Innovations And Applications, Glasgow, UK.","DOI":"10.1049\/cp:19971168"},{"key":"ref_13","unstructured":"Wu, Z., and Wah, B.W. (August, January 30). An Efficient Global-Search Strategy in Discrete Lagrangian Methods for Solving Hard Satisfiability Problems. Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence, Austin, TX, USA."},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Van Hentenryck, P. (2002). Scaling and Probabilistic Smoothing: Efficient Dynamic Local Search for SAT. Principles and Practice of Constraint Programming\u2014CP 2002, Springer.","DOI":"10.1007\/3-540-46135-3"},{"key":"ref_15","unstructured":"Thornton, J., Pham, D.N., Bain, S., and Ferreira, V. (2004, January 25\u201329). Additive versus Multiplicative Clause Weighting for SAT. Proceedings of the 19th National Conference on Artificial Intelligence, San Jose, CA, USA."},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0167-6377(89)90002-3","article-title":"A Probabilistic Heuristic for a Computationally Difficult Set Covering Problem","volume":"8","author":"Feo","year":"1989","journal-title":"Oper. Res. Lett."},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Louren\u00e7o, H.R., Martin, O.C., and St\u00fctzle, T. (2010). Iterated Local Search: Framework and Applications. Handbook of Metaheuristics, Springer.","DOI":"10.1007\/978-1-4419-1665-5_12"},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Dorigo, M., and St\u00fctzle, T. (2004). Ant Colony Optimization, Bradford Company.","DOI":"10.7551\/mitpress\/1290.001.0001"},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Effatparvar, M., Aghayi, S., Asadzadeh, V., and Dashti, Y. (2016, January 25\u201327). Swarm Intelligence Algorithm for Job Scheduling in Computational Grid. Proceedings of the 2016 7th International Conference on Intelligent Systems, Modelling and Simulation (ISMS), Bangkok, Thailand.","DOI":"10.1109\/ISMS.2016.25"},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/TITS.2017.2688132","article-title":"Application of Evolutionary Computation for Berth Scheduling at Marine Container Terminals: Parameter Tuning Versus Parameter Control","volume":"19","author":"Dulebenets","year":"2018","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"134743","DOI":"10.1109\/ACCESS.2020.3010176","article-title":"An Optimization Model and Solution Algorithms for the Vehicle Routing Problem With a \u201cFactory-in-a-Box\u201d","volume":"8","author":"Pasha","year":"2020","journal-title":"IEEE Access"},{"key":"ref_22","unstructured":"Morris, P. (1993, January 11\u201315). The Breakout Method for Escaping from Local Minima. Proceedings of the Eleventh National Conference on Artificial Intelligence, Washington, WA, USA."},{"key":"ref_23","unstructured":"Selman, B., and Kautz, H. (1993). Domain-Independent Extensions to GSAT: Solving Large Structured Satisfiability Problems. Proceedings of the 13th International Joint Conference on Artificial Intelligence\u2014Volume 1, Morgan Kaufmann Publishers Inc."},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"Ishtaiwi, A., Alshahwan, F., Jamal, N., Hadi, W., and AbuArqoub, M. (2021). A Dynamic Clause Specific Initial Weight Assignment for Solving Satisfiability Problems Using Local Search. Algorithms, 14.","DOI":"10.3390\/a14010012"},{"key":"ref_25","unstructured":"Biere, A. (2014, January 14\u201317). Yet another local search solver and lingeling and friends entering the SAT competition 2014. Proceedings of the SAT Competition 2014, Vienna, Austria."},{"key":"ref_26","first-page":"302","article-title":"Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses","volume":"Volume 8561","author":"Sinz","year":"2014","journal-title":"Proceedings of the Theory and Applications of Satisfiability Testing\u2014SAT 2014\u201417th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014"},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Balint, A., and Fr\u00f6hlich, A. (2010). Improving Stochastic Local Search for SAT with a New Probability Distribution. Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing, Springer.","DOI":"10.1007\/978-3-642-14186-7_3"},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"van Beek, P. (2005). Neighborhood Clause Weight Redistribution in Local Search for SAT. Principles and Practice of Constraint Programming\u2014CP 2005, Springer.","DOI":"10.1007\/11564751"},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Hoos, H.H., and St\u00fctzle, T. (2015). Stochastic Local Search Algorithms: An Overview. Springer Handbook of Computational Intelligence, Springer.","DOI":"10.1007\/978-3-662-43505-2_54"},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1287\/opre.39.3.378","article-title":"Optimization by Simulated Annealing: An Experimental Evaluation; Part II, Graph Coloring and Number Partitioning","volume":"39","author":"Johnson","year":"1991","journal-title":"Oper. Res."},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/BF00940812","article-title":"Thermodynamical approach to the traveling salesman problem: An efficient simulation algorithm","volume":"45","year":"1985","journal-title":"J. Optim. Theory Appl."},{"key":"ref_32","unstructured":"Fischler, M.A., and Firschein, O. (1987). Optimization by Simulated Annealing. Readings in Computer Vision, Morgan Kaufmann."},{"key":"ref_33","doi-asserted-by":"crossref","first-page":"874","DOI":"10.18178\/ijmlc.2019.9.6.886","article-title":"Weight Resets in Local Search for SAT","volume":"9","author":"Ishtaiwi","year":"2019","journal-title":"Int. J. Mach. Learn. Comput."},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"Luo, C., Cai, S., Wu, W., and Su, K. (2014, January 27\u201331). Double Configuration Checking in Stochastic Local Search for Satisfiability. Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, Qu\u00e9bec, QC, Canada.","DOI":"10.1609\/aaai.v28i1.9110"},{"key":"ref_35","first-page":"1014","article-title":"Clause States Based Configuration Checking in Local Search for Satisfiability","volume":"45","author":"Luo","year":"2015","journal-title":"IEEE Trans. Cybernetics"},{"key":"ref_36","doi-asserted-by":"crossref","unstructured":"Sinz, C., and Egly, U. (2014, January 14\u201317). Theory and Applications of Satisfiability Testing. Proceedings of the SAT 2014\u201417th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria. Lecture Notes in Computer Science.","DOI":"10.1007\/978-3-319-09284-3"},{"key":"ref_37","unstructured":"(September, January 28). Theory and Applications of Satisfiability Testing. Proceedings of the SAT 2017\u201420th International Conference, Melbourne, VIC, Australia. Lecture Notes in Computer Science."},{"key":"ref_38","doi-asserted-by":"crossref","unstructured":"Janota, M., and Lynce, I. (2019, January 9\u201312). Theory and Applications of Satisfiability Testing. Proceedings of the SAT 2019\u201422nd International Conference, SAT 2019, Lisbon, Portugal. Lecture Notes in Computer Science.","DOI":"10.1007\/978-3-030-24258-9"},{"key":"ref_39","doi-asserted-by":"crossref","unstructured":"Pulina, L., and Seidl, M. (2020, January 3\u201310). Theory and Applications of Satisfiability Testing. Proceedings of the SAT 2020\u201423rd International Conference, Alghero, Italy. Lecture Notes in Computer Science.","DOI":"10.1007\/978-3-030-51825-7"},{"key":"ref_40","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1155\/2015\/637809","article-title":"A Variable Depth Search Algorithm for Binary Constraint Satisfaction Problems","volume":"2015","author":"Bouhmala","year":"2015","journal-title":"Math. Probl. Eng."},{"key":"ref_41","doi-asserted-by":"crossref","unstructured":"Orgun, M.A., and Thornton, J. (2007). Weight Redistribution for Unweighted MAX-SAT. AI 2007: Advances in Artificial Intelligence, Springer.","DOI":"10.1007\/978-3-540-76928-6"},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.artint.2016.07.006","article-title":"New local search methods for partial MaxSAT","volume":"240","author":"Cai","year":"2016","journal-title":"Artif. Intell."},{"key":"ref_43","doi-asserted-by":"crossref","unstructured":"Biere, A., and Gomes, C.P. (2006). On Solving the Partial MAX-SAT Problem. Theory and Applications of Satisfiability Testing\u2014SAT 2006, Springer.","DOI":"10.1007\/11814948"}],"container-title":["Algorithms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1999-4893\/14\/4\/115\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T14:10:46Z","timestamp":1760364646000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1999-4893\/14\/4\/115"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3,31]]},"references-count":43,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2021,4]]}},"alternative-id":["a14040115"],"URL":"https:\/\/doi.org\/10.3390\/a14040115","relation":{},"ISSN":["1999-4893"],"issn-type":[{"type":"electronic","value":"1999-4893"}],"subject":[],"published":{"date-parts":[[2021,3,31]]}}}