Dantchev, Stefan and Martin, Barnaby (2013) 'Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems.', Computational complexity., 22 (1). pp. 191-213.
We prove a dichotomy theorem for the rank of propositional contradictions, uniformly generated from first-order sentences, in both the Lovász-Schrijver (LS) and Sherali-Adams (SA) refutation systems. More precisely, we first show that the propositional translations of first-order formulae that are universally false, that is, fail in all finite and infinite models, have LS proofs whose rank is constant, independent of the size of the (finite) universe. In contrast to that, we prove that the propositional formulae that fail in all finite models, but hold in some infinite structure, require proofs whose SA rank grows polynomially with the size of the universe. Until now, this kind of so-called complexity gap theorem has been known for tree-like Resolution and, in somehow restricted forms, for the Resolution and Nullstellensatz 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 refutation system (since the conference version of this paper, SA has been considered as a refutation system in several further papers). An interesting feature of the SA system is that it simulates LS, the Lovász-Schrijver refutation system without semi-definite cuts, in a rank-preserving fashion.
|Full text:||(AM) Accepted Manuscript|
Download PDF (234Kb)
|Publisher Web site:||https://doi.org/10.1007/s00037-012-0049-1|
|Publisher statement:||The final publication is available at Springer via https://doi.org/10.1007/s00037-012-0049-1.|
|Date accepted:||No date available|
|Date deposited:||27 September 2017|
|Date of first online publication:||06 November 2012|
|Date first made open access:||No date available|
Save or Share this output
|Look up in GoogleScholar|