论文标题
要更好地理解（部分加权）MaxSat证明系统
Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems
论文作者
论文摘要
著名SAT问题的优化版本Maxsat在过去十年中引起了很多研究兴趣。受到许多重要应用的动机，并受到现代SAT求解器的成功的启发，研究人员开发了许多MaxSat求解器。由于大多数研究都是算法，因此其意义主要在经验上评估。在本文中，我们希望从更正式的证据复杂性的角度来解决MaxSat。以此目的，我们开始提供基本定义并证明一些基本结果。然后，我们将添加和虚拟的两个原始推理规则添加的效果分析为MaxSat解决方案。我们表明，每次添加使最终的证明系统更强大，虚拟规则捕获了最近提出的循环证明概念。
MaxSAT, the optimization version of the well-known SAT problem, has attracted a lot of research interest in the last decade. Motivated by the many important applications and inspired by the success of modern SAT solvers, researchers have developed many MaxSAT solvers. Since most research is algorithmic, its significance is mostly evaluated empirically. In this paper we want to address MaxSAT from the more formal point of view of Proof Complexity. With that aim we start providing basic definitions and proving some basic results. Then we analyze the effect of adding split and virtual, two original inference rules, to MaxSAT resolution. We show that each addition makes the resulting proof system stronger, with the virtual rule capturing the recently proposed concept of circular proof.
