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: |