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 →