Rodrigue Konan Tchinda ; Clémentin Tayou Djamegni - Amélioration du raisonnement dans les solveurs SAT CDCL avec la règle d'extension

arima:6434 - Revue Africaine de Recherche en Informatique et Mathématiques Appliquées, 9 novembre 2021, Volume 33 - Numéro spécial CRI 2019 - 2020-21 - https://doi.org/10.46298/arima.6434
Amélioration du raisonnement dans les solveurs SAT CDCL avec la règle d'extensionArticle

Auteurs : Rodrigue Konan Tchinda 1,2,3,4; Clémentin Tayou Djamegni 1

  • 1 Université de Dschang
  • 2 University of Bamenda, Bambili, Cameroon
  • 3 University of Bamenda
  • 4 Higher Teachers' Training College, University of Maroua

La règle d'extension introduite pour la première fois par G. Tseitin est une règle simple mais puissante qui, ajoutée à la résolution, conduit à un système de preuves plus puissant appelé résolution étendue (ER). Malgré les résultats théoriques remarquables obtenus avec ER, son exploitation pratique pour améliorer l'efficacité des solveurs SAT pose encore quelques problèmes. Plusieurs tentatives visant à intégrer la règle d'extension aux solveurs CDCL SAT existent dans la littérature, mais les résultats ne sont en général pas aussi prometteurs qu'en théorie. Une remarque importante à faire sur ces tentatives est qu'elles se concentrent pour la plupart sur la réduction de la taille des preuves à l'aide des variables étendues introduites dans le solveur. Nous adoptons dans ce travail un point de vue différent. Nous considérons les variables étendues comme un moyen d'améliorer le raisonnement dans les solveurs et donc de leur donner la capacité de raisonner sur différents aspects sémantiques des variables. Les expérimentations réalisées sur les instances tirées des compétition SAT 2018 et 2020 montrent que l'utilisation de la règle d'extension dans les solveurs CDCL est bénéfique aussi bien pour les instances satisfiables que celles insatisfiables.


Volume : Volume 33 - Numéro spécial CRI 2019 - 2020-21
Publié le : 9 novembre 2021
Accepté le : 23 octobre 2021
Soumis le : 28 avril 2020
Mots-clés : SAT,CDCL,Extension Rule,SAT,CDCL,Règle d'extension,[INFO]Computer Science [cs],[INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI]

Statistiques de consultation

Cette page a été consultée 382 fois.
Le PDF de cet article a été téléchargé 294 fois.