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.
