Le problème SAT

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à :

(x \vee y \vee z) \wedge (\bar x \vee \bar y) \wedge (\bar x \vee y \vee z)

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. \vee, ça veut dire « ou », et \wedge, ça veut dire « et ». Les petites barres au-dessus de certaines lettres indiquent un négation. Les symboles se lisent comme ça :

\begin{array}{|c|c||c|c|c|c|} \hline x & y & \bar x &\bar y & x \vee y & x \wedge y \\ \hline 0 & 0 & 1 & 1 & 0 & 0 \\ \hline 0 & 1 & 1 & 0 & 1 & 0 \\ \hline 1 & 0 & 0 & 1 & 1 & 0 \\ \hline 1 & 1 & 0 & 0 & 1 & 1 \\ \hline \end{array}

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

  • si x = 1, alors \bar x = 0, sinon \bar x = 1 (\bar x prend la valeur inverse de x)
  • si x = 1, alors x \vee y = 1 ; si y = 1 alors x \vee y = 1 ; si x = 0 et y = 0, alors x \vee y = 0 (« 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 x \wedge y = 1, sinon x \wedge y = 0 (« 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 \wedge (« 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 bar x) tous reliés entre eux par des symboles \vee (« 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:

F = (x \vee y \vee z) \wedge (\bar x \vee \bar y) \wedge (\bar x \vee y \vee z)

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.

\begin{array}{|c|c|c||c|c|c||c|} \hline x & y & z & x \vee y \vee z & \bar x \vee \bar y & \bar x \vee y \vee z & F \\  \hline 0 & 0 & 0 & 0 & 1 & 1 & 0 \\  \hline 0 & 0 & 1 & 1 & 1 & 1 & 1 \\  \hline 0 & 1 & 0 & 1 & 1 & 1 & 1\\  \hline 0 & 1 & 1 & 1 & 1 & 1 & 1\\  \hline 1 & 0 & 0 & 1 & 1 & 0 & 0 \\  \hline 1 & 0 & 1 & 1 & 1 & 1 & 1 \\  \hline 1 & 1 & 0 & 1 & 0 & 1 & 0\\  \hline 1 & 1 & 1 & 1 & 0 & 1 & 0\\  \hline \end{array}

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 🙂

14 commentaires sur « Le problème SAT »

    1. ‘Bsolument pas. Je ne dis rien quant à l’arité des problèmes SAT que je considère. Par conséquent, SAT, c’est dur. Il se trouve que les instances 2-SAT de SAT sont faciles. Il se trouve aussi que, mettons, SAT avec moins de 2^k clauses, c’est facile aussi. Il se trouve que SAT qui rentre dans le cadre du Lovasz Local Lemma, c’est facile aussi. Il n’empêche que SAT, c’est dur.

      1. (rha, je déteste laisser un commentaire sans preview)

        Je n’ai pas vraiment le temps de débattre, du coup je vais me cantonner à te laisser mon avis. À savoir, pour ton commentaire:

        – « Je ne dis rien quant à l’arité des problèmes SAT que je considère » → oui
        – « SAT, c’est dur » → oui (pour moi en tout cas 😉
        – « Par conséquent, » → non

        Et pour ton dernier paragraphe: je l’ai trouvé hâtif au point d’induire en erreur. (en fait il gagnerait à intégrer ton commentaire.) Mais peut-être te réserves-tu pour un prochain article?

        RÀV, mais tant qu’à poster sans preview, je me devais de te signaler que sous ma config «boulot», qui risque d’être courante (Chrome sous Windows), plein de caractères s’affichent en carré. Probablement l’espace fine insécable, vu le placement à proximité de guillemets et de points-virgules. C’est pas beau et c’est pas strictement de ta faute, mais… c’est pas beau.

  1. Hop, j’ai fait un edit, j’espère que ça clarifie. Et ouais, je compte plus ou moins faire un article sur les cas « faciles » de SAT à l’occasion – disons que c’est un sujet qui me vient à l’esprit si je cherche un thème de billet dans le coin 😉
    Bon, et je viens de mettre un preview, je sais pas s’il marche bien, mais je suis en train de tester, là 😛
    Quant aux caractères en carré, là j’avoue un certain « putain de bordel de merde, chier ». Parce qu’entre les espaces non insécables qui sont assez dégueu il faut le dire, les non-fines insécables que je peux pas foutre dans l’éditeur WP pour une raison qui m’échappe, et les fines insécables qui apparemment passent pas sous Zindoz….. je fais quoi, moi ?

    1. Bon, je viens d’allumer un Windows pour jeter un œil au problème, et, heuuuuu, ça march’chémoi ™. Du coup, je crois que c’est encore moins strictement de ma faute 😛

      1. Et il est à jour ton Chrome je suppose ? ça doit pas être un problème de polices système si ça marche dans FFX… à moins que FFX ne convertisse à la volée…? bizarre (et relou 😦 )

  2. Bonjour,
    Merci pour cet article , il m’a aidé vraiment de bien comprendre le problème SAT.
    J’aimerais bien comprendre la réduction du problème couverture de sommets de taille k vers le problème SAT.

    je vous remercie d’avance.

Laisser un commentaire

Entrez vos coordonnées ci-dessous ou cliquez sur une icône pour vous connecter:

Logo WordPress.com

Vous commentez à l'aide de votre compte WordPress.com. Déconnexion / Changer )

Image Twitter

Vous commentez à l'aide de votre compte Twitter. Déconnexion / Changer )

Photo Facebook

Vous commentez à l'aide de votre compte Facebook. Déconnexion / Changer )

Photo Google+

Vous commentez à l'aide de votre compte Google+. Déconnexion / Changer )

Connexion à %s