I am studying the complexity of SAT resolution refutation. There is a useful tool named weakening rule

The weakening rule:
B -->B ∨ C says that from a clause B we can derive the weaker clause B ∨ C for an arbitrary C. We say that B ∨ C is a weakening of B. We can add this extra rule without loss of generality, since any applications of weakening in a resolution refutation can always be eliminated.

My question: Why weakening rule doesn't increase the size of resolution refutation?

where size means the number of clauses the refutation contained.

Ituitively, I can understand it, but I can't state the proof formally.

enter image description here

  • 1
    $\begingroup$ Please edit your question to define what you mean by the "size" of resolution refutation. Please add your thoughts and understanding. What progress have you made? $\endgroup$
    – D.W.
    Commented Apr 13, 2023 at 6:14
  • 1
    $\begingroup$ Theorem 2 solves my problem. mathweb.ucsd.edu/~sbuss/CourseWeb/Math267_2002W/lecture7.pdf $\endgroup$
    – Jxb
    Commented May 26, 2023 at 9:31


Your Answer

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