Rank Complexity Gap for Lovasz-Schrijver and Sherali-Adams Proof Systems

We prove a dichotomy theorem for the rank of the uniformly generated (i.e. expressible in First-Order (170) Logic) propositional tautologies in both the Lovdsz-Schrijver (LS) and Sherali-Adams (SA) proof systems. More precisely, we first show that the propositional translations of FO formulae that are universally trite, i.e. hold in all finite and infinite models, have LS proofs whose rank is constant, independently from the size of the (finite) universe. In contrast to that, we prove that the propositional formulae that hold in all finite models but fail in some infinite structure require proofs whose SA rank grows poly-logarithmically with the size of the universe. Up to now, this kind of so-called "Complexity Gap" theorems have been known for Tree-like Resolution and, in some-how restricted forms, for the Resolution and Nullstellensatz proof systems. As far as we are aware, this is the first time the Sherali-Adams lift-and-project method has been considered as a propositional proof system. An interesting feature of the SA proof system is that it is static and rank-preserving simulates LS, the Lovisz-Schrijver proof system without semidefinite cuts.