Journal version:

    Sam Buss and Neil Thapen
    A Simple Supercritical Tradoff between Size and Height in Resolution
    Submitted for publication. December 2023.

    Download preprint version.

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 \emph{supercritical} tradeoff between size and height because, if we do not care about size, every CNF is refutable in height n. A similar result appeared in [Fleming, Pitassi and Robere, ITCS '22], for different formulas using a more complicated construction. 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. We are not able to show this, but we show that a simpler version of our formula, with a similar irregularity property, does have polynomial size pool resolution refutations.