Resolution and the binary encoding of combinatorial principles
Authors: Barnaby Martin, Stefan Dantchev and Nicola Galesi
Paper Information
| Title: | Resolution and the binary encoding of combinatorial principles |
| Authors: | Barnaby Martin, Stefan Dantchev and Nicola Galesi |
| Proceedings: | PC Abstracts |
| Editors: | Jan Johannsen and Olaf Beyersdorff |
| Keywords: | Proof Complexity, Lower Bounds, Binary Encoding |
| Abstract: | ABSTRACT. We give lower bounds in Resolution-with-bounded-conjunction, Res$(s)$, for families of contradictions where witnesses are given in the unusual binary encodings. The two families we focus on are the $k$-Clique Formulas and those associated with the (weak) Pigeonhole Principle. If one could give lower bounds in Res$(\log$) for such families under the binary encoding, then these would translate to lower bounds for the more typical unary encoding in Resolution, Res$(1)$. Such a lower bound is not possible for certain very weak Pigeonhole Principles, but might be dreamt of for the $k$-Clique Formulas. |
| Pages: | 1 |
| Talk: | Jul 07 17:00 (Session 31M) |
| Paper: | ![]() |
