| Summary: | 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).
<br>
These results have consequences for total 𝖭𝖯 search problems. First, we characterise the classes 𝖯𝖯𝖠𝖣𝖲, 𝖯𝖯𝖠𝖣, 𝖲𝖮𝖯𝖫 by unary-SA, unary-NS, and Reversible Resolution, respectively. Second, we show that, relative to an oracle, 𝖯𝖫𝖲⊈𝖯𝖯𝖯, 𝖲𝖮𝖯𝖫⊈𝖯𝖯𝖠, and 𝖤𝖮𝖯𝖫⊈𝖴𝖤𝖮𝖯𝖫. In particular, together with prior work, this gives a complete picture of the black-box relationships between all classical 𝖳𝖥𝖭𝖯 classes introduced in the 1990s.
|
|---|