|
|||||
|
|
Lower Bounds for the Weak Pigeonhole Principle and Random Formulas beyond Resolution |
|
| Authors: | Albert Atserias Maria Luisa Bonet Juan Luis Esteban |
| Affiliation: | a Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya, C/Jordi Girona Salgado, 1-3, Edif. C6, Barcelona, E08034, Spainf1;b Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya, C/Jordi Girona Salgado, 1-3, Edif. C6, Barcelona, E08034, Spainf2;c Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya, C/Jordi Girona Salgado, 1-3, Edif. C6, Barcelona, E08034, Spainf3 |
| Abstract: | We work with an extension of Resolution, called Res(2), that allows clauses with conjunctions of two literals. In this system there are rules to introduce and eliminate such conjunctions. We prove that the weak pigeonhole principle PHPcnn and random unsatisfiable CNF formulas require exponential-size proofs in this system. This is the strongest system beyond Resolution for which such lower bounds are known. As a consequence to the result about the weak pigeonhole principle, Res(log) is exponentially more powerful than Res(2). Also we prove that Resolution cannot polynomially simulate Res(2) and that Res(2) does not have feasible monotone interpolation solving an open problem posed by Krají |
| Keywords: | Abbreviations: proof complexityAbbreviations: resolutionAbbreviations: lower boundsAbbreviations: random restrictionsAbbreviations: martingalesAbbreviations: monotone interpolation |
| 本文献已被 ScienceDirect 等数据库收录！ | |