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: