Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR24-001 | 2nd January 2024 12:23

A Simple Supercritical Tradeoff between Size and Height in Resolution


Authors: Sam Buss, Neil Thapen
Publication: 2nd January 2024 19:46
Downloads: 112


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. 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.

ISSN 1433-8092 | Imprint