The survey propagation (SP) algorithm has been shown to work well on large instances of the random 3-SAT problem near its phase transition. It was shown that SP estimates marginals over covers that represent clusters of solutions. The SP-y algorithm generalizes SP to work on the maximum satisfiability (Max-SAT) problem, but the cover interpretation of SP does not generalize to SP-y. In this paper, we formulate the relaxed survey propagation (RSP) algorithm, which extends the SP algorithm to apply to the weighted Max-SAT problem. We show that RSP has an interpretation of estimating marginals over covers violating a set of clauses with minimal weight. This naturally generalizes the cover interpretation of SP. Empirically, we show that RSP outperforms SP-y and other state-of-the-art Max-SAT solvers on random Max-SAT instances. RSP also outperforms state-of-the-art weighted Max-SAT solvers on random weighted Max-SAT instances.
Approximating the Backbone in the Weighted Maximum Satisfiability Problem
School of Software, Dalian University of Technology（大连理工大学软件学院）；The State Key Laboratory of Computer Science, Institute of Software, CAS（中国科学院软件研究所计算机科学国家重点实验室）
加权最大可满足性问题（weighted Maximum Satisfiability problem，简称MAX-SAT）是一个NP难问题，在人工智能中有着广泛的应用。主干作为一种有效的启发式设计工具，已被应用于许多NP难问题的启发式设计中。本文研究了在加权MAX-SAT中检索骨干的计算复杂性，并提出了一种新的算法来解决这个问题。我们证明了在以下假设下检索完整的主干是困难的。此外，它是棘手的，以恢复一个固定的骨干部分，以及。在此基础上，提出了一种基于Walksat算子的骨干引导局部搜索算法（BGLS）。BGLS包括两个阶段：第一阶段从局部最优解中抽取骨干信息，骨干阶段在骨干的指导下进行局部搜索。在基准测试上的大量实验结果表明，BGLS在解的质量和运行时间方面都优于现有的算法。
Scaling up Hybrid Probabilistic Inference with Logical and Arithmetic Constraints via Message Passing
University of California, Los Angeles（加州大学洛杉矶分校）；University of Trento（特伦托大学）；Academy of Mathematics and Systems Science, Chinese Academy of Sciences（中国科学院数学与系统科学研究院）
加权模型集成（Weighted Model Integration，简称WIM）是一个非常吸引人的概率推理框架：它允许通过可满足性模理论（Satisfiability Modulo Theories，简称SMT）的语言来表达变量既连续又离散的真实世界问题的复杂依赖关系，以及计算具有复杂逻辑和算术约束的概率查询。然而，现有的非线性规划求解器还没有准备好扩展到这些问题。它们要么完全忽略了问题的内在依赖结构，要么局限于限制性太强的结构。为了缩小这一差距，我们推导出一个因式分解的形式主义，使我们能够设计一个可扩展的基于消息传递，MP-BSSOVER。也就是说，MP-SVM是第一个SVM求解器，它允许：1）对整个树结构的SVM问题进行精确推理; 2）在线性时间内计算所有边缘密度; 3）摊销查询间的推理。实验结果表明，我们的求解器显着优于现有的非线性规划求解器在一个大的基准集。
Enhancing Local Search for MaxSAT with Deep Differentiation Clause Weighting
School of Computer Science, South China Normal University, Guangzhou, China（计算机科学学院，华南师范大学，广州，中国）；School of Artificial Intelligence, South China Normal University, Foshan, China（人工智能学院，华南师范大学，佛山，中国）
