Equivalence Between Systems Stronger Than Resolution

In recent years there has been an increasing interest in studying proof systems stronger than Resolution, with the aim of building more efficient SAT solvers based on them. In defining these proof systems, we try to find a balance between the power of the proof system (the size of the proofs required to refute a formula) and the difficulty of finding the proofs. Among those proof systems we can mention Circular Resolution, MaxSAT Resolution with Extensions and MaxSAT Resolution with the Dual-Rail encoding. In this paper we study the relative power of those proof systems from a theoretical perspective. We prove that Circular Resolution and MaxSAT Resolution with extension are polynomially equivalent proof systems. This result is generalized to arbitrary sets of inference rules with proof constructions based on circular graphs or based on weighted clauses. We also prove that when we restrict the Split rule (that both systems use) to bounded size clauses, these two restricted systems are also equivalent. Finally, we show the relationship between these two restricted systems and Dual-Rail MaxSAT Resolution.