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.

翻译：MaxSAT是众所周知的SAT问题的优化版,在过去十年中引起了许多研究兴趣。受许多重要应用的激励和现代SAT解答器的成功激励,研究人员开发了许多MaxSAT解答器。由于大多数研究都是算法性的,因此其意义大多是通过经验来评估的。在本文中,我们希望从更正式的证明复杂性的角度来探讨MaxSAT。为了达到这个目的,我们开始提供基本定义并证明一些基本结果。然后我们分析在MaxSAT分辨率中增加分裂和虚拟两个原始推论规则的效果。我们显示,每一项增加都使由此产生的证明系统更加强大,虚拟规则抓住了最近提出的循环证明概念。