We address the problem of proving that a boolean formula is unsatisable. We present a local repair scheme which proves unsatisability by resolution. The main idea is to consider the linear proofs which number of allowed resolutions is bounded by a constant as being equivalent to constraint satisfaction problems (CSP), which solu- tions are refutations of the boolean formula. Therefore, any local repair technique applicable to CSP can be reu- sed, once dened the neighborhood of a "refutation to be repaired" and its proximity to a true refutation. We propose criteria to evaluate the proofs to be repaired and dene neighborhood operators that re-assign a va- riable of CSP (change of a clause) or swap the values of variables (move of a clause inside the proof).