DOI

For any unsatisfiable CNF formula F that is hard to refute in the Resolution proof system, we show that a gadget-composed version of F is hard to refute in any proof system whose lines are computed by efficient communication protocols—or, equivalently, that a monotone function associated with F has large monotone circuit complexity. Our result extends to monotone real circuits, which yields new lower bounds for the Cutting Planes proof system.

Original languageEnglish
Title of host publicationSTOC 2018 - Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing
EditorsMonika Henzinger, David Kempe, Ilias Diakonikolas
PublisherAssociation for Computing Machinery
Pages801-814
Number of pages14
ISBN (Electronic)9781450355599
DOIs
StatePublished - 20 Jun 2018
Event50th Annual ACM Symposium on Theory of Computing, STOC 2018 - Los Angeles, United States
Duration: 25 Jun 201829 Jun 2018

Publication series

NameProceedings of the Annual ACM Symposium on Theory of Computing
ISSN (Print)0737-8017

Conference

Conference50th Annual ACM Symposium on Theory of Computing, STOC 2018
Country/TerritoryUnited States
CityLos Angeles
Period25/06/1829/06/18

    Research areas

  • Circuit complexity, Proof complexity

    Scopus subject areas

  • Software

ID: 52048100