We see that the version of the pigeon-hole principle in which every hole is forced to receive a pigeon (called onto) and the version in which every pigeon is mapped into exactly one hole (called functional) have ...

We show that the problem of finding a Resolution refutation that is at most polynomially longer than a shortest one is NP-hard. In the parlance of proof complexity, Resolution is not automatable unless P = NP. Indeed, we ...

Tree-width and path-width are two well-studied parameters of structures that measure their similarity to a tree and a path, respectively. We show that QBF on instances with constant path-width, and hence constant tree-width, ...