FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
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: