Deux médailles d'or pour le LIS (équipe COALA) à la compétition internationale SAT Competition, 2021.

Mohamed Sami Cherif, Djamal Habet et Cyril Terrioux de l'équipe COALA ont obtenu deux médailles d'or à la 20ème édition de l'International SAT Competition (2021) grâce à leur travail proposant l'usage des techniques d'apprentissage par renforcement pour guider le choix des heuristiques de branchement. La première médaille a été obtenue dans le Main Track, qui est la catégorie « reine » de cette compétition. La seconde médaille est obtenue dans le SAT Main Track, une sous-catégorie du Main Track qui en comporte deux. La portée d'un tel résultat est significative et fondamentale, à la fois parce que le problème SAT (satisfiabilité en logique propositionnelle) est central en Théorie de la Complexité algorithmique, et que les solveurs SAT ont atteint désormais une réelle maturité qui en fait des systèmes qui sont beaucoup utilisés dans le cadre industriel pour résoudre quantité de problèmes réels dans de nombreux domaines d’applications, en plus de problèmes académiques, comme notamment certaines conjectures en mathématiques.

Le détail des résultats est consultable ici : https://satcompetition.github.io/2021/

Parallèlement, un papier décrivant l'approche utilisée dans Kissat-MAB a été accepté et publié dans les actes de la 23ème édition de la conférence internationale en programmation par contraintes : Principles and Practice of Constraint Programming, 2021.

https://cp2021.a4cp.org  

Title: Combining VSIDS and CHB Using Restarts in SAT
Authors : Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux

Conflict Driven Clause Learning (CDCL) solvers are known to be efficient on structured instances and manage to solve ones with a large number of variables and clauses. An important component in such solvers is the branching heuristic which picks the next variable to branch on. In this paper, we evaluate different strategies which combine two state-of-the-art heuristics, namely the Variable State Independent Decaying Sum (VSIDS) and the Conflict History-Based (CHbranching heuristic. These strategies take advantage of the restart mechanism, which helps to deal with the heavy-tailed phenomena in SAT, to switch between these heuristics thus ensuring a better and more diverse exploration of the search space. Our experimental evaluation shows that combining VSIDS and CHB using restarts achieves competitive results and even significantly outperforms both heuristics for some chosen strategies.