0
$\begingroup$

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

Improve this question
$\endgroup$
2
  • 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. ♦
    Apr 13 at 6:14
  • $\begingroup$ Theorem 2 solves my problem. mathweb.ucsd.edu/~sbuss/CourseWeb/Math267_2002W/lecture7.pdf $\endgroup$
    – Jxb
    May 26 at 9:31

0

Reset to default

Your Answer

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