Accéder directement au contenu Accéder directement à la navigation
Communication dans un congrès

Eigenvector centrality in industrial SAT instances

Abstract : Despite the success of modern SAT solvers on industrial instances, most of the progress relies on intensive experimental testing of improvements or new ideas. In most cases, the behavior of CDCL solvers cannot be predicted and even small changes may have a dramatic positive or negative effect. In this paper, we do not try to improve the performance of SAT solvers, but rather try to improve our understanding of their behavior. More precisely, we identify an essential structural property of industrial instances, based on the Eigenvector centrality of a graphical representation of the formula.We show how this static value, computed only once over the initial formula casts new light on the behavior of CDCL solvers. We also advocate for a better partitionning of industrial problems. Our experiments clearly suggest deep discrepancies among the families of benchmarks used in the last SAT competitions.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

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

https://hal.inrae.fr/hal-02746136
Déposant : Migration Prodinra <>
Soumis le : mercredi 3 juin 2020 - 09:34:34
Dernière modification le : mercredi 14 octobre 2020 - 03:59:08

Fichier

Eigenvector centrality in indu...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Georgios Katsirelos, Laurent Simon. Eigenvector centrality in industrial SAT instances. CP 2012 - 18th International Conference on Principles and Practice of Constraint Programming, Oct 2012, Québec, Canada. 1012p., ⟨10.1007/978-3-642-33558-7_27⟩. ⟨hal-02746136⟩

Partager

Métriques

Consultations de la notice

10

Téléchargements de fichiers

37