Having good algorithms to verify tautologies as efficiently as possible
is of prime interest in different fields of computer science.
In this paper we present an algorithm for finding Resolution refutations
based on finding tree-like Res(k) refutations. The algorithm is based on
the one of Beame and Pitassi \cite{BP96} ... more >>>

We resolve two open problems regarding the Sherali-Adams proof system. First, we show that Res(2), which manipulates 2-DNF formulas, is exponentially stronger than Sherali-Adams. This provides a sharp separation in power between Sherali-Adams and the bounded-depth Frege hierarchy, as Sherali-Adams polynomially simulates Resolution. Second, we prove that Sherali-Adams is not ... more >>>