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.

Mais c’est juste une manière de voir les choses. On peut aussi dire que les trois types de solveurs sont purement déductifs. DPLL déduit implicitement des clauses à partir des conflits en réalisant un raisonnement par l’absurde. Les déductions réalisées sont représentées de manière très concise par les phases des variables de branchement, qui font office d’hypothèses pour la raisonnement par l’absurde. Quand à CDCL, il déduit des clauses par analyse des conflits provoqués par des hypothèses appelées décisions, et ses déductions correspondent à des cas particuliers de Résolutions.

Quoi qu’il en soit, un des gros défaut de DPLL est qu’il ne permet de réfuter qu’en temps exponentiel certaines formules qui peuvent être réfutées en temps polynomial par CDCL. Il a été démontré que CDCL peut simuler la Résolution en temps polynomial, alors que, de fait, DPLL ne le peut pas. Ce gap exponentiel entre DPLL et CDCL est un argument qui explique peut être en partie que les recherches sur DPLL aient été presque abandonnées. Il y a aussi un autre argument , qui est que les solveurs CDCL sont en pratiques plus efficaces que les solveurs DPLL sur de nombreuses instances SAT, en particulier à vocation industrielle.

Mais une modification très simple de DPLL lui permet de produire des réfutations de même taille que celles pouvant être produites par CDCL, sous réserve de disposer d’un « oracle » permettant de choisir les variables de décision / branchement de manière appropriée. Cette modification consiste à permettre à DPLL de réaliser des redémarrages précédés d’un apprentissage des clauses représentant les connaissances accumulées depuis le début de chaque session de recherche. Pour simuler CDCL, nous réalisons un redémarrage après chaque conflit, mais en pratique, il est possible de faire des redémarrages moins drastiques et je pense que cela ouvre des perspectives de recherche très intéressantes, car si les redémarrages sont espacés, le nombre de clauses apprises peut devenir beaucoup plus petit qu’avec CDCL. Le potentiel de cette approche dépend de l’existence d’heuristiques de choix de variables de décision et de stratégie de redémarrage efficaces. Cela représente un énorme champ d’investigation encore inexploré.