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

Réduction et Encodage des Contraintes Ensemblistes en SAT

Résumé : D’un cˆot ́e, les probl`emes de satisfaction decontraintes (CSP) procurent une m ́ethode d ́eclarative etexpressive pour mod ́eliser les probl`emes. D’un autre cˆot ́e,les solveurs pour les probl`emes de satisfiabilit ́e de for-mules logique propositionnelle (SAT) peuvent manipulerdes instances ́enormes jusqu’`a des millions de clauses etvariables. Dans cet article, nous pr ́esentons une approcheb ́en ́eficiant de la mod ́elisation CSP et de la r ́esolutionSAT. Notre technique consiste `a mod ́eliser, de fa ̧con ex-pressive, des probl`emes de contraintes ensemblistes enen CSP qui sont ensuite automatiquement r ́eduits afinde retirer les valeurs des variables qui ne participent `aaucune solution. Ces CSPs r ́eduits sont ensuite encod ́esen de “bonnes” instances SAT qui peuvent ˆetre r ́esoluespar des solveurs SAT standards. Nous illustrons notretechnique par divers probl`emes standards : le Sudoku, leSocial Golfer Problem et le Sports Tournament Schedu-ling Problem.Notre technique est plus simple, plus expressive etmoins sensible aux erreurs qu’une mod ́elisation directeen SAT. De plus, les instances SAT automatiquementg ́en ́er ́ees sont g ́en ́eralement plus petites que celles direc-tement ́ecrite pour un probl`eme particulier (comme parexemple pour le Social Golfer Problem [18]) et peuventˆetre ́evalu ́ees efficacement mˆeme pour des instances ́enormes. Enfin, la phase de r ́eduction nous permet derepousser les limites et de traiter des probl`emes encoreplus gros.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal.univ-angers.fr/hal-02709514
Contributeur : Okina Univ Angers Connectez-vous pour contacter le contributeur
Soumis le : mercredi 13 octobre 2021 - 11:18:36
Dernière modification le : mercredi 27 avril 2022 - 04:14:41
Archivage à long terme le : : vendredi 14 janvier 2022 - 18:47:22

Fichier

JFPC2016-FR.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-02709514, version 1
  • OKINA : ua15348

Collections

Citation

Frédéric Lardeux, Eric Monfroy. Réduction et Encodage des Contraintes Ensemblistes en SAT. Douzièmes journées Francophones de Programmation par Contraintes (JFPC), 2016, Montpellier, France. ⟨hal-02709514⟩

Partager

Métriques

Consultations de la notice

20

Téléchargements de fichiers

17