The concept of redundancy in SAT lead to more expressive and powerful proof search techniques, e.g. able to express various inprocessing techniques, and to interesting hierarchies of proof systems [Heule et.al’20, Buss-Thapen’19].
We propose a general way to integrate redundancy rules in MaxSAT, that is we define MaxSAT variants of proof systems such as SPR, PR, SR, and others. The main difference compared to the recent alternative approach in [Ihalainen et.al’22] is that our redundancy rules are polynomially checkable. We discuss the strength of the systems introduced and we give a short cost-SR proof that any assignment for the weak pigeonhole principle $\mathrm{PHP}^m_n$ falsifies at least $m - n$ clauses.