Je vais expliquer un peu ce qu’est le problème SAT, parce que j’aurai l’occasion d’en reparler plus en détail bientôt (pour une certaine définition de bientôt dépendant de ma charge scolaire 🙂 ). C’est aussi une des briques fondamentales liées à la question « P = NP » ; j’avais commencé à écrire ce billet dans un prochain billet à propos de problèmes NP-complets, mais je crois que je peux faire un billet complet sur le sujet, ça m’évitera d’avoir la tentation de « faire vite ». L’autre raison pour laquelle je veux pas faire vite, c’est que je fais en ce moment un « projet de semestre » sur un sujet très très très voisin, et comme j’ai aussi l’intention de faire un billet sur ce que je fais plus précisément, ben ça ça sera fait.

SAT est une abréviation pour « boolean satisfiability problem », ou en français « problème de satisfaisabilité booléenne ». L’idée, c’est qu’on a une formule booléenne, ou formule SAT, et qu’on cherche à décider si on peut la résoudre ou pas.

Une formule SAT peut, par exemple, avoir cette tête là :

Il y a plusieurs éléments dans ce machin. Le premier élément, ce sont les variables – ici, x, y, z. On peut les voir comme les « inconnues » d’une équation : on veut ici savoir si on peut trouver des valeurs pour x, y et z. En plus de ça, on est dans un univers un peu bizarre, l’univers booléen : x, y et z ne peuvent prendre que la valeur 0 ou la valeur 1.

Après, il y a des symboles bizarres. , ça veut dire « ou », et , ça veut dire « et ». Les petites barres au-dessus de certaines lettres indiquent un négation. Les symboles se lisent comme ça :

Ou, si j’écris ça en toutes lettres :

• si x = 1, alors , sinon ( prend la valeur inverse de x)
• si x = 1, alors  ; si y = 1 alors  ; si x = 0 et y = 0, alors (« x OU y vaut 1 »). Il faut préciser que quand on dit « ou » dans ce contexte, ce n’est pas dans le même sens que « fromage ou dessert » : si on prend du fromage et du dessert, alors on prend du fromage ou du dessert (puisqu’on prend au moins l’un des deux). 
• si x = 1 et y = 1, alors , sinon (« x ET y valent tous les deux 1 »).

On peut combiner tous ces machins de la manière qu’on veut pour obtenir des formules booléennes. On s’intéresse en particulier aux formules du type que j’ai donné précédemment, qui sont appelées des formules « CNF » (pour « conjunctive normal form »). Ce type de formule est défini comme un ensemble de clauses, toutes reliées entre elles par des symboles (« et »). Une clause se compose d’un ou plusieurs littéraux (un littéral, des littéraux), qui sont soit une variable (par exemple x), soit sa négation (par exemple ) tous reliés entre eux par des symboles (« ou »). On veut donc que toutes les clauses aient comme valeur 1 (parce qu’on veut que la première ET la deuxième ET la troisième ET toutes les suivantes aient la valeur 1). Et le fait que chaque clause ait la valeur 1, ça se traduit par le fait qu’au moins un des littéraux de la formule ait la valeur 1 (parce qu’on veut que le premier littéral OU le deuxième OU le troisième OU… ait la valeur 1). Même remarque que précédemment, il peut arriver que tous les littéraux aient la valeur 1, ça renvoie quand même toujours 1. 

La question posée par une instance de SAT, c’est « est-ce que je peux trouver des valeurs pour toutes les variables de manière à ce que la formule complète ait pour valeur 1 ? ».

Reprenons l’exemple précédent, et nommons la formule F:

Si je veux regarder s’il existe des valeurs pour x, y et z qui font que la formule F vaut 1 (c’est-à-dire pour que la formule soit satisfaite), je peux toutes les énumérer et regarder ce qu’il se passe.

Mon petit tableau répond à la question « est-ce qu’il existe des valeurs pour x, y et z de sorte à ce que la formule F vaille 1 » (la réponse est oui), et il va même plus loin en donnant lesdites valeurs (par exemple, x = 1, y = 0, z = 1 sont des valeurs valides pour satisfaire la formule).

Le problème, c’est que c’est pas vraiment gérable dès qu’on commence à avoir beaucoup de variables. La raison, c’est que pour chaque variable, il faut que je regarde ce qu’il se passe pour sa valeur 0 et pour sa valeur 1. Donc j’ai deux choix pour la première variable ; deux choix pour la deuxième variable ; deux choix pour la troisième variable, etc. Les choix en question se multiplient : on voit ça dans le tableau au-dessus, il faut que je fasse une ligne pour toutes les combinaisons possibles de valeurs de variables. Donc, pour 3 variables, 2*2*2 = 2³ = 8 lignes. Pour 5 variables, on est déjà à 2*2*2*2*2 = 2⁵ = 32 lignes, et ça commence à être relou à faire à la main. Pour 20 variables, on est à 2²⁰ = 1.048.576 lignes, et ça commence à ne pas être vraiment instantané à calculer. Et ça augmente de plus en plus vite : les joies de la fonction puissance.

Pour ceux qui ont suivi les explications précédentes, ce n’est PAS un algorithme en temps polynomial ; c’est un algorithme en temps exponentiel. D’autant plus que je ne considère là que l’énumération de tous les cas et que je ne regarde même pas combien de temps il me faut pour conclure dans chacun des cas.

Du point de vue « classe de complexité », SAT fait partie des problèmes de la classe NP. Si on me donne une formule et des valeurs pour toutes les variables de la formule, je peux vérifier efficacement que, effectivement, ça marche : je peux vérifier qu’une formule peut être satisfaite si on m’en fournit la preuve.

Par contre, on ne sait pas s’il fait partie des problèmes de la classe P : on ne sait pas s’il existe un algorithme polynomial permettant de décider si, oui ou non, une formule peut être satisfaite ou non. On ne sait pas non plus s’il est en dehors des problèmes de la classe P : on ne sait pas s’il faut nécessairement un algorithme « plus puissant » qu’un algorithme polynomial pour le résoudre. Et répondre à cette question (et le prouver correctement) permettrait de répondre à la question « est-ce que P = NP ? » – mais pour ça, il faut que je parle de problèmes NP-complets, et je ferai ça dans le prochain billet 🙂

EDIT : bon, je re-précise un ou deux trucs, parce que tripa a pas COMPLÈTEMENT tort dans les commentaires. Quand je dis « on ne sait pas si », je veux parler du cas général, c’est-à-dire de n’importe quelle formule SAT. Après, il y a des cas où c’est « facile », c’est-à-dire qu’on peut conclure très vite. C’est par exemple le cas si on se restreint à des clauses avec deux littéraux (2-SAT) : dans ce cas précis, il y a un algorithme qui permet de conclure en temps linéaire (c’est-à-dire, en gros, qu’on lit la formule, et qu’on sait.) La difficulté intrinsèque du problème général ne donne pas vraiment d’indication sur les instances individuelles. C’est plutôt un point que je traiterai dans le billet suivant, parce que c’est aussi important de s’en souvenir, mais, bon. Tout ça pour dire que SAT c’est dur, mais qu’il y a des instances du problème qui sont faciles, et qu’il faut éventuellement se poser les bonnes questions avant de conclure qu’on n’a aucune chance de résoudre une formule donnée 🙂