enthaltenIn diesem Kurs lernen Sie, wie Sie die Werkzeuge der Erfüllbarkeit (SAT/SMT) anwenden, um eine Vielzahl von Problemen zu lösen. Es werden einige grundlegende Beispiele gegeben, um einen Eindruck von den Anwendungen zu bekommen: das Einpassen von Rechtecken, die für den Druck von Postern verwendet werden sollen, Terminplanungsprobleme, das Lösen von Rätseln und die Korrektheit von Programmen. Außerdem wird die zugrundeliegende Theorie vorgestellt: die Auflösung als grundlegender Ansatz für die propositionale Erfüllbarkeit, das CDCL-Framework zur Skalierung für große Formeln und die Simplex-Methode zur Behandlung linearer Ungleichungen. Der leichtgewichtige Ansatz, um den Kurs Automated Reasoning: satisfiability zu verfolgen, besteht darin, sich nur die Vorlesungen anzusehen und die entsprechenden Quizfragen zu beantworten. Um ein Gefühl für das Thema zu bekommen, mag das gut funktionieren. Der weitaus interessantere Ansatz besteht jedoch darin, SAT/SMT selbst auf verschiedene Probleme anzuwenden, zum Beispiel auf die in der Ehrenaufgabe vorgestellten Probleme.
(43 Bewertungen)
Wichtige Details
Zu Ihrem LinkedIn-Profil hinzufügen
19 Aufgaben
Erfahren Sie, wie Mitarbeiter führender Unternehmen gefragte Kompetenzen erwerben.
Erwerben Sie ein Karrierezertifikat.
Fügen Sie diese Qualifikation zur Ihrem LinkedIn-Profil oder Ihrem Lebenslauf hinzu.
Teilen Sie es in den sozialen Medien und in Ihrer Leistungsbeurteilung.
In diesem Kurs gibt es 4 Module
Dieses Modul führt von Grund auf in SAT (Erfüllbarkeit) und SMT (SAT modulo theories) ein und gibt eine Reihe von Beispielen für die Anwendung von SAT.
Das ist alles enthalten
6 Videos2 Lektüren3 Aufgaben
Dieses Modul zeigt eine Reihe von Anwendungen der Erfüllbarkeit modulo der Theorie der linearen Ungleichungen (SMT)
Das ist alles enthalten
4 Videos2 Lektüren7 Aufgaben
Dieses Modul beschreibt, wie eine Regel namens Resolution dazu dient, festzustellen, ob eine propositionale Formel in konjunktiver Normalform (CNF) nicht erfüllbar ist. Es wird gezeigt, wie ein Ansatz namens DPLL die gleiche Aufgabe erfüllt und wie er mit Resolution zusammenhängt. Schließlich wird gezeigt, wie aktuelle SAT-Solver die DPLL im Wesentlichen implementieren und optimieren.
Das ist alles enthalten
6 Videos5 Aufgaben
Dieses Modul besteht aus zwei Teilen. Im ersten Teil geht es darum, beliebige Aussagenformeln in CNF umzuwandeln, was dazu führt, dass die Tseitin-Transformation diese Aufgabe so erledigt, dass die Größe der umgewandelten Formel linear zur Größe der ursprünglichen Formel ist. Im zweiten Teil geht es um die Erweiterung von SAT auf SMT, insbesondere um den Umgang mit linearen Ungleichungen. Es wird gezeigt, wie die Simplex-Methode für lineare Optimierung für diese Aufgabe geeignet ist; die Simplex-Methode selbst wird ausführlich erklärt.
Das ist alles enthalten
6 Videos4 Aufgaben
Dozent
von
Empfohlen, wenn Sie sich für Algorithmen interessieren
Duke University
Arizona State University
Intel
Warum entscheiden sich Menschen für Coursera für ihre Karriere?
Bewertungen von Lernenden
43 Bewertungen
- 5 stars
81,39 %
- 4 stars
13,95 %
- 3 stars
4,65 %
- 2 stars
0 %
- 1 star
0 %
Zeigt 3 von 43 an
Geprüft am 26. Mai 2024
This course really opened my mind on the possibilities that can be achieved with the SMT solver. Great course!!!
Geprüft am 2. Mai 2020
More programming problems (probably on the later half) would be really interesting and helpful
Geprüft am 9. März 2020
The course is a great introduction to satisfiability problem and its wide range of applications in day to day life. Honors assignments really helped me understand the core concepts better.
Neue Karrieremöglichkeiten mit Coursera Plus
Unbegrenzter Zugang zu 10,000+ Weltklasse-Kursen, praktischen Projekten und berufsqualifizierenden Zertifikatsprogrammen - alles in Ihrem Abonnement enthalten
Bringen Sie Ihre Karriere mit einem Online-Abschluss voran.
Erwerben Sie einen Abschluss von erstklassigen Universitäten – 100 % online
Schließen Sie sich mehr als 3.400 Unternehmen in aller Welt an, die sich für Coursera for Business entschieden haben.
Schulen Sie Ihre Mitarbeiter*innen, um sich in der digitalen Wirtschaft zu behaupten.
Häufig gestellte Fragen
Der Zugang zu Vorlesungen und Aufgaben hängt von der Art Ihrer Einschreibung ab. Wenn Sie einen Kurs im Prüfungsmodus belegen, können Sie die meisten Kursmaterialien kostenlos einsehen. Um auf benotete Aufgaben zuzugreifen und ein Zertifikat zu erwerben, müssen Sie die Zertifikatserfahrung während oder nach Ihrer Prüfung erwerben. Wenn Sie die Prüfungsoption nicht sehen:
Der Kurs bietet möglicherweise keine Prüfungsoption. Sie können stattdessen eine kostenlose Testversion ausprobieren oder finanzielle Unterstützung beantragen.
Der Kurs bietet möglicherweise stattdessen die Option 'Vollständiger Kurs, kein Zertifikat'. Mit dieser Option können Sie alle Kursmaterialien einsehen, die erforderlichen Bewertungen abgeben und eine Abschlussnote erhalten. Dies bedeutet auch, dass Sie kein Zertifikat erwerben können.
Wenn Sie sich für den Kurs einschreiben, erhalten Sie Zugang zu allen Kursen der Specializations, und Sie erhalten ein Zertifikat, wenn Sie die Arbeit abgeschlossen haben. Ihr elektronisches Zertifikat wird Ihrer Erfolgsseite hinzugefügt - von dort aus können Sie Ihr Zertifikat ausdrucken oder zu Ihrem LinkedIn-Profil hinzufügen. Wenn Sie die Kursinhalte nur lesen und ansehen möchten, können Sie den Kurs kostenlos besuchen.
Wenn Sie ein Abonnement abgeschlossen haben, erhalten Sie eine kostenlose 7-tägige Testphase, in der Sie kostenlos kündigen können. Danach gewähren wir keine Rückerstattung, aber Sie können Ihr Abonnement jederzeit kündigen. Siehe unsere vollständigen Rückerstattungsbedingungen.