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

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.

  • $\begingroup$ Do you want to prove a lower bound for general or for regular resolution? $\endgroup$ Apr 21, 2023 at 5:15
  • $\begingroup$ @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. $\endgroup$
    – Jxb
    Apr 21, 2023 at 6:09
  • 1
    $\begingroup$ 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. $\endgroup$ Apr 21, 2023 at 6:53
  • 1
    $\begingroup$ 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 $\endgroup$ Apr 21, 2023 at 7:17
  • 1
    $\begingroup$ 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. $\endgroup$ Apr 22, 2023 at 1:34


Your Answer

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