最大可满足性问题的局部搜索算法

The maximum satisfiability problem (MaxSAT) is the optimization version of the satisfiability problem (SAT). The idea is that sometimes not all restrictions of a problem can be satisfied, and we try to satisfy the maximum number of them. MaxSAT is an important problem from both a theoretical and a practical point of view. Many real world applications can be naturally encoded into MaxSAT. MaxSAT is an NP hard problem, and practical algorithms for this problem mainly fall into two types: complete algorithms and incomplete algorithms. Complete algorithms guarantee the optimality of the solutions they find, but may fail to find a good solution within reasonable time for large instances. Incomplete algorithms, mainly including local search algorithms, cannot guarantee the optimality of their solutions, but they may find high-quality solutions quickly even for large instances. Local search MaxSAT algorithms perform well on random instances, but they have poor performance on structured instances generated from industry problems. This project will study local search algorithms for solving structured MaxSAT instances including Partial MaxSAT instances, and the developed algorithms will be evaluated on the standard benchmarks and compared with state of the art MaxSAT algorithms.

最大可满足性问题（MaxSAT）是可满足性问题（SAT）的优化版本。对于约束问题，有时不可能满足所有约束，MaxSAT问题就是考虑满足尽可能多的约束。解决MaxSAT问题不仅有重要的理论意义，也有重要的现实意义。许多现实应用问题都可以自然地转化为MaxSAT问题。MaxSAT是NP难问题，求解该问题的方法可分为完备算法和不完备算法。完备算法保证求得的解是最优的，但对大规模的实例往往会失效。不完备算法，主要指局部搜索算法，不能保证解的最优性，但较快找到高质量的解，即使对大规模实例也有效。局部搜索MaxSAT算法虽然对随机实例有很好的性能，但他们对于从工业界产生的结构化实例的性能差强人意。本项目主要研究局部搜索算法求解结构化MaxSAT实例包括Partial MaxSAT问题实例，所开发的算法将在权威测试集上进行评估，也和当前最好的MaxSAT算法进行比较。

最大可满足性问题（Maximum Satisfiability，简称MaxSAT）是一个基本的约束优化问题。在MaxSAT问题中，约束以子句的形式出现，而MaxSAT问题的目标就是找到一组变量赋值同时满足最多的子句。许多现实应用的问题都可以很自然地转化为MaxSAT问题，尤其是带硬约束和软约束的Partial MaxSAT问题。解决MaxSAT问题不仅有重要的理论意义，也有重要的现实意义。MaxSAT是NP难问题，本课题研究基于局部搜索近似求解MaxSAT问题的算法，尤其注重对大规模工业实例的求解。我们设计了针对Partial MaxSAT问题及其加权版本的高效局部搜索算法，并提出预赋值技术改进算法对工业实例的求解性能。我们设计了线性复杂度的基于推理的“消元法”，结合该方法和局部搜索，显著提高了局部搜索求解大规模MaxSAT工业实例的性能。在此基础上，我们针对（Weighted）Partial MaxSAT大规模工业实例，设计了基于子句加权方法的轻量级局部搜索算法，该算法可以在较短时间内求得高达千万变量的大规模（Weighted）Partial MaxSAT工业实例的高质量近似解。我们在本课题资助下，共发表论文14篇，课题负责人以一作或通讯作者发表论文10篇，其中有7篇为CCF A类论文，在人工智能顶级期刊Artificial Ingelligence上发表了2篇论文。我们基于设计的算法开发了相应的求解器，参加MaxSAT国际比赛，并获得了多个冠军，包括工业组冠军。在2018年MaxSAT比赛中，我们的求解器获得了不完备组4个比赛项目的其中2项冠军，并在60秒时间限制的Partial MaxSAT比赛项目上，遥遥领先其他求解器。我们的团队在2018年联合逻辑大会奥林匹克上也被授予一枚金牌，肯定我们在MaxSAT方面的成绩。另外，我们的求解器在一些来自现实应用的测试集上也取得了很好的效果，比其他MaxSAT求解器有更好的性能。本课题所研发的算法和技术也被用于实际项目包括意大利银行权限管理系统的优化和腾讯地图语音播报系统的优化。