提出新权重策略，让局部搜索更懂PMS与WPMS的区别。
Enhancing Local Search for MaxSAT with Deep Differentiation Clause Weighting
- 针对PMS和WPMS设计不同权重更新规则
- 在多个评测集上超越现有顶尖求解器
- 适合需要高效求解MaxSAT的工程应用
部分最大可满足性（PMS）与加权部分最大可满足性（WPMS）是最大可满足性（MaxSAT）的推广形式，具有广泛的实际应用。近年来，随机局部搜索（SLS）算法在求解（W）PMS方面取得进展，主要集中在条款权重策略的设计。然而，现有方法往往未能充分区分PMS与WPMS，通常对两类实例采用统一的权重更新策略，并忽视了两者之间的关键结构差异。本文首次提出一种新的条款权重更新方案，根据不同的问题类型分别设定更新条件。该方案还引入了一种新的初始化方法，更好地适应两类实例的独特特征。此外，我们设计了一种消解策略，优先满足单位条款和硬条款，有效补充了所提出的权重机制。基于上述方法，我们开发了新的SLS求解器DeepDist。在最近几届MaxSAT评估赛的即时求解赛道基准测试中，DeepDist的表现优于现有顶尖的SLS求解器。特别地，将DeepDist与TT-Open-WBO-Inc结合形成的混合求解器，性能超过了2024年MaxSAT评估赛冠军SPB-MaxSAT-c-Band和SPB-MaxSAT-c-FPS，充分验证了本方法的有效性。代码已公开于https://github.com/jmhmaxsat/DeepDist。
原文摘要 · Abstract (English)
Partial Maximum Satisfiability (PMS) and Weighted Partial Maximum Satisfiability (WPMS) generalize Maximum Satisfiability (MaxSAT), with broad real-world applications. Recent advances in Stochastic Local Search (SLS) algorithms for solving (W)PMS have mainly focused on designing clause weighting schemes. However, existing methods often fail to adequately distinguish between PMS and WPMS, typically employing uniform update strategies for clause weights and overlooking critical structural differences between the two problem types. In this work, we present a novel clause weighting scheme that, for the first time, updates the clause weights of PMS and WPMS instances according to distinct conditions. This scheme also introduces a new initialization method, which better accommodates the unique characteristics of both instance types. Furthermore, we propose a decimation method that prioritizes satisfying unit and hard clauses, effectively complementing our proposed clause weighting scheme. Building on these methods, we develop a new SLS solver for (W)PMS named DeepDist. Experimental results on benchmarks from the anytime tracks of recent MaxSAT Evaluations show that DeepDist outperforms state-of-the-art SLS solvers. Notably, a hybrid solver combining DeepDist with TT-Open-WBO-Inc surpasses the performance of the MaxSAT Evaluation 2024 winners, SPB-MaxSAT-c-Band and SPB-MaxSAT-c-FPS, highlighting the effectiveness of our approach. The code is available at https://github.com/jmhmaxsat/DeepDist
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。