Max-SAT的新推理规则
New Inference Rules for Max-SAT
摘要：
与SAT求解器相比，精确Max-SAT求解器在证明树的每个节点上应用很少的推理。常用的SAT推理规则（如单位传播）会产生一个保留可满足性的简化公式，但不幸的是，解决简化公式的Max-SAT问题并不等同于解决原始公式。在本文中，我们定义了一些原始的推理规则，除了被有效地应用，转换的Max-SAT实例到等价的Max-SAT实例，更容易解决。规则的合理性，可以被看作是适应最大SAT的单位分辨率的改进，通过整数规划变换以一种新颖而简单的方式被证明。为了找出推理规则在实践中的强大功能，我们开发了一个新的Max-SAT求解器，称为MaxSatz，它包含了这些规则，并进行了实验研究。结果提供了经验证据，MaxSatz是非常有竞争力的，至少在随机Max-2SAT，随机Max-3SAT，Max-Cut和Graph 3着色实例上，以及在Max-SAT Evaluation 2006的基准测试中。
英文摘要：
Exact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability but, unfortunately, solving the Max-SAT problem for the simplified formula is not equivalent to solving it for the original formula. In this paper, we define a number of original inference rules that, besides being applied efficiently, transform Max-SAT instances into equivalent Max-SAT instances which are easier to solve. The soundness of the rules, that can be seen as refinements of unit resolution adapted to Max-SAT, are proved in a novel and simple way via an integer programming transformation. With the aim of finding out how powerful the inference rules are in practice, we have developed a new Max-SAT solver, called MaxSatz, which incorporates those rules, and performed an experimental investigation. The results provide empirical evidence that MaxSatz is very competitive, at least, on random Max-2SAT, random Max-3SAT, Max-Cut, and Graph 3-coloring instances, as well as on the benchmarks from the Max-SAT Evaluation 2006.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
