Resolution and the binary encoding of combinatorial principles

Location: Bourne LT2

Abstract

We investigate the size of refutations in Res(k), an extension of Resolution working on k-DNFs instead of clauses, for certain contradictions given in the less usual binary encoding. In particular, we prove lower bounds for binary k-Clique principle as well as for the Weak Pigeon-Hole Principle. Previously, a resolution lower bound was known for the former while the later was considered in the more usual unary encoding only. This is based on a joint work with Nicola Galesi (La Sapienza, Roma) and Barnaby Martin (Durham). The first half of the talk will be a kind of general introduction to Propositional Proof Complexity, and thus accessible to everyone.

Bio

Stefan Dantchev got his PhD from Aarhus University, Denmark in 2002. He spent two years at University of Leicester, before moving to Durham University. His research interests are in Computational Complexity, and in particular in Propositional Proof Complexity.