How can a DAG-like resolution proof be transformed to a tree-like resolution proof?

Is such a transformation possible in polynomial time?

  • 4
    $\begingroup$ It's an exercise to come up with a transformation with exponential blow up, and that's sometimes necessary: math.ias.edu/~avi/PUBLICATIONS/MYPAPERS/BIW03/biw03.pdf. Moreover, the paper shows a more efficient transformation than the trivial one. $\endgroup$ Aug 11 '18 at 18:51
  • $\begingroup$ Thanks. the paper is a bit long. I'll read it carefully to see how the authors proceed. $\endgroup$
    – RTK
    Aug 11 '18 at 20:54

Your Answer

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

Browse other questions tagged or ask your own question.