Comment savoir si un solveur SAT progresse dans sa tentative de réfuter une formule ? S’il a franchi une étape vers une réfutation ? Si la déduction qu’il vient de produire sera vraiment utile ? Si les déductions produites vont s’agréger de manière efficace ? Ces questions me hantent depuis des années, pour ne pas dire des décennies.

A l’occasion d’une journée RAP (Représentations et Algorithmes enPratique) du GDR IA, j’ai réalisé une vidéo présentant ma vision actuelle de la recherche dans le domaine de la résolution indirecte de CSP par reformulation de contraintes.

Les idées et résultats présentés sommairement ici sont développés dans ce rapport de recherche.

Dans ma vision de l’histoire de SAT, il y a trois générations de solveurs. Les solveurs de première génération sont purement déductifs et utilisent un système de preuve complet (pour la réfutation), la Résolution. Ceux de deuxième génération, appelé DPLL, exploitent une règle d’inférence plus faible et incomplète, la résolution unitaire, et rétablissent la complétude par une exploration arborescente de l’espace des interprétations. Les solveurs de troisième génération, de type CDCL, utilisent la résolution unitaire d’une manière similaire à DPLL, pour produire un conflit à partir d’hypothèses, mais il produisent une clause expliquant chaque conflit et ont recours à un retour arrière non chronologique permettant d’exploiter immédiatement chaque clause apprise.

Raisonner c’est paver. C’est en tout cas la vision que je défends dans une note de recherche en anglais téléchargeable ici. L’idée est de représenter l’espace d’interprétation des variables d’une formule propositionnelle par un hypercube, et chaque clause de cette formule comme une dalle hypercubique couvrant une partie de cet espace. Déterminer si la formule est cohérente revient alors à rechercher s’il existe un sommet de l’hypercube non recouvert par une clause.

La Résolution générale est le fondement des solveurs SAT complets actuels, de type CDCL, de ceux de la générations précédente, de type DPLL, et de ceux de première génération, qui l’utilisaient de manière plus directe.

Étant donnée une formule CNF , Produire une réfutation de de taille minimale en terme de nombre de déductions est intéressant à au moins deux titres : (1) la taille d’une telle réfutation donne une information sur la difficulté intrinsèque de pour la Résolution, et en particulier donne une borne inférieure de l’effort de calcul nécessaire pour réfuter , et (2) toute réfutation est une explication de l’incohérence d’une formule, et plus cette explication est courte, plus elle est, d’une certaine façon, pertinente.

Je suis chercheur à temps partiel, puisque je dois assumer également des missions d’enseignement et que je consacre beaucoup de temps à l’innovation pédagogique. Or toute activité de recherche à temps partiel comporte une charge incompressible de temps de travail aussi importante qu’une activité de recherche à plein temps, qui consiste à lire, décrypter, analyser, décortiquer de nombreuses publications scientifiques dans le but de rester informé des dernières avancées dans la spécialité concernée. Par exemple, si un chercheur à plein temps travaille 2500 heures par an et passe 500 heures à faire de la veille scientifique, cela représente 20% de son temps de travail. Mais un enseignant-chercheur ne pouvant consacrer, par exemple, que 1000 heures par an à son activité scientifique, doit faire la même veille scientifique, qui représente alors la moitié de son temps de travail. Son temps de travail « productif » représentera donc 50% de son temps consacré à la recherche, contre 80% pour notre hypothétique chercheur à plein temps. Je dis « hypothétique » car les chercheurs à plein temps n’existent pas vraiment ou sont des oiseaux rares. La plupart des chercheurs, de nos jours, doivent en effet consacrer une partie significative de leur temps à rédiger de très nombreux dossiers pour tenter d’obtenir les fonds nécessaires au financement de leur travaux de recherche.