Branchement pour SAT et au-delà – BforSAT

BforSAT

Branchement pour SAT et au delà

Résumé

Le problème de satisfiabilité propositionnelle (SAT) est un formalisme fondamental en programmation par contraintes qui est utilisé pour modéliser et résoudre une grande variété de problèmes académiques et industriels. Les solveurs SAT modernes sont désormais capables de résoudre des instances comportant des millions de variables et de clauses dans un délai raisonnable, mais ils peuvent encore échouer drastiquement sur certaines instances. En effet, l'efficacité des solveurs SAT est fortement influencée par les décisions prises au cours de la résolution. Les heuristiques de branchement jouent donc un rôle clé dans l'amélioration des performances des solveurs SAT, rendant leur développement et leur optimisation cruciale pour une résolution efficace de SAT. De plus, récemment, il y a un intérêt croissant pour l'intégration de mécanismes d'apprentissage automatique dans la résolution de problèmes combinatoires et, de manière plus marginale, dans le contexte de SAT. Le projet BforSAT vise à améliorer et à affiner les heuristiques de branchement pour SAT et au-delà. Notre intention est d'explorer des heuristiques innovantes incorporant des mécanismes d'apprentissage automatique, et ainsi de tirer parti de son potentiel à améliorer les capacités de prise de décision des solveurs SAT modernes. Ces nouvelles heuristiques seront soumises à une évaluation rigoureuse, contribuant ainsi à une compréhension plus approfondie des stratégies de branchement pour SAT et au-delà. Nos efforts viseront, entre autres, à combler le fossé entre les techniques traditionnelles de résolution de problèmes combinatoires et les méthodologies de pointe en apprentissage automatique. En exploitant ce paradigme, nous anticipons un changement dans la manière d'aborder et de résoudre les problèmes SAT et apparentés, mais aussi de découvrir de nouvelles stratégies pour relever des défis du monde réel, avec des implications majeures tant pour le milieu académique que pour l'industrie.