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.
Durée limitée ! Obtenez Coursera Plus avec 30 % de réduction.
Réinitialiser. Réinventer. Atteindre de nouveaux objectifs professionnels. Profitez de votre offre maintenant.
Raisonnement automatisé : satisfiabilité
Enseigné en Anglais
Certains éléments de contenu peuvent ne pas être traduits
4 592 déjà inscrits
(43 avis)
Détails à connaître
Ajouter à votre profil LinkedIn
19 quizzes
Découvrez comment les employés des entreprises prestigieuses maîtrisent des compétences recherchées
Obtenez un certificat professionnel
Ajoutez cette qualification à votre profil LinkedIn ou à votre CV
Partagez-le sur les réseaux sociaux et dans votre évaluation de performance
Il y a 4 modules dans ce cours
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 quizzes
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 quizzes
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 quizzes
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 quizzes
Instructeur
Offert par
Recommandé si vous êtes intéressé(e) par Algorithmes
University of Colorado Boulder
University of Leeds
Stanford University
Pour quelles raisons les étudiants sur Coursera nous choisissent-ils pour leur carrière ?
Avis des étudiants
Affichage de 3 sur 43
43 avis
- 5 stars
81,39 %
- 4 stars
13,95 %
- 3 stars
4,65 %
- 2 stars
0 %
- 1 star
0 %
Ouvrez de nouvelles portes avec Coursera Plus
Accès illimité à plus de 7 000 cours de renommée internationale, à des projets pratiques et à des programmes de certificats reconnus sur le marché du travail, tous inclus dans votre abonnement
Faites progresser votre carrière avec un diplôme en ligne
Obtenez un diplôme auprès d’universités de renommée mondiale - 100 % en ligne
Rejoignez plus de 3 400 entreprises mondiales qui ont choisi Coursera pour les affaires
Améliorez les compétences de vos employés pour exceller dans l’économie numérique
Foire Aux Questions
L'accès aux cours et aux devoirs dépend de votre type d'inscription. Si vous suivez un cours en mode audit, vous pourrez consulter gratuitement la plupart des supports de cours. Pour accéder aux devoirs notés et obtenir un certificat, vous devrez acheter l'expérience de certificat, pendant ou après votre audit. Si vous ne voyez pas l'option d'audit :
Il se peut que le cours ne propose pas d'option d'audit. Vous pouvez essayer un essai gratuit ou demander une aide financière.
Le cours peut proposer l'option "Cours complet, pas de certificat" à la place. 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.
Lorsque vous vous inscrivez au cours, vous avez accès à tous les cours de la Specializations, et vous obtenez un certificat lorsque vous terminez le travail. Votre certificat électronique sera ajouté à votre page de réalisations - de là, vous pouvez imprimer votre certificat ou l'ajouter à votre profil LinkedIn. Si vous souhaitez uniquement lire et visualiser le contenu du cours, vous pouvez auditer le cours gratuitement.
Si vous vous êtes abonné, vous bénéficiez d'une période d'essai gratuite de 7 jours pendant laquelle vous pouvez annuler votre abonnement sans pénalité. Après cette période, nous ne remboursons pas, mais vous pouvez résilier votre abonnement à tout moment. Consultez notre politique de remboursement complète.