将ILP预处理融入MaxSAT求解，显著提升6大顶尖求解器性能。
Integer Linear Programming Preprocessing for Maximum Satisfiability
- 把ILP预处理技术深度嵌入MaxSAT求解流程
- 使6个顶尖求解器中有5个性能提升，最优者多解15个实例
- 适合需要高效求解MaxSAT的工业优化与验证场景
最大可满足性问题（MaxSAT）是众多实际应用中的核心优化挑战。近期的MaxSAT评测中，多数求解器已将其组合进求解器组合（portfolio）中使用整数线性规划（ILP）求解器。然而，有效的组合策略需要大量调优工作，且受限于特定评测基准。本文提出一种方法，将ILP预处理技术完全集成到MaxSAT求解流程中，并研究其对顶级求解器的影响。实验结果表明，该方法帮助6个最先进的MaxSAT求解器中的5个实现性能提升，尤其在未加权赛道2024年冠军求解器WMaxCDCL-OpenWbo1200上，成功多求解15个实例。
原文摘要 · Abstract (English)
The Maximum Satisfiability problem (MaxSAT) is a major optimization challenge with numerous practical applications. In recent MaxSAT evaluations, most MaxSAT solvers have incorporated an Integer Linear Programming (ILP) solver into their portfolios. However, a good portfolio strategy requires a lot of tuning work and is limited to the profiling benchmark. This paper proposes a methodology to fully integrate ILP preprocessing techniques into the MaxSAT solving pipeline and investigates the impact on the top-performing MaxSAT solvers. Experimental results show that our approach helps to improve 5 out of 6 state-of-the-art MaxSAT solvers, especially for WMaxCDCL-OpenWbo1200, the winner of the MaxSAT evaluation 2024 on the unweighted track, which is able to solve 15 additional instances using our methodology.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。