Journal version:

    Sam Buss and Neil Thapen
    A Simple Supercritical Tradoff between Size and Height in Resolution
    Information Processing Letters, 191 (2026), article 106589.

    Download preprint version.

Related talk: Supercritical Tradeoffs between Size and Height in Resolution.
    Computability in Europe (CiE)
    Special Session on Proof Complexity & SAT
    Lisbon, 2025.

Abstract: We describe CNFs in n variables which, over a range of parameters, have small resolution refutations but are such that any small refutation must have height larger than n (even exponential in n), where the height of a refutation is the length of the longest path in it. This is called a supercritical tradeoff between size and height because, if we do not care about size, every CNF is refutable in height n. Our proof method involves uses a simple construction, based on or-ification and base d representations of integers, to reduce the number of variables. A similar result appeared in [Fleming, Pitassi and Robere, ITCS '22], for different formulas using a more complicated construction for reducing the number of variables.

Small refutations of our formula are necessarily highly irregular, making it a plausible candidate to separate resolution from pool resolution, which amounts to separating CDCL with restarts from CDCL without restarts. We are not able to show this. In the other direction, we show that a simpler version of our formula, with a similar irregularity property, \emph{does} have polynomial size pool resolution refutations and thus does not provide such a separation for CDCL.