  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.
