On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems

The propositional proof system Sherali-Adams (SA) has polynomial-size proofs of the pigeonhole principle (PHP). Similarly, the Nullstellensatz (NS) proof system has polynomial size proofs of the bijective (i.e. both functional and onto) pigeonhole principle (ofPHP). We characterize the strength of these algebraic proof systems in terms of Boolean proof systems the following way. We show that SA (resp. NS over Z) with unary coefficients lies strictly between tree-like resolution and tree-like depth-1 Frege + PHP (resp. ofPHP). We introduce weighted versions of PHP and ofPHP, resp. wtPHP and of-wtPHP and we show that SA (resp. NS over Z) lies strictly between resolution and tree-like depth-1 Frege + wtPHP (resp. of-wtPHP). We also show analogue results for “depth-d” versions of SA and NS.