Apprendre les bases de la résolution SAT (Boolean Satisfiability) et SMT (Satisfiability Modulo Theories)
Appliquer les techniques SAT/SMT à des problèmes réels tels que l'ordonnancement, la résolution de Sudoku, l'ajustement de rectangles et la vérification de programmes.
Comprendre les principaux algorithmes de résolution de SAT, notamment Resolution, DPLL et CDCL.
Utiliser la méthode du Simplexe et les techniques SMT pour raisonner sur les inégalités linéaires et les problèmes d'optimisation.
Compétences que vous acquerrez
Catégorie : Combinatoire
Combinatoire
Catégorie : Arithmétique
Arithmétique
Catégorie : Informatique théorique
Informatique théorique
Catégorie : Modélisation mathématique
Modélisation mathématique
Catégorie : Optimisation du modèle
Optimisation du modèle
Catégorie : Raisonnement déductif
Raisonnement déductif
Catégorie : Recherche opérationnelle
Recherche opérationnelle
Catégorie : Mathématiques appliquées
Mathématiques appliquées
Catégorie : Algèbre linéaire
Algèbre linéaire
Catégorie : Algorithmes
Algorithmes
Catégorie : Raisonnement logique
Raisonnement logique
Catégorie : Vérification et validation
Vérification et validation
Catégorie : Logique informatique
Logique informatique
Outils que vous découvrirez
Catégorie : Logiciels mathématiques
Logiciels mathématiques
Détails à connaître
Certificat partageable
Ajouter à votre profil LinkedIn
Évaluations
19 devoirs
Enseigné en Anglais
Découvrez comment les employés des entreprises prestigieuses maîtrisent des compétences recherchées
Dans ce cours, vous apprendrez à appliquer les outils de satisfiabilité (SAT/SMT) pour résoudre un large éventail de problèmes. Plusieurs exemples de base sont donnés pour avoir un aperçu des applications : l'ajustement de rectangles à appliquer pour l'impression d'affiches, les problèmes d'ordonnancement, la résolution de puzzles, et la correction de programmes. La théorie sous-jacente est également présentée : la résolution comme approche de base pour la satisfiabilité propositionnelle, le cadre CDCL pour passer à l'échelle pour les grandes formules, et la méthode du simplexe pour traiter les inégalités linéaires. L'approche légère pour suivre le cours Automated Reasoning : satisfiability consiste simplement à regarder les conférences et à faire les quiz correspondants. Pour avoir un aperçu du sujet, cette approche peut s'avérer efficace. Cependant, l'approche la plus intéressante est de s'en servir comme base pour appliquer SAT/SMT vous-même sur plusieurs problèmes, par exemple sur les problèmes présentés dans le devoir d'honneur.
Ce module présente SAT (satisfiabilité) et SMT (SAT modulo théories) à partir de zéro, et donne un certain nombre d'exemples d'application de SAT.
Inclus
6 vidéos2 lectures3 devoirs
Afficher les informations sur le contenu du module
6 vidéos•Total 58 minutes
Introduction générale et application à l'impression d'affiches•7 minutes
Introduction au SAT•8 minutes
Syntaxe et outils SMT•11 minutes
Problème des huit reines•9 minutes
Arithmétique binaire : addition•11 minutes
Arithmétique binaire : multiplication•13 minutes
2 lectures•Total 20 minutes
Exemples tirés de la conférence•10 minutes
Formule des huit reines en syntaxe SMT•10 minutes
3 devoirs•Total 90 minutes
Table de vérité•30 minutes
Porte dans l'addition binaire•30 minutes
Multiplication binaire•30 minutes
Applications SMT
Module 2•18 heures à terminer
Détails du module
Ce module présente un certain nombre d'applications de la satisfiabilité modulo la théorie des inégalités linéaires (SMT)
Inclus
4 vidéos2 lectures7 devoirs
Afficher les informations sur le contenu du module
4 vidéos•Total 33 minutes
Raccord rectangulaire•8 minutes
Résoudre le Sudoku•8 minutes
Programmation•9 minutes
Vérification de modèles délimités•9 minutes
2 lectures•Total 20 minutes
Formule de Sudoku au format SMT 2•10 minutes
Introduction•10 minutes
7 devoirs•Total 1 050 minutes
Raccord rectangulaire•30 minutes
Programmation•30 minutes
Vérification de modèles limités•30 minutes
Remplissage de camions pour une usine de magie•240 minutes
Une variante du sudoku•240 minutes
Planification des tâches•240 minutes
Correction du programme•240 minutes
Théorie et algorithmes pour les SAT basés sur la CNF
Module 3•3 heures à terminer
Détails du module
Ce module décrit comment une règle appelée Résolution permet de déterminer si une formule propositionnelle en forme normale conjonctive (CNF) est insatisfaisante. Il est montré comment une approche appelée DPLL fait le même travail, et comment elle est liée à la résolution. Enfin, nous montrons comment les solveurs SAT actuels implémentent et optimisent essentiellement la DPLL.
Inclus
6 vidéos5 devoirs
Afficher les informations sur le contenu du module
6 vidéos•Total 56 minutes
Résolution•10 minutes
Exemple de résolution•8 minutes
DPLL•10 minutes
Transformation de la DPLL en résolution•9 minutes
Les bases du CDCL•11 minutes
Optimisations du CDCL•7 minutes
5 devoirs•Total 120 minutes
Résolution•30 minutes
appliquer la résolution•30 minutes
DPLL•30 minutes
DPLL à la résolution•30 minutes
Les bases du CDCL•0 minutes
Théorie et algorithmes pour SAT/SMT
Module 4•1 heure à terminer
Détails du module
Ce module se compose de deux parties. La première partie concerne la transformation de formules propositionnelles arbitraires en CNF, conduisant à la transformation de Tseitin qui effectue ce travail de telle sorte que la taille de la formule transformée est linéaire par rapport à la taille de la formule originale. La deuxième partie concerne l'extension de SAT à SMT, en particulier pour traiter les inégalités linéaires. Il est montré comment la méthode du Simplex pour l'optimisation linéaire sert à cette fin ; la méthode du Simplex elle-même est expliquée en détail.
Inclus
6 vidéos4 devoirs
Afficher les informations sur le contenu du module
6 vidéos•Total 55 minutes
Transformer une formule propositionnelle en CNF•8 minutes
La transfomation de Tseitin•10 minutes
Introduction à la méthode du simplexe•7 minutes
Optimisation par la méthode du simplexe•12 minutes
Vérification de la faisabilité par la méthode du simplexe•9 minutes
La méthode du simplexe et le SMT•9 minutes
4 devoirs
Transformer une formule propositionnelle en CNF•0 minutes
La transfomation de Tseitin•0 minutes
Formulaire Slack•0 minutes
Optimisation par la méthode du simplexe•0 minutes
Instructeur
Évaluations de l’enseignant
Évaluations de l’enseignant
Nous avons demandé à tous les étudiants de fournir des commentaires sur nos enseignants au sujet de la qualité de leur pédagogie.
28DIGITAL est le moteur de l'innovation numérique en Europe, une plateforme multipartite, ancrée dans les valeurs européennes et ouverte sur le monde. Nous transformons la connaissance en innovation, transformons les start-ups en entreprises mondiales et formons la prochaine génération de talents numériques pour façonner un avenir numérique équitable, compétitif et centré sur l'humain.
nous travaillons à l'intersection de la science, des affaires et de la société, transformant les percées en IA, cybersécurité, robotique et informatique avancée en solutions qui favorisent l'innovation dans les technologies numériques, accélèrent la transition écologique et améliorent les vies. 28DIGITAL fournit un enseignement en ligne et en face-à-face sur l'innovation et l'entrepreneuriat afin d'améliorer la qualité, d'accroître la diversité et d'étendre la disponibilité d'un contenu de haut niveau provenant de 20 universités techniques de premier plan à travers l'Europe. Les universités offrent un mélange unique du meilleur de l'excellence technique, des compétences entrepreneuriales et de l'esprit aux ingénieurs et entrepreneurs numériques à tous les stades de leur carrière. Les partenaires académiques soutiennent la vision audacieuse de Coursera qui consiste à permettre à n'importe qui, n'importe où, de transformer sa vie en donnant accès aux meilleures expériences d'apprentissage au monde. Cela signifie que 28DIGITAL partage progressivement des parties de ses programmes d'éducation entrepreneuriale et académique pour démontrer son excellence et la rendre accessible à un public beaucoup plus large. Le portefeuille d'éducation en ligne de 28DIGITAL peut être utilisé dans des contextes d'éducation mixte, à la fois dans les programmes de maîtrise et de doctorat, et par les professionnels pour mettre à jour leurs connaissances
Pour quelles raisons les étudiants sur Coursera nous choisissent-ils pour leur carrière ?
Felipe M.
Étudiant(e) depuis 2018
’Pouvoir suivre des cours à mon rythme à été une expérience extraordinaire. Je peux apprendre chaque fois que mon emploi du temps me le permet et en fonction de mon humeur.’
Jennifer J.
Étudiant(e) depuis 2020
’J'ai directement appliqué les concepts et les compétences que j'ai appris de mes cours à un nouveau projet passionnant au travail.’
Larry W.
Étudiant(e) depuis 2021
’Lorsque j'ai besoin de cours sur des sujets que mon université ne propose pas, Coursera est l'un des meilleurs endroits où se rendre.’
Chaitanya A.
’Apprendre, ce n'est pas seulement s'améliorer dans son travail : c'est bien plus que cela. Coursera me permet d'apprendre sans limites.’
Avis des étudiants
4.8
45 avis
5 stars
80,43 %
4 stars
13,04 %
3 stars
6,52 %
2 stars
0 %
1 star
0 %
Affichage de 3 sur 45
K
KK
4·
Révisé le 16 août 2019
Good course, but some quizes are a bit confusing :)Thank you very much professor.
H
HS
5·
Révisé le 2 mai 2020
More programming problems (probably on the later half) would be really interesting and helpful
O
OE
5·
Révisé le 26 mai 2024
This course really opened my mind on the possibilities that can be achieved with the SMT solver. Great course!!!
Pour accéder aux supports de cours, aux devoirs et pour obtenir un certificat, vous devez acheter l'expérience de certificat lorsque vous vous inscrivez à un cours. Vous pouvez essayer un essai gratuit ou demander une aide financière. Le cours peut proposer l'option "Cours complet, pas de certificat". Cette option vous permet de consulter tous les supports de cours, de soumettre les évaluations requises et d'obtenir une note finale. Cela signifie également que vous ne pourrez pas acheter un certificat d'expérience.
Qu'est-ce que je recevrai si je souscris à cette Specializations ?
Lorsque vous vous inscrivez au cours, vous avez accès à tous les cours de la spécialisation et vous obtenez un certificat lorsque vous terminez le travail. Votre certificat électronique sera ajouté à votre page Réalisations - de là, vous pouvez imprimer votre certificat ou l'ajouter à votre profil LinkedIn.
Une aide financière est-elle disponible ?
Oui, pour certains programmes de formation, vous pouvez demander une aide financière ou une bourse si vous n'avez pas les moyens de payer les frais d'inscription. Si une aide financière ou une bourse est disponible pour votre programme de formation, vous trouverez un lien pour postuler sur la page de description.