%% nav-debut : généré par gen_navigation.py, ne pas modifier à la main %% > [!nav] > ↩ [[Code et Développement/Programmation/Optimisation de problème/Optimisation de problème|Accueil · Optimisation de problème]] > > | [[Code et Développement/Programmation/Optimisation de problème/02_Le problème du sac à dos\|← Le problème du sac à dos]] | | > |:---|---:| %% nav-fin %% # Satisfaisabilité (SAT) Ce chapitre présente le problème de satisfaisabilité, noté SAT. ## Énoncé Une formule de logique propositionnelle relie des variables booléennes par les connecteurs ET (∧), OU (∨) et NON (¬). Le problème SAT demande s'il existe des valeurs des variables qui rendent la formule vraie. Si de telles valeurs existent, la formule est **satisfaisable**. Sinon, elle est **insatisfaisable**. ## Forme normale conjonctive On étudie les formules en forme normale conjonctive (FNC). Un **littéral** est une variable ou sa négation : *x* ou ¬*x*. Une **clause** est une disjonction de littéraux : (*x* ∨ ¬*z* ∨ *y*). Une formule en FNC est une conjonction de clauses : (*x* ∨ ¬*z* ∨ *y*) ∧ (¬*y* ∨ *k*) ∧ (¬*k* ∨ ¬*x*). Toute formule de logique propositionnelle peut s'écrire en FNC. Les variantes de SAT se distinguent par le nombre de littéraux par clause. | Variante | Exemple | Difficulté | |---|---|---| | 1-SAT | *x* ∧ ¬*y* ∧ *z* ∧ ¬*k* | temps linéaire | | 2-SAT | (*x* ∨ ¬*z*) ∧ (¬*y* ∨ *k*) ∧ (¬*k* ∨ ¬*x*) | temps polynomial | | 3-SAT | (*x* ∨ *y* ∨ *z*) ∧ (*k* ∨ ¬*x* ∨ *y*) ∧ (¬*k* ∨ *x* ∨ ¬*y*) | NP-complet | ### 1-SAT Chaque clause contient un seul littéral. Chaque clause impose donc la valeur d'une variable. La formule est satisfaisable si elle ne contient pas à la fois *x* et ¬*x* pour une même variable. ### 2-SAT Chaque clause contient deux littéraux. Le problème se résout en temps polynomial à l'aide d'un graphe orienté, appelé graphe des implications. - Les sommets sont les littéraux : *x*, ¬*x*, *y*, ¬*y*, etc. - Chaque clause (*a* ∨ *b*) donne deux arcs : ¬*a* ⇒ *b* et ¬*b* ⇒ *a*. Si *a* est faux, *b* doit être vrai, et inversement. - La formule est satisfaisable si, pour chaque variable *x*, les sommets *x* et ¬*x* ne sont pas dans la même composante fortement connexe. Une composante fortement connexe est un ensemble de sommets où chaque sommet mène à chacun des autres en suivant les arcs. ### 3-SAT Chaque clause contient trois littéraux. Le problème 3-SAT est NP-complet. Toute formule en FNC se ramène en temps polynomial à une formule dont les clauses ont trois littéraux. 3-SAT est donc aussi difficile que SAT en général. ## Horn-SAT Une **clause de Horn** contient au plus un littéral positif. Une clause de Horn s'écrit comme une implication. Par exemple, (¬*a* ∨ ¬*b* ∨ *c*) équivaut à (*a* ∧ *b*) ⇒ *c*. - Les variables de gauche sont les **impliquants**. La variable de droite est l'**impliqué**. - Une clause réduite à un littéral positif, comme *c*, est un **fait** : son ensemble d'impliquants est vide. Le problème Horn-SAT porte sur les formules composées de clauses de Horn. Il se résout en temps polynomial. Horn-SAT et 1-SAT sont deux problèmes différents : une clause de Horn peut contenir plusieurs littéraux. ### Exemple On considère les propositions suivantes. 1. Si Mr White a un chien, alors Mme Brown a un chat. 2. Si Mr Green a un chien, alors il a aussi un chat. 3. Si Mr White a un chien et Mr Green a un chat, alors Mme Yellow a un chien. 4. Si Mme Brown et Mr Green ont un animal de la même espèce, alors Mr White a un chat. 5. Tous les hommes ont un chien. On définit huit variables booléennes. - *w*, *b*, *g* et *y* sont vraies si White, Brown, Green et Yellow ont un chien. - *W*, *B*, *G* et *Y* sont vraies si White, Brown, Green et Yellow ont un chat. Les propositions s'écrivent ainsi. 1. *w* ⇒ *B* 2. *g* ⇒ *G* 3. (*w* ∧ *G*) ⇒ *y* 4. ((*g* ∧ *b*) ⇒ *W*) ∧ ((*G* ∧ *B*) ⇒ *W*) 5. *w* ∧ *g* La proposition 4 donne deux clauses : une pour les chiens, une pour les chats. La proposition 5 donne deux faits : *w* et *g*. En Python, chaque clause est un couple (liste des impliquants, impliqué). ```python variables = ['w', 'b', 'g', 'y', 'W', 'B', 'G', 'Y'] clauses = [(['w'], 'B'), (['g'], 'G'), (['w', 'G'], 'y'), (['g', 'b'], 'W'), (['G', 'B'], 'W'), ([], 'w'), ([], 'g')] ``` ### Algorithme 1. Toutes les variables valent Faux. 2. On place dans une liste « à traiter » les impliqués des clauses dont l'ensemble d'impliquants est vide, c'est-à-dire les faits. 3. Tant que la liste « à traiter » n'est pas vide : - on retire la première variable *v* de la liste ; - *v* passe à Vrai ; - pour chaque clause qui a *v* parmi ses impliquants, on retire *v* de ses impliquants ; - si les impliquants de cette clause deviennent vides, son impliqué entre dans la liste « à traiter », s'il n'est pas déjà vrai ni déjà dans la liste. 4. On renvoie les valeurs. Les variables qui restent à Faux ne sont imposées par aucune clause. ```python def horn_sat(variables, clauses): """Renvoie les valeurs qui satisfont des clauses de Horn sans clause négative.""" valeurs = {v: False for v in variables} restes = [list(imp) for imp, conc in clauses] # copie : clauses n'est pas modifié a_traiter = [conc for imp, conc in clauses if not imp] while a_traiter: v = a_traiter.pop(0) valeurs[v] = True for k, (imp, conc) in enumerate(clauses): if v in restes[k]: restes[k].remove(v) if not restes[k] and not valeurs[conc] and conc not in a_traiter: a_traiter.append(conc) return valeurs print(horn_sat(variables, clauses)) # {'w': True, 'b': False, 'g': True, 'y': True, 'W': True, 'B': True, 'G': True, 'Y': False} ``` La fonction travaille sur une copie des impliquants. La liste `clauses` reste intacte après l'appel. La liste « à traiter » est parcourue dans l'ordre. Le déroulement est le même à chaque exécution. **À manipuler :** suivez la propagation variable par variable. ```sq-horn variables: w, b, g, y, W, B, G, Y w -> B g -> G w, G -> y g, b -> W G, B -> W -> w -> g w = Mr White a un chien b = Mme Brown a un chien g = Mr Green a un chien y = Mme Yellow a un chien W = Mr White a un chat B = Mme Brown a un chat G = Mr Green a un chat Y = Mme Yellow a un chat ``` ### Lecture du résultat Mr White et Mr Green ont chacun un chien et un chat. Mme Brown a un chat. Mme Yellow a un chien. Les variables *b* et *Y* restent à Faux : aucune proposition n'impose que Mme Brown ait un chien ni que Mme Yellow ait un chat. Ces situations restent possibles. Une clause sans littéral positif, comme (¬*a* ∨ ¬*b*), s'écrit (*a* ∧ *b*) ⇒ Faux. Si ses impliquants deviennent tous vrais, la formule est insatisfaisable. L'exemple n'en contient pas. ## SAT en forme normale conjonctive Des programmes appelés solveurs SAT traitent toute formule en FNC. Le module Python `python-sat` (`pysat`) en fournit plusieurs, comme Glucose. Dans ces solveurs, les variables sont des entiers : 1 représente *x*₁ et −1 représente ¬*x*₁. ```python from pysat.solvers import Glucose3 g = Glucose3() g.add_clause([-1, 2]) # (¬x₁ ∨ x₂) g.add_clause([-2, 3]) # (¬x₂ ∨ x₃) print(g.solve()) # True print(g.get_model()) # [-1, -2, -3] : x₁, x₂ et x₃ valent Faux ``` Ce bloc est une illustration de l'usage d'un solveur : le module `python-sat` s'installe avec `pip install python-sat` et ne s'exécute pas sur ce site. Le composant `sq-sat` ci-dessous donne le même verdict à partir de la table de vérité. La formule (¬*x*₁ ∨ *x*₂) ∧ (¬*x*₂ ∨ *x*₃) est satisfaisable. Par exemple, *x*₁, *x*₂ et *x*₃ valent Faux. Pour 3 variables, la table de vérité compte 2³ = 8 lignes. Elle donne la réponse sans solveur. **À manipuler :** repérez les lignes de la table qui rendent la formule vraie. ```sq-sat clauses: -1 2; -2 3 ``` On considère une autre formule à 8 clauses de 3 littéraux. - *a* = (*x*₁ ∨ *x*₂ ∨ *x*₃) - *b* = (¬*x*₁ ∨ ¬*x*₂ ∨ *x*₃) - *c* = (*x*₁ ∨ ¬*x*₂ ∨ *x*₃) - *d* = (*x*₁ ∨ *x*₂ ∨ ¬*x*₃) - *e* = (¬*x*₁ ∨ *x*₂ ∨ ¬*x*₃) - *f* = (¬*x*₁ ∨ ¬*x*₂ ∨ ¬*x*₃) - *g* = (¬*x*₁ ∨ *x*₂ ∨ *x*₃) - *h* = (*x*₁ ∨ ¬*x*₂ ∨ ¬*x*₃) S = *a* ∧ *b* ∧ *c* ∧ *d* ∧ *e* ∧ *f* ∧ *g* ∧ *h* Le solveur répond `False` : la formule est insatisfaisable. Chaque clause est fausse pour exactement une combinaison des trois variables. Les 8 clauses excluent les 8 combinaisons. Aucune combinaison ne rend S vraie. **À manipuler :** cliquez sur une ligne pour voir quelle clause est fausse. ```sq-sat clauses: 1 2 3; -1 -2 3; 1 -2 3; 1 2 -3; -1 2 -3; -1 -2 -3; -1 2 3; 1 -2 -3 ``` La table de vérité compte 2ⁿ lignes pour *n* variables. Cette méthode a une complexité exponentielle. %% nav-debut : généré par gen_navigation.py, ne pas modifier à la main %% > [!nav] > ↩ [[Code et Développement/Programmation/Optimisation de problème/Optimisation de problème|Accueil · Optimisation de problème]] > > | [[Code et Développement/Programmation/Optimisation de problème/02_Le problème du sac à dos\|← Le problème du sac à dos]] | | > |:---|---:| %% nav-fin %%