大规模Partial MaxSAT问题的高效求解

Zhendong Lei, Shaowei Cai (2018): Solving (Weighted) Partial MaxSAT by Dynamic Local Search for SAT. IJCAI 2018: 1346-1352

背景：最大可满足性问题（Maximum Satisfiability，简称MaxSAT）是一个基本的约束优化问题。许多现实应用的问题都可以很自然地转化为MaxSAT问题，尤其是带硬约束和软约束的Partial MaxSAT问题。解决MaxSAT问题不仅有重要的理论意义，也有重要的现实意义。

科学难题：MaxSAT是NP难问题，对于大规模实例一般难以在短时间内精确求解。局部搜索算法是一种主要的近似求解方法，在只有软子句的MaxSAT问题上已经取得很好的进展，但是对于带硬约束和软约束的Partial MaxSAT问题的大规模工业实例，局部搜索算法效果还不好，对一些工业实例不能在合理时间内求出可行解。

重要突破：Partial MaxSAT问题带有明显的问题结构，如何利用硬约束和软约束的区别是算法设计的关键。以前的局部搜索算法设计了专门的机制，对两种约束分别定义评分函数和加权机制，取得了一定的进展。但是，这些技术需要较为复杂的数据结构，使得算法的单步复杂度较高，限制了其在大规模实例上性能。我们 针对（Weighted）Partial MaxSAT大规模工业实例，设计了轻量级的局部搜索算法。该算法不需要维护复杂的数据结构，而是把硬约束和软约束的区别通过一个自适应的加权机制利用起来，算法单步速度较快，可以在较短时间内求得高达千万变量规模的（Weighted）Partial MaxSAT工业实例的高质量近似解。由此开发的SATLike算法在2018年MaxSAT比赛中取得两个冠军，尤其是在60秒时间限制的PMS比赛项目上，遥遥领先其他求解器。我们的团队也因此被2018年联合逻辑大会奥林匹克(Federated Logic Conference, Oxford, 6-19 July 2018 )授予金牌。