5
$\begingroup$

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

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

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.

Addendum:

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

$\endgroup$
  • $\begingroup$ Hi Kaveh - I meant $\min_f (R(f)-ER(f))$. I've updated the question to reflect that. $\endgroup$ – DPLL Apr 26 '12 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 Apr 26 '12 at 2:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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