{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T17:50:16Z","timestamp":1764784216177,"version":"3.37.3"},"reference-count":27,"publisher":"Oxford University Press (OUP)","issue":"9","license":[{"start":{"date-parts":[[2019,8,15]],"date-time":"2019-08-15T00:00:00Z","timestamp":1565827200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"DOI":"10.13039\/501100004739","name":"Youth Innovation Promotion Association, Chinese Academy of Sciences","doi-asserted-by":"publisher","award":["2017150"],"award-info":[{"award-number":["2017150"]}],"id":[{"id":"10.13039\/501100004739","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,8,20]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Maximum satisfiability (MaxSAT) is the optimization version of the satisfiability (SAT). Partial MaxSAT (PMS) generalizes SAT and MaxSAT by introducing hard and soft clauses, while Weighted PMS (WPMS) is the weighted version of PMS where each soft clause has a weight. These two problems have many important real-world applications. Local search is a popular method for solving (W)PMS. Recently, significant progress has been made in this direction by tailoring local search for (W)PMS, and a representative algorithm is the Dist algorithm. In this paper, we propose two ideas to improve Dist, including a clause-weighting scheme and a variable-selection heuristic. The resulting algorithm is called NuDist. Extensive experiments on PMS and WPMS benchmarks from the MaxSAT Evaluations (MSE) 2016 and 2017 show that NuDist significantly outperforms state-of-the-art local search solvers and performs better than state-of-the-art complete solvers including Open-WBO and WPM3 on MSE 2017 benchmarks. Also, empirical analyses confirm the effectiveness of the proposed ideas.<\/jats:p>","DOI":"10.1093\/comjnl\/bxz063","type":"journal-article","created":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T11:07:25Z","timestamp":1559214445000},"page":"1321-1337","source":"Crossref","is-referenced-by-count":6,"title":["NuDist: An Efficient Local Search Algorithm for (Weighted) Partial MaxSAT"],"prefix":"10.1093","volume":"63","author":[{"given":"Zhendong","family":"Lei","sequence":"first","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China"},{"name":"School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing 101408, China"}]},{"given":"Shaowei","family":"Cai","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China"},{"name":"School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing 101408, China"}]}],"member":"286","published-online":{"date-parts":[[2019,8,15]]},"reference":[{"key":"2020091506340978600_ref1","doi-asserted-by":"crossref","first-page":"360","DOI":"10.1007\/978-3-642-21581-0_29","article-title":"Analyzing the Instances of the Maxsat Evaluation","volume-title":"Theory and Applications of Satisfiability Testing\u2014SAT 2011","author":"Argelich","year":"2011"},{"key":"2020091506340978600_ref2","first-page":"910","article-title":"Solving the Coalition Structure Generation Problem With Maxsat","author":"Liao","year":"2012","journal-title":"IEEE Int. Conf. on Tools With Artificial Intelligence, Athens, Greece"},{"key":"2020091506340978600_ref3","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1016\/j.cor.2016.08.004","article-title":"Maxsat-based large neighborhood search for high school timetabling","volume":"78","author":"Demirovic","year":"2017","journal-title":"Comput. Oper. Res."},{"key":"2020091506340978600_ref4","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/s10479-017-2693-y","article-title":"Modeling and solving staff scheduling with partial weighted maxsat","volume":"275","author":"Demirovic","year":"2019","journal-title":"Ann. Oper. Res."},{"key":"2020091506340978600_ref5","first-page":"252","article-title":"On Solving the Partial MAX-SAT Problem","volume-title":"Proc. of the 9th Int. Conf. of Theory and Applications of Satisfiability Testing (SAT)","author":"Fu","year":"2006"},{"key":"2020091506340978600_ref6","first-page":"59","article-title":"The sat4j library, release 2.2","volume":"7","author":"Berre","year":"2010","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"2020091506340978600_ref7","first-page":"225","article-title":"Solving MAXSAT by Solving a Sequence of Simpler SAT Instances","author":"Davies","year":"2011","journal-title":"Proc. of the 17th Int. Conf. of Principles and Practice of Constraint Programming (CP)"},{"key":"2020091506340978600_ref8","first-page":"95","article-title":"Qmaxsat: a partial max-SAT solver","volume":"8","author":"Koshimura","year":"2012","journal-title":"J. Satisf. Boolean Model. Comput"},{"key":"2020091506340978600_ref9","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/j.artint.2013.01.002","article-title":"SAT-based MaxSAT algorithms","volume":"196","author":"Ans\u00f3tegui","year":"2013","journal-title":"Artif. Intell."},{"key":"2020091506340978600_ref10","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/s10601-013-9146-2","article-title":"Iterative and core-guided MaxSAT solving: a survey and assessment","volume":"18","author":"Morgado","year":"2013","journal-title":"Constraints"},{"key":"2020091506340978600_ref11","doi-asserted-by":"crossref","first-page":"531","DOI":"10.1007\/978-3-319-10428-7_39","article-title":"Incremental Cardinality Constraints for Maxsat","author":"Martins","year":"2014","journal-title":"Proc. of the 20th Int. Conf. of Principles and Practice of Constraint Programming (CP),"},{"key":"2020091506340978600_ref12","first-page":"2717","article-title":"Maximum Satisfiability Using Core-Guided MaxSAT Resolution","volume-title":"Proc. of the 28th AAAI Conf. on Artificial Intelligence (AAAI)","author":"Narodytska","year":"2014"},{"key":"2020091506340978600_ref13","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/j.artint.2017.05.003","article-title":"WPM3: an (in)complete algorithm for weighted partial maxsat","volume":"250","author":"Ans\u00f3tegui","year":"2017","journal-title":"Artif. Intell."},{"key":"2020091506340978600_ref14","first-page":"263","article-title":"Local Search Algorithms for Partial MAXSAT","volume-title":"Proc. of the 14th National Conf. on Artificial Intelligence (AAAI)","author":"Cha","year":"1997"},{"key":"2020091506340978600_ref15","doi-asserted-by":"crossref","first-page":"1830","DOI":"10.1109\/TC.2014.2346196","article-title":"CCLS: an efficient local search algorithm for weighted maximum satisfiability","volume":"64","author":"Luo","year":"2015","journal-title":"IEEE Trans. Comput."},{"key":"2020091506340978600_ref16","first-page":"377","article-title":"Dynamic Constraint Weighting for Over-Constrained Problems","author":"Thornton","year":"1998","journal-title":"Proc. of the 5th Pacific Rim Int. Conf. on Artificial Intelligence (PRICAI)"},{"key":"2020091506340978600_ref17","first-page":"603","article-title":"A Two Level Local Search for MAX-SAT Problems With Hard and Soft Constraints","author":"Thornton","year":"2002","journal-title":"Proc. of the 15th Australian Joint Conf. on Artificial Intelligence (AI)"},{"key":"2020091506340978600_ref18","first-page":"2623","article-title":"Tailoring Local Search for Partial MaxSAT","volume-title":"Proc. of the 28th AAAI Conf. on Artificial Intelligence (AAAI)","author":"Cai","year":"2014"},{"key":"2020091506340978600_ref19","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":"2020091506340978600_ref20","first-page":"571","article-title":"From Decimation to Local Search and Back: A New Approach to Maxsat. Proc. of the Twenty-Sixth Int. Joint Conf. on Artificial Intelligence, IJCAI 2017","author":"Cai","year":"2017"},{"key":"2020091506340978600_ref21","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1016\/j.artint.2016.11.001","article-title":"CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability","volume":"243","author":"Luo","year":"2017","journal-title":"Artif. Intell."},{"key":"2020091506340978600_ref22","first-page":"139","article-title":"Hard Neighboring Variables Based Configuration Checking in Stochastic Local Search for Weighted Partial Maximum Satisfiability","volume-title":"29th IEEE Int. Conf. on Tools With Artificial Intelligence, ICTAI 2017","author":"Chu","year":"2017"},{"key":"2020091506340978600_ref23","first-page":"747","article-title":"Balance Between Complexity and Quality: Local Search for Minimum Vertex Cover in Massive Graphs","author":"Cai","year":"2015","journal-title":"Proc. of the Twenty-Fourth Int. Joint Conf. on Artificial Intelligence, IJCAI 2015"},{"key":"2020091506340978600_ref24","first-page":"191","article-title":"Additive Versus Multiplicative Clause Weighting for SAT","volume-title":"Proc. of the 19th National Conf. on Artificial Intelligence (AAAI)","author":"Thornton","year":"2004"},{"key":"2020091506340978600_ref25","first-page":"1346","article-title":"Solving (Weighted) Partial Maxsat by Dynamic Local Search for SAT","volume-title":"Proc. of the Twenty-Seventh Int. Joint Conf. on Artificial Intelligence, IJCAI 2018","author":"Lei","year":"2018"},{"key":"2020091506340978600_ref26","first-page":"438","article-title":"Open-WBO: A Modular MaxSAT Solver","volume-title":"Proc. of the 17th Int. Conf. of Theory and Applications of Satisfiability Testing","author":"Martins","year":"2014"},{"article-title":"Solving MaxSAT by decoupling optimization and satisfaction","year":"2013","author":"Davies","key":"2020091506340978600_ref27"}],"container-title":["The Computer Journal"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/comjnl\/article-pdf\/63\/9\/1321\/33747619\/bxz063.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/comjnl\/article-pdf\/63\/9\/1321\/33747619\/bxz063.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,15]],"date-time":"2020-09-15T10:35:12Z","timestamp":1600166112000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/comjnl\/article\/63\/9\/1321\/5544159"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,15]]},"references-count":27,"journal-issue":{"issue":"9","published-online":{"date-parts":[[2019,8,15]]},"published-print":{"date-parts":[[2020,8,20]]}},"URL":"https:\/\/doi.org\/10.1093\/comjnl\/bxz063","relation":{},"ISSN":["0010-4620","1460-2067"],"issn-type":[{"type":"print","value":"0010-4620"},{"type":"electronic","value":"1460-2067"}],"subject":[],"published-other":{"date-parts":[[2020,9]]},"published":{"date-parts":[[2019,8,15]]}}}