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

<p>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.</p>

<p>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. </p>

<p>Addendum:</p>

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

CC BY-SA 3.0
2012-04-26T02:06:21.433Z
Hi Kaveh - I meant $\min_f (R(f)-ER(f))$. I've updated the question to reflect that.
DPLL
CC BY-SA 3.0
2012-04-26T02:08:58.473Z
@DPLL, hi, I also updated the answer. It might help in formulating the question if you explain what you want to do.
Kaveh
CC BY-SA 3.0
2012-04-26T02:03:42.517Z
2012-04-26T02:19:32.160Z
2012-04-26T02:19:32.160Z
Kaveh
<p>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$.</p>

<p>Edit: Clarified question as per Kaveh's answer below</p>

CC BY-SA 3.0
2012-04-26T11:32:29.263Z
What exactly do you mean by a “worst-case family of boolean formulae”?
Emil Jeřábek
<cc.complexity-theory><lo.logic><proof-complexity><proof-theory>
Resolution vs Extended Resolution
DPLL
# Resolution vs Extended Resolution

(Asked by: username_0 on 2012-04-26)

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

**Tags:** cc.complexity-theory, lo.logic, proof-complexity, proof-theory
> **Comments:**
> **username_1**: What exactly do you mean by a “worst-case family of boolean formulae”?  

---

## 1 answers

### Answer by username_2 on 2012-04-26. Score: 8

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

> **Comments:**
> **username_0**: Hi Kaveh - I meant $\min_f (R(f)-ER(f))$. I've updated the question to reflect that.  
> **username_2**: @DPLL, hi, I also updated the answer. It might help in formulating the question if you explain what you want to do.  

---

