一种有效求解Max-SAT的逻辑方法
A Logical Approach to Efficient Max-SAT solving
摘要：
加权Max-SAT是SAT的优化版本，许多重要问题可以自然编码。求解加权Max-SAT问题是一个重要的理论和实际问题。近年来，有相当大的兴趣，在寻找有效的解决技术。这项工作的大部分集中在良好的质量下限的计算中使用的分支和绑定DPLL类算法。大多数情况下，这些下限是以程序的方式描述的。因此，很难实现后面的{ \em逻辑}。在本文中，我们介绍了一个原始的Max-SAT框架，强调与经典SAT的并行性。然后，我们扩展了两个基本的SAT求解技术：{ \em search}和{ \em inference}。我们表明，许多算法{ \em技巧}中使用的国家的最先进的最大-SAT求解器很容易表达在{ \em逻辑}方面与我们的框架在一个统一的方式。此外，我们引入了一个原始的搜索算法，执行有限数量的{ \em加权分辨率}在每个访问节点。我们经验比较我们的算法与各种解决方案的几个基准。据我们所知，我们的实验构成了有史以来最全面的Max-sat评估报告，表明我们的算法通常比任何竞争对手快几个数量级。
英文摘要：
Weighted Max-SAT is the optimization version of SAT and many important problems can be naturally encoded as such. Solving weighted Max-SAT is an important problem from both a theoretical and a practical point of view. In recent years, there has been considerable interest in finding efficient solving techniques. Most of this work focus on the computation of good quality lower bounds to be used within a branch and bound DPLL-like algorithm. Most often, these lower bounds are described in a procedural way. Because of that, it is difficult to realize the {\em logic} that is behind. In this paper we introduce an original framework for Max-SAT that stresses the parallelism with classical SAT. Then, we extend the two basic SAT solving techniques: {\em search} and {\em inference}. We show that many algorithmic {\em tricks} used in state-of-the-art Max-SAT solvers are easily expressable in {\em logic} terms with our framework in a unified manner. Besides, we introduce an original search algorithm that performs a restricted amount of {\em weighted resolution} at each visited node. We empirically compare our algorithm with a variety of solving alternatives on several benchmarks. Our experiments, which constitute to the best of our knowledge the most comprehensive Max-sat evaluation ever reported, show that our algorithm is generally orders of magnitude faster than any competitor.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
