Skip to Main content Skip to Navigation
Conference papers

Réparation locale de réfutation de formules SAT

Abstract : 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).
Document type :
Conference papers
Complete list of metadata

Cited literature [7 references]  Display  Hide  Download
Contributor : Christophe Lecoutre Connect in order to contact the contributor
Submitted on : Saturday, September 18, 2010 - 3:40:47 PM
Last modification on : Saturday, June 25, 2022 - 7:48:40 PM
Long-term archiving on: : Tuesday, October 23, 2012 - 4:20:53 PM


Explicit agreement for this submission


  • HAL Id : inria-00519164, version 1


Nicolas Prcovic. Réparation locale de réfutation de formules SAT. JFPC 2010 - Sixièmes Journées Francophones de Programmation par Contraintes, Jun 2010, Caen, France. pp.237-246. ⟨inria-00519164⟩



Record views


Files downloads