Thèse en complexité de la preuve et compilation de connaissances (H/F)

Sujet de thèse :
L'objectif original de la complexité de la preuve est de prouver que P est différent de NP en montrant qu'il n'y a pas de preuves courtes pour coNP. À cette fin, des systèmes de preuves fortes pour différents problèmes, en particulier SAT ont été introduit dans le but de montrer qu'en général, il n'existe pas de preuves courtes et efficacement vérifiables pour le problème en question.

Une autre orientation, plus récente, de la complexité de la preuve provient de l'observation que de nombreux algorithmes génèrent implicitement des preuves de correction, souvent une forme de représentation de l'exécution de l'algorithme sur une instance. Ainsi, la compréhension des preuves générées permet de mieux comprendre l'algorithme considéré et ses limites. Cette approche est également utile pour vérifier l'exactitude des résultats des solveurs mettant en œuvre l'algorithme : l'écriture explicite de la preuve générée permet de vérifier l'exactitude avec un vérificateur de preuve indépendant qui, étant moins complexe qu'un solveur complet, est aujourd'hui souvent vérifié de manière formelle. Cela permet de vérifier l'exactitude des résultats générés par le solveur, ce qui permet de lui faire confiance dans les applications critiques. Cette approche est la plus développée dans la résolution SAT pour le système de preuve DRAT et ses variantes, mais il existe également des approches similaires pour les solveurs pseudo-booléens, QBF et le problème de comptage propositionnel #SAT (entre autres).

Ces dernières années, les structures de données utilisées en compilation de connaissances ont trouvé des applications dans le domain de la complexité de la preuve. Ce domaine étudie systématiquement différentes représentations des fonctions booléennes. Les plus importantes de ces représentations sont les circuits connus sous le nom de DNNF (decomposable negation normal form) et leurs différentes sous-classes. Ces sous-classes correspondent essentiellement à différents algorithmes de comptage. Cette observation a conduit à l'introduction de DNNF certifiées comme format de preuve pour #SAT.

L'idée de la thèse proposée est d'étudier plus largement la compilation de connaissances dans un contexte de complexité de la preuve. Quelques exemples de questions sont les suivants : quels systèmes de preuves pour #SAT peuvent être vus comme des preuves sous forme de DNNF ? Les séparations connues entre les différentes classes de DNNF peuvent-elles être étendues aux systèmes de preuves ? Quelles restrictions ou extensions naturelles des DNNF donnent des systèmes de preuves utiles ? Au-delà du comptage, quels autres problèmes se prêtent à une analyse à l'aide de techniques de compilation de connaissances ? On sait par exemple que les DNNF peuvent être utilisée dans des algorithmes pour QBF et MaxSAT. Cela donne-t-il une nouvelle perspective sur ces problèmes ? Cela conduit-il à des algorithmes utiles ?


Le travail
Voir plus sur le site emploi.cnrs.fr...