Department of Computer Science & Engineering

For each $k \geq 1$, we give a famiily of unsatisfiable sets of clauses which have polynomial size ${\mbox{Res}}(k+1)$ refutations, but which require ${\mbox{Res}}(k)$ refutations of $2^{n^{\epsilon_k}}$. This improves the superpolynomial- separation between resolution and ${\mbox{Res}}(2)$ given by Bonet and Galesi to exponential. As a corollary, we obtain an exponential separation between depth 0 Frege and depth 1 Frege, improving upon the superpolynomial separation given by the weak pigeonhole principle.

Pre-2018 CSE ID: CS2002-0697