Exponential Separation of Res(k) and Res(k+1)
Skip to main content
Open Access Publications from the University of California

Exponential Separation of Res(k) and Res(k+1)


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

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View