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.

Le problème, c’est que la production d’une réfutation minimale est une tâche extrêmement couteuse. Je ne me doutait d’ailleurs pas à quel point en entreprenant la conception et le développement d’algorithmes dédiés à cet usage. J’espérais produire des réfutation minimales de formules à 10 variables, voire un peu plus, mais je me suis heurté à une barrière au delà de 5 variables.

J’ai expérimenté deux algorithmes qui sont présentés dans cet article. Le premier produit en parallèle toutes les inférences possibles à partir de la formule à réfuter, alors que le deuxième énumère toutes les réfutations possibles une par une. Pour chaque approche, j’ai développé plusieurs optimisations qui sont décrites dans l’article, mais n’ont pas suffit à permettre de trouver une réfutation minimale pour une formule « difficile » de 6 variables.

Voici deux exemples de réfutation minimales produites pour la formule suivante de 5 variables :

   

Elle a été produite par un processus de recherche locale stochastique faisant évoluer une formule avec comme objectif de maximiser la taille des réfutations minimales de . Mon but était de tenter de trouver une formule 3-CNF de 5 variables ne pouvant être réfutée sans produire au moins une clause de 4 littéraux. Je ne suis pas parvenu à produire une telle formule et j’ignore s’il en existe, mais j’ai obtenu quelques formules qui, comme celle-ci, ont des réfutations minimale de taille différente selon qu’on autorise ou non la production de clauses de longueur 4, c’est à dire plus longues que les clauses initiales de .

Jusqu’à plus ample informé, produire des Réfutation par Résolution de taille minimale pour des formules ayant significativement plus de 5 variables reste donc un challenge.