# Resolution vs Extended Resolution

Let $R(f)$ and $ER(f)$ be the minimum-size for unsat proofs of $f$ in Resolution and Extended Resolution respectively. What's the best bound we have on $D=\min_f (R(f)-ER(f))$ where $f$ belongs to a worst-case family of boolean formulae? Since no superpolynomial lower bounds are known on Extended Resolution, we don't have a good upper bound on $D$, so I'm interested in lower bounds on $D$.

Edit: Clarified question as per Kaveh's answer below

• What exactly do you mean by a “worst-case family of boolean formulae”? – Emil Jeřábek Apr 26 '12 at 11:32

Your definition of $D$ is not clear, if it is $D = \max_f (R(f) - ER(f))$, then it is exponential.
Unsatisfiability of $f$ is the same as $\lnot f$ being a tautology. Let $\lnot f$ be as PHP. Then $R(f)$ is exponential where as $ER(f)$ is polynomial, so the difference is exponential. Also it cannot be more than exponential.
If $D = \min_f (R(f) - ER(f))$ then it is 0. Take $\lnot f=\top$ and it has one line proof in both. (R is included in ER so it cannot be less than 0.)
• Hi Kaveh - I meant $\min_f (R(f)-ER(f))$. I've updated the question to reflect that. – DPLL Apr 26 '12 at 2:06