C-M. Li, F. Xiao, M. Luo, F. Manya, Z. Lu, Y. Li, ‘Clause vivification by unit propagation in CDCL SAT Solvers‘, Artificial Intelligence, Volume 279, 2020

      Commentaires fermés sur C-M. Li, F. Xiao, M. Luo, F. Manya, Z. Lu, Y. Li, ‘Clause vivification by unit propagation in CDCL SAT Solvers‘, Artificial Intelligence, Volume 279, 2020
  • Lien
  • Résumé : Les clauses originales et apprises dans les solveurs SAT à base d’apprentissage de clauses dirigé par les conflits (CDCL) contiennent souvent des littéraux redondants. Cela peut avoir un impact négatif sur les performances du solveur, car les littéraux redondants peuvent détériorer à la fois l’efficacité de la propagation des contraintes booléennes et la qualité des clauses apprises ultérieures. Pour surmonter cet inconvénient, nous proposons une approche de vivification de clauses qui élimine les littéraux redondants en appliquant la propagation unitaire. La vivification de clauses proposée est activée avant que le solveur SAT déclenche certains redémarrages sélectionnés et n’affecte qu’un sous-ensemble de clauses originales et apprises, considérées comme plus pertinentes selon des métriques telles que la distance en blocs littéraux (LBD). De plus, nous avons mené une enquête empirique avec des instances provenant des catégories difficiles de combinatoire et d’applications des récentes compétitions SAT. Les résultats montrent qu’un nombre significatif d’instances supplémentaires sont résolues lorsque l’approche proposée est incorporée dans cinq des solveurs SAT CDCL les plus performants (Glucose, TC_Glucose, COMiniSatPS, MapleCOMSPS et MapleCOMSPS_LRB). Plus important encore, l’enquête empirique comprend une analyse approfondie de l’efficacité de la vivification de clauses. Il est à noter qu’un des solveurs SAT décrits ici a été classé premier dans la catégorie principale de la compétition SAT 2017 grâce à l’incorporation de la vivification de clauses proposée. Ce solveur a été encore amélioré dans cet article et a remporté la médaille de bronze dans la catégorie principale de la compétition SAT 2018.