Article mis en avant

Pourquoi un blog de recherche

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.

Continuer la lecture →

Apprentissage guidé par la subsomption

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.

Continuer la lecture →

DPLL avec redémarrages simule linéairement CDCL

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.

Continuer la lecture →

SAT est un problème de pavage d’hypercube

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.

Continuer la lecture →

Apprendre avec la propagation unitaire

Je présente dans ce billet une idée qui est décrite en anglais dans cette note. Elle consiste à exploiter des séquences d’hypothèses et de déductions pour produire des clauses qui sont conséquences logiques de celles ayant servi à réaliser les déductions, comme le font les solveurs CDCL, mais avec une approche différente, permettant de produire d’autres clauses.

Par exemple, considérons cette séquence contradictoire d’hypothèses et de déductions qui pourrait être produite par un solveur SAT de type CDCL ou même DPLL. Je propose d’appeler une telle séquence AUP-séquence contradictoire (AUP pour Assumption and Unitary Propagation).

Continuer la lecture →

Réfutations minimales

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 \Sigma, Produire une réfutation de \Sigma 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 \Sigma pour la Résolution, et en particulier donne une borne inférieure de l’effort de calcul nécessaire pour réfuter \Sigma , 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.

Continuer la lecture →