J’étudie comment la structure des graphes façonne la complexité des preuves
et le comportement des solveurs SAT, avec les formules de Tseitin comme
laboratoire expérimental et théorique.
Un programme de recherche à l’intersection de la théorie des graphes,
de la complexité des preuves et de l’expérimentation computationnelle,
consacré aux mécanismes qui rendent certaines instances SAT difficiles.
Programme de recherche · 2025–2026
Structure, preuves et difficulté des formules de Tseitin
Mes travaux utilisent les formules de Tseitin pour étudier le lien entre
la géométrie d’un graphe, la complexité des réfutations par Résolution
et le comportement empirique des solveurs SAT.
Une première étude, Spectral Predictors for Tseitin Hardness,
a exploré le pouvoir prédictif de propriétés spectrales des graphes.
Les expériences plus récentes mettent également en évidence des
transitions brutales de difficulté et une forte sensibilité du solveur
à des perturbations structurelles et à la présentation d’instances
mathématiquement équivalentes.
Le programme actuel cherche à relier ces observations expérimentales
à des quantités intrinsèques du graphe, notamment la treewidth et les
paramètres spectraux, puis à comprendre l’écart entre complexité
théorique des preuves et difficulté observée dans les solveurs CDCL.