Zur Seitennavigation oder mit Tastenkombination für den accesskey-Taste und Taste 1 
Zum Seiteninhalt oder mit Tastenkombination für den accesskey und Taste 2 

ONLINE im SoSe22: Algorithmisches Beweisen LAB - Einzelansicht

  • Funktionen:
Grunddaten
Veranstaltungsart Praktikum Langtext
Veranstaltungsnummer 160075 Kurztext
Semester SS 2022 SWS 4
Teilnehmer 1. Platzvergabe 15 Max. Teilnehmer 2. Platzvergabe 15
Rhythmus Jedes Semester Studienjahr
Credits für IB und SPZ
E-Learning
Hyperlink
Sprache Deutsch
Belegungsfrist Standardbelegung Wintersemester ab Mitte August/ Sommersemester ab Mitte Februar
Abmeldefristen B1 - Belegung ohne Abmeldung    21.02.2022 09:00:00 - 05.04.2022 08:29:59   
Nach Zulassung ist eine Abmeldung nur durch die Dozierenden möglich.
B2 - Belegung mit Abmeldung 6 Wochen    05.04.2022 08:30:00 - 23.05.2022 23:59:59   
Nach Zulassung ist eine Abmeldung auch durch die Teilnehmenden möglich.
B3 - Belegung ohne Abmeldung    24.05.2022 00:00:01 - 22.08.2022 07:59:59    aktuell
Nach Zulassung ist eine Abmeldung nur durch die Dozierenden möglich.
Termine Gruppe: 1-Gruppe iCalendar Export für Outlook
  Tag Zeit Rhythmus Dauer Raum Lehrperson (Zuständigkeit) Status Bemerkung fällt aus am Max. Teilnehmer 2. Platzvergabe
Einzeltermine anzeigen Mo. 12:00 bis 14:00 w. 11.04.2022 bis
11.07.2022
    findet statt  
Einzeltermine anzeigen Fr. 12:00 bis 14:00 w. 15.04.2022 bis
15.07.2022
    findet statt  
Gruppe 1-Gruppe:



Zugeordnete Personen
Zugeordnete Personen Zuständigkeit
Beyersdorff, Olaf, Universitätsprofessor, Dr.rer.nat. begleitend
Spachmann, Luc verantwortlich
Module / Prüfungen
Modul Prüfungsnummer Titel VE.Nr. Veranstaltungseinheit
FMI-IN0159 Algorithmisches Beweisen LAB
P-Nr. : 65591 Algorithmisches Beweisen LAB: Klausur o. mündl. Prüfung
65593 Algorithmisches Beweisen LAB: Praktikum
FMI-IN3162 Mastermodul Algorithmik/Theoretische Informatik II - 6 LP
P-Nr. : 352121 Mastermodul Algorithmik/Theoretische Informatik II - 6 LP: mündl. o. schriftl. Prüfung
352123 Mastermodul Algorithmik/Theoretische Informatik II - 6 LP: Vorlesung/Übung/Praktikum
FMI-IN3163 Mastermodul Algorithmik/Theoretische Informatik III - 6 LP
P-Nr. : 352131 Mastermodul Algorithmik/Theoretische Informatik III - 6 LP: mündl. o. schriftl. Prüfung
352133 Mastermodul Algorithmik/Theoretische Informatik III - 6 LP: Vorlesung/Übung/Praktikum
FMI-IN3161 Mastermodul Algorithmik/Theoretische Informatik I - 6 LP
P-Nr. : 352111 Mastermodul Algorithmik/Theoretische Informatik I - 6 LP: mündl. o. schriftl. Prüfung
352113 Mastermodul Algorithmik/Theoretische Informatik I - 6 LP: Vorlesung/Übung/Praktikum
FMI-IN3164 Mastermodul Algorithmik/Theoretische Informatik IV - 6 LP
P-Nr. : 352141 Mastermodul Algorithmik/Theoretische Informatik IV - 6 LP: mündl. o. schriftl. Prüfung
352143 Mastermodul Algorithmik/Theoretische Informatik IV - 6 LP: Vorlesung/Übung/Praktikum
Zuordnung zu Einrichtungen
Theoretische Informatik
Fakultät für Mathematik und Informatik
Inhalt
Kommentar

 

Literatur
  • Uwe Schöning, Jacobo Toran: Das Erfüllbarkeitsproblem SAT, Lehmanns 2012
  • Stasys Jukna: Boolean Function Complexity, Springer 2012
  • Handbook of Satisfiability, IOS Pres, 2009
Bemerkung

Umfang: 4 SWS Praktikum

Leistungspunkte: 4

Voraussetzungen

Empfohlene bzw. erwartete Vorkenntnisse:

  • FMI-IN0001 Algorithmen und Datenstrukturen
  • FMI-IN0005 Automaten und Berechenbarkeit
Leistungsnachweis

Voraussetzung für die Zulassung zur Modulprüfung:

  • Übungskriterien, die zum Modulbeginn festgelegt werden

Voraussetzung für die Vergabe von Leistungspunkten (Prüfungsform)

  • Klausur oder mündliche Prüfung (Festlegung erfolgt zu Beginn des Moduls)
Lerninhalte

Inhalt:

Algorithmische Begleitung der Vorlesung Algorithmisches Beweisen;

Prototyp-Implementierungen von Algorithmen zum SAT-Solving:

  • Hornformel
  • 2-KNF
  • Lokale Suche, random walk
  • DPLL, CDCL
  • QBF Expansion

 Experimente mit Solvern

  • Testen einfacher/harter Formeln
  • Kodierung von Problemen
  • Analyse von Formelklassen
  • Zufällige Formeln

Lern- und Qualifikationsziele:

  • Vertiefte Kenntnisse in Theoretischer Informatik, Logik und der algorithmischen Lösung von Erfüllbarkeitsproblemen
  • Befähigung zur beweistheoretischen Einordnung konkreter Formelklassen
  • Grundverständnis und Befähigung zur Implementierung moderner SAT-Algorithmen
  • Kenntnisse zum Einsatz moderner SAT- und QBF-Solver
  • Einsichten in Chancen und Grenzen moderner SAT-Solver
Zielgruppe
  • Wahlpflichtmodul (TIA, ALG) für den M.Sc. Informatik
  • Wahlpflichtmodul für den B.Sc. Informatik
  • Wahlpflichtmodul (Bereich Informatik) für den M.Sc. Bioinformatik
  • Wahlpflichtmodul (Angewandte Mathematik, Vertiefung Algorithmik, Nebenfach Informatik) für den M.Sc. Mathematik 
  • Wahlpflichtmodul (Nebenfach Informatik) für den B.Sc. Mathematik
  • Wahlpflichtmodul für den B.Sc. Wirtschaftswissenschaften, Schwerpunkt IMS[
  • Wahlpflichtmodul für den B.A. Ergänzungsfach Informatik

 

Strukturbaum
Die Veranstaltung wurde 6 mal im Vorlesungsverzeichnis SoSe 2022 gefunden:
Vertiefung Informatik  - - - 2
Informatik  - - - 3
Wahlpflichtmodule  - - - 6

Impressum | Datenschutzerklärung