Optimisation des certificats pour la satisfiabilité et au delà // Understanding and Optimizing Proofs in Satisfiability and Beyond

Ce projet de thèse s'inscrit dans les objectifs de la chaire Symbolic AI Problem Solving (SAIPS), financée par l'université de Picardie Jules Verne, et vise à approfondir la compréhension et l'amélioration des solveurs modernes en explorant des techniques innovantes pour la satisfiabilité propositionnelle (SAT) et au-delà. L'un des axes majeurs de cette recherche est d'améliorer l'interprétabilité des solveurs en optimisant la structure des preuves générées. En s'appuyant sur des approches d'apprentissage automatique, ce projet cherche donc à détecter les redondances et à extraire les informations essentielles des structures de preuve, afin de réduire leur taille et d'accroître l'efficacité des solveurs. L'objectif ultime est d'améliorer l'explicabilité et la transparence des solveurs SAT modernes, en produisant des preuves plus compactes et structurées, facilitant ainsi l'interprétation de leur fonctionnement.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

This PhD project aligns with the objectives of the Symbolic AI Problem Solving (SAIPS) chair, funded by the university of Picardie Jules Verne, and aims to deepen the understanding and enhancement of modern solvers by exploring innovative techniques for propositional satisfiability (SAT) and beyond. One of the major objectives is to improve solver interpretability by optimizing the structure of certificates generated by modern solvers. Using machine learning approaches, this project thus seeks to detect redundancies and extract essential information from proof structures to reduce their size and enhance solver efficiency. The ultimate goal is to improve the explainability and transparency of modern SAT solvers by producing more compact and structured proofs, thereby facilitating our understanding of their behavior and potentially helping to enhance their efficency.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Début de la thèse : 01/10/2025

Financement d'un établissement public Français

Université de Picardie - Jules Verne

585 Sciences, Technologie, Santé

Le candidat doit être titulaire d'un Master en informatique (obtenu avant le début de la thèse). De solides compétences en programmation (C/C++) ainsi qu'une maîtrise de l'anglais sont requises. Il devra faire preuve de rigueur scientifique, de capacités d'analyse et de résolution de problèmes. Une connaissance préalable en programmation par contraintes, et plus particulièrement en satisfiabilité (SAT), serait fortement appréciée.
The candidate must hold a Master's degree in computer science (obtained before the start of the PhD). Strong programming skills (C/C$++$) and proficiency in English are required. The candidate should demonstrate scientific rigor, problem-solving abilities, and analytical skills. Prior knowledge of constraint programming and particularly Satisfiability would be highly appreciated.