科学研究 / 科研进展

大规模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 )授予金牌。