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).
Type de document :
Communication dans un congrès
JFPC 2010 - Sixièmes Journées Francophones de Programmation par Contraintes, Jun 2010, Caen, France. pp.237-246, 2010
Liste complète des métadonnées

Littérature citée [7 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00519164
Contributeur : Christophe Lecoutre <>
Soumis le : samedi 18 septembre 2010 - 15:40:47
Dernière modification le : jeudi 15 mars 2018 - 16:56:06
Document(s) archivé(s) le : mardi 23 octobre 2012 - 16:20:53

Fichier

prcovic.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : inria-00519164, version 1

Collections

Citation

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, 2010. 〈inria-00519164〉

Partager

Métriques

Consultations de la notice

99

Téléchargements de fichiers

68