We consider two natural measures associated with a Resolution refutation*: its width (the widest clause appearing in the refutation) and its space (the minimum amount of memory necessary to verify its correctness). A natural question to ask is the following: can we optimise both parameters at once? In other words, can we find a resolution refutation whose space and width are both close to the minimum possible value?

I shall exhibit a negative result in this direction: there exists an unsatisfiable CNF which has a refutation with constant space and a refutation with constant width, but making one parameter small necessarily causes a blowup in the other parameter.

I shall be following this paper: https://dl.acm.org/doi/10.1145/509907.509975

*PS: Don't worry if you don't know the definition of Resolution refutation.