Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Leçon 916 : Formule du calcul propositionnel : représentation, forme normale, s

Leçon 916 : Formule du calcul propositionnel : représentation, forme normale, satisﬁabilité. Applications. Julie Parreaux 2018 - 2019 [2] Duparc, La logique pas à pas. [1] Cori et Lascar, La logique mathématique, tome 1. [3] Stern, Fondements mathématiques de l’informatique. Références pour la leçon Transformation de Tseitin 2-SAT est NL-complet (donc dans P) Développements de la leçon Plan de la leçon 1 Le langage de la logique propositionnelle 2 1.1 Syntaxe [2, p.68] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Représentations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Sémantique [2, p.83] . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.4 Théories et preuves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2 Équivalence de formules 3 2.1 Équivalence sémantique et équisatisﬁabilité [2, p.106] . . . . . . . . . . . . . . . . 3 2.2 Systèmes de connecteurs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.3 Formes normales conjonctives ou disjonctives . . . . . . . . . . . . . . . . . . . . 3 3 Résoudre la satisﬁabilité en pratique 4 3.1 Considérer des fragments de la logique . . . . . . . . . . . . . . . . . . . . . . . . 4 3.2 Essayer de résoudre astucieusement . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Motivation Défense La logique propositionnelle est une logique très simple permettant d’exprimer des contraintes : c’est la première logique que nous utilisons. 1 Ce qu’en dit le jury Le jury attend des candidats qu’ils abordent les questions de la complexité de la satisﬁa- bilité. Pour autant, les applications ne sauraient se réduire à la réduction de problèmes NP- complets à SAT. Une partie signiﬁcative du plan doit être consacrée à la représentation des formules et à leurs formes normales. 1 Le langage de la logique propositionnelle On formalise la logique grâce à une syntaxe, une sémantique et un lien entre les deux donné par un système de preuve (sur la syntaxe). Nous allons également donner plusieurs représentations possibles (dans un ordinateur) de la syntaxe. 1.1 Syntaxe [2, p.68] — Déﬁnition : langage avec connecteurs minimaux (induction) + exemples — Notation : Autres connecteurs — Remarque : Ambiguïté et parenthèses + exemples 1.2 Représentations Comment on représente les mots de ce langage dans un ordinateur ? Laquelle est la plus efﬁcace (sous quels critères) ? — Représentation linéaire — Représentation arborescente (fait apparaître l’induction) + Théorème de la lecture unique [1, p.57] (unicité de la représentation par l’arbre, représentation fortement non ambiguë) — Représentation DAG (direct acyclique graph) : moins de mémoire (utilisé pour la satis- ﬁabilité) — Représentation BD — Représentation circuit (donne de nouvelles classes de complexités) 1.3 Sémantique [2, p.83] Comment donner du sens à ce qu’on écrit ? Que signiﬁe ces formules ? — Valuation sur un modèle — Application : traduction du langage naturel — Problèmes : validité et satisﬁabilité (deux notions duales) — Une représentation : table de vérité (c’est une méthode pratique, ordonnée, pour tester la validité d’une formule) — Remarque : complexité de calcul (Conséquence de Cook) — Théorème Cook — Application : réduction de problème pour NP-dureté (problème de séparation des auto- mates) — Déﬁnition : tautologie / contradictions 2 1.4 Théories et preuves Vériﬁer que nous n’avons pas fait n’importe quoi avec ces déﬁnitions... — Déﬁnition : théorie — Théorème : compacité — Applications : coloriage de sous-graphe // pavage // logique du premier ordre — Déﬁnition : CNF (on voit après comment la mettre sous forme normale) + résolution — Théorème : correction et complétude Les autres logiques ? — Taille des arbres et certiﬁcats. 2 Équivalence de formules Aﬁn de trouver des moyens de résoudre le problème de satisﬁabilité, on peut chercher à mettre nos formules sous différentes forme qui sont équivalentes : elles expriment les mêmes contraintes. Pour cela nous avons besoins de la notions d’équivalence et de formes normales. 2.1 Équivalence sémantique et équisatisﬁabilité [2, p.106] Comparer deux formules c’est connaître les modèles qui les discrimine (satisfait une des formule mais pas l’autre). Lorsque nous ne pouvons pas les différentier, nous parlons d’équi- valence sémantique (c’est l’équivalence que l’on souhaite). — Déﬁnition : équivalence sémantique + Exemples : loi de Morgan — Proposition : caractérisation avec la validité — Conséquence : Complexité du problème VALIDITE — Déﬁnition : équisatisﬁabilité (l’équivalence sémantique est trop contraignante mais pour la satisﬁabilité, celle-ci sufﬁt) — Proposition : équivalent implique équisatisﬁable. 2.2 Systèmes de connecteurs L’ensemble des connecteurs logiques, appelé système de connecteurs, que nous choisissons pour écrire nos formules peuvent exprimer plus ou moins de choses. On en veut le moins de symbole possibles pour décrire notre logique. — Déﬁnition : systèmes complets et minimaux + Exemples — Proposition : {¬, ∨}, {¬, ∧}, {nand} sont des systèmes complets minimaux. — Remarque : {¬, ∧, ∨} est un système complet mais pas minimal. 2.3 Formes normales conjonctives ou disjonctives Les formes normales sont une manière de représenté une formule par une autre formule dont les connecteurs logiques sont restreints et ordonnés selon un certain ordre. On présente leur mise en forme, leurs points forts et leurs limites Forme normale négative Elle est à l’origine de toutes les autres — Déﬁnition : Forme normale négative (par sa grammaire) — Proposition : Transformation en une forme normale négative 3 Forme normale conjonctive — Proposition : Existence d’une formule CNF équivalente + Remarque : transformation expo- nentielle (ϕn = (a1 ∧b1) ∨· · · ∨(an ∧bn)) Remarque : C’est une forme normale négative — Proposition : Existence d’une formule CNF équisatisﬁable de taille linéaire (Transforma- tion de Tseitin) DEV — Corollaire : Le problème CNF-SAT est NP-complet — Remarque : Le problème CNF-VALIDE est dans P. Forme normale disjonctive Les formules conjonctives (et uniquement conjonctives) per- mettent de représenter un modèle. — Déﬁnitions : forme normale disjonctive DNF — Proposition : Existence d’une formule DNF équivalente — Théorème : Le problème DNF-SAT est dans P — Conséquence : Par Cook et P ̸= NP, transformation exponentielle — Exemple : ϕn = (a1 ∨b1) ∧· · · ∧(an ∨bn) — Remarque : Le problème DNF-VALIDE est dans NP-complet 3 Résoudre la satisﬁabilité en pratique On a vu que savoir si une formule est satisﬁable est difﬁcile. Cependant, en pratique on est souvent amené à résoudre cette question : on pose des contraintes (emplois du temps) ou issue de problème NP-complet. On aimerai alors un moyen de résoudre la satisﬁabilité de manière efﬁcace. 3.1 Considérer des fragments de la logique Limiter la logique (si le problème le permet) peut nous donner des algorithmes qui ré- solvent la satisﬁabilité en temps linaire. — Problème : 3SAT -> NP-complet (pas assez réduit) — Problème : 2SAT -> NL-dur (donc dans P) DEV Attention expressivité n’est pas la même — Application : problème d’ordonnancement multiprocesseurs où les processeurs n’ont que deux créneaux pour les tâches — Problème : Horn -> P — Application [3] : Prolog avec les clauses de Horn — Application : Analyse syntaxique : calcul de premier, LL(1), problèmes sur grammaires algébriques 3.2 Essayer de résoudre astucieusement Si on provient d’un problème NP-complet, on peut mettre la formule sous forme CNF et résoudre à l’aide d’un algorithme dont le pire cas s’exécute en temps exponentiel mais dont on espère que celui-ci soit meilleur dans la pratique. — DPLL / CDLL — Application : SAT-solver (Un des moyen de contrer la NP-complétude) 4 Quelques notions importantes Équivalence sémantique et équisatisﬁabilité Comparer deux formules c’est connaître les modèles qui les discrimine (satisfait une des formule mais pas l’autre). Lorsque nous ne pouvons pas les différentier, nous parlons d’équi- valence sémantique (c’est l’équivalence que l’on souhaite). Cependant être sémantiquement équivalent est une contrainte forte pour notre but de résoudre la satisﬁabilité. On va alors déﬁnir une deuxième notion ; l’équisatisﬁablité. Formules sémantiquement équivalentes [2, p.106] On rappelle qu’une formule est satis- ﬁable s’il existe un modèle (une valuation dans notre uploads/Philosophie/ 916-logiquepropositionnelle.pdf