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

  • 1
    $\begingroup$ What exactly do you mean by a “worst-case family of boolean formulae”? $\endgroup$ Commented Apr 26, 2012 at 11:32

1 Answer 1


Your definition of $D$ is not clear, if it is $D = \max_f (R(f) - ER(f))$, then it is exponential.

There are DNFs whose shortest proofs in ER is exponentially shorter than their shortest proofs in R e.g. PHP (pigeon hole principle) has polynomial size ER-proofs but only exponential size R-proofs.

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

  • $\begingroup$ Hi Kaveh - I meant $\min_f (R(f)-ER(f))$. I've updated the question to reflect that. $\endgroup$
    – DPLL
    Commented Apr 26, 2012 at 2:06
  • $\begingroup$ @DPLL, hi, I also updated the answer. It might help in formulating the question if you explain what you want to do. $\endgroup$
    – Kaveh
    Commented Apr 26, 2012 at 2:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.