<p><strong>Background:</strong><br />
For an unsatisfiable SAT formulas, the length of a resolution refutaion means the number of clauses in it.
It's well known that there exist exponential separation between tree-like and general resolution length. <br />
i.e. there are some unsatisfiable SAT formulas whose shortest general resolution refutation length is <span class="math-container">$S$</span>, while the shortest tree-like resolution refutation length is <span class="math-container">$2^{\Omega(S/logS)}$</span>. see</p>
<ul>
<li>Ben-Sasson*, E., Impagliazzo†, R. &amp; Wigderson‡, A. <a href="https://www.researchgate.net/publication/220442116_Near_Optimal_Separation_Of_Tree-Like_And_General_Resolution" rel="nofollow noreferrer">Near Optimal Separation Of Tree-Like And General Resolution.</a> Combinatorica 24, 585–603 (2004).</li>
</ul>
<p><strong>Problem:</strong><br />
Conversely, I am wondering for what kind of unsatifiable SAT formulas, the shortest tree-like and general resolution refutation length is the same/polynomially?</p>
<p><strong>My purpose:</strong><br />
My purpose is to get the lower bound of general(regular) resolution for an unsatisfiable SAT formula. By far I have get the lower bound of tree-like resolution.and I want to show there's no big separation in my SAT instance to  get the lower bound of general(regular) resolution.<br />
However, I have not found any articles about In what situation the separation is small.</p>

CC BY-SA 4.0
2023-04-21T05:15:31.363Z
Do you want to prove a lower bound for general or for regular resolution?
notautogenerated
CC BY-SA 4.0
2023-04-21T06:09:23.483Z
@notautogenerated Exactly lower bound for regular resolution. Since general size is always $\leq$ regular size.  If I can get lower bound for general resolution, it makes sense.
Jxb
CC BY-SA 4.0
2023-04-21T06:53:31.120Z
They are the same up to a polynomial speedup e.g. for all CNF that require size $2^{\Omega(n)}$ in general resolution, or that have polynomial-size tree-like resolution refutations. However, I guess this is not very helpful; I am not aware of any easily recognizable class of CNF where the speedup is only polynomial.
Emil Jeřábek
CC BY-SA 4.0
2023-04-21T07:06:03.870Z
@EmilJeřábek I am not clear of "polynomial speedup". Could you please explain it?
Jxb
CC BY-SA 4.0
2023-04-21T07:17:10.820Z
I mean that the size of a tree-like proof is polynomial in the size of the smallest general resolution proof, as you want in the question
Emil Jeřábek
CC BY-SA 4.0
2023-04-22T01:34:13.400Z
To rephrase Emil's comment, the cases where we know there is no large separation are those where we can already prove upper or lower bounds by other means. I would probably try to prove a width lower bound and use BenSasson--Widgerson.
notautogenerated
<reference-request><sat><proof-complexity><resolution>
When the tree-like resolution size is the same with general(regular) resolution size？
Jxb
# When the tree-like resolution size is the same with general(regular) resolution size？

(Asked by: username_0 on 2023-04-19)

**Background:**  
For an unsatisfiable SAT formulas, the length of a resolution refutaion means the number of clauses in it.
It's well known that there exist exponential separation between tree-like and general resolution length.   
i.e. there are some unsatisfiable SAT formulas whose shortest general resolution refutation length is $S$, while the shortest tree-like resolution refutation length is $2^{\Omega(S/logS)}$. see

* Ben-Sasson\*, E., Impagliazzo†, R. & Wigderson‡, A. [Near Optimal Separation Of Tree-Like And General Resolution.](https://www.researchgate.net/publication/220442116_Near_Optimal_Separation_Of_Tree-Like_And_General_Resolution) Combinatorica 24, 585–603 (2004).

**Problem:**  
Conversely, I am wondering for what kind of unsatifiable SAT formulas, the shortest tree-like and general resolution refutation length is the same/polynomially?

**My purpose:**  
My purpose is to get the lower bound of general(regular) resolution for an unsatisfiable SAT formula. By far I have get the lower bound of tree-like resolution.and I want to show there's no big separation in my SAT instance to get the lower bound of general(regular) resolution.  
However, I have not found any articles about In what situation the separation is small.

**Tags:** reference-request, sat, proof-complexity, resolution
> **Comments:**
> **username_1**: Do you want to prove a lower bound for general or for regular resolution?  
> **username_0**: @notautogenerated Exactly lower bound for regular resolution. Since general size is always $\leq$ regular size.  If I can get lower bound for general resolution, it makes sense.  
> **username_2**: They are the same up to a polynomial speedup e.g. for all CNF that require size $2^{\Omega(n)}$ in general resolution, or that have polynomial-size tree-like resolution refutations. However, I guess this is not very helpful; I am not aware of any easily recognizable class of CNF where the speedup is only polynomial.  
> **username_0**: @EmilJeřábek I am not clear of "polynomial speedup". Could you please explain it?  
> **username_2**: I mean that the size of a tree-like proof is polynomial in the size of the smallest general resolution proof, as you want in the question  
> **username_1**: To rephrase Emil's comment, the cases where we know there is no large separation are those where we can already prove upper or lower bounds by other means. I would probably try to prove a width lower bound and use BenSasson--Widgerson.  

---

## 0 answers

