Abstract
It is well-known that Resolution proofs can be efficiently simulated by Sherali-Adams (SA) proofs. We show, however, that any such simulation needs to exploit huge coefficients: Resolution cannot be efficiently simulated by SA when the coefficients are written in unary. We also show that Reversible Resolution (a variant of MaxSAT Resolution) cannot be efficiently simulated by Nullstellensatz (NS). These results can be interpreted in the language of total NP search problems. We show that PPADS, PPAD, SOPL are captured by unary-SA, unary-NS, and Reversible Resolution, respectively. Consequently, relative to an oracle, PLS PPADS and SOPL PPA.