A rank lower bound for cutting planes proofs of Ramsey's theorem
2013 (English)In: Theory and Applications of Satisfiability Testing – SAT 2013: 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings, Springer, 2013, 351-364 p.Conference paper (Refereed)
Ramsey's Theorem is a cornerstone of combinatorics and logic. In its simplest formulation it says that there is a function r such that any simple graph with r(k,s) vertices contains either a clique of size k or an independent set of size s. We study the complexity of proving upper bounds for the number r(k,k). In particular we focus on the propositional proof system cutting planes; we prove that the upper bound "r(k,k) ≤ 4k" requires cutting planes proof of high rank. In order to do that we show a protection lemma which could be of independent interest.
Place, publisher, year, edition, pages
Springer, 2013. 351-364 p.
, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 7962 LNCS
Combinatorics, Cutting planes, Independent set, Lower bounds, Propositional proof systems, Ramsey's theorem, Upper Bound, Artificial intelligence, Computer science, Formal logic
IdentifiersURN: urn:nbn:se:kth:diva-134088DOI: 10.1007/978-3-642-39071-5_26ScopusID: 2-s2.0-84879905485ISBN: 978-364239070-8OAI: oai:DiVA.org:kth-134088DiVA: diva2:664522
16th International Conference on Theory and Applications of Satisfiability Testing, SAT 2013; Helsinki; Finland; 8 July 2013 through 12 July 2013
FunderEU, European Research Council
QC 201311152013-11-152013-11-152013-11-15Bibliographically approved