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.
翻译:最大可满足性问题(MaxSAT)是一个具有众多实际应用的重要优化挑战。在近期的MaxSAT评测中,大多数MaxSAT求解器已在其算法组合中集成了整数线性规划(ILP)求解器。然而,优秀的组合策略需要大量调优工作,且受限于基准测试集的特性。本文提出一种将ILP预处理技术完全整合到MaxSAT求解流程中的方法,并研究其对顶尖MaxSAT求解器性能的影响。实验结果表明,我们的方法能帮助改进6个当前最优MaxSAT求解器中的5个,特别是对于2024年MaxSAT评测无权重赛道冠军WMaxCDCL-OpenWbo1200,采用本方法后可额外求解15个问题实例。