Seminar Wissensbasierte Systeme
Prof. Dr. Hans Kleine Büning / Dr. Uwe Bubeck
Wintersemester 2011 / 2012
Was hier zu finden ist...
Anmerkung: Bei Problemen im Zusammenhang mit dieser Veranstaltung bitte Herrn Bubeck kontaktieren.
Aktuelles
- 19.10.2011 Vorbesprechung
- bis 26.10.2011 Veröffentlichung von Themenvorschlägen und Diskussion eigener Vorschläge
- bis 02.11.2011 Themenauswahl und -zuordnung
- bis 16.11.2011 Abgabe der Gliederung
- bis 19.12.2011 Abgabe der schriftlichen Ausarbeitung
- bis 12.01.2012 Einreichen der Peer Reviews
- 27.01.2012 Blockseminar mit Vorträgen
- bis 17.02.2012 Abgabe der überarbeiteten Ausarbeitungen
Allgemeine Informationen
| Dozent: |
Prof. Dr. Hans Kleine Büning Dr. Uwe Bubeck |
| Umfang: | 2 SWS Seminar |
| Termin: | Blockveranstaltung nach Absprache |
| Modul (2004): | III 1.7 Wissensbasierte Systeme (Kleine Büning) |
| Modul (2009): | III 1.4 Wissensbasierte Systeme (Kleine Büning) |
Themen
Das Seminar Wissensbasierte Systeme steht dieses Semester im Zeichen der Wissensrepräsentation und -verarbeitung mit Logik. Dieser Bereich bietet nicht nur Raum für interessante theoretische Fragestellungen, sondern auch vielfältige anwendungsorientierte und technische Aspekte. Insbesondere SAT-Solver haben sich inzwischen zu leistungsfähigen universellen Problemlösern entwickelt. Sie kommen zum Beispiel in den Paketverwaltungen von Eclipse oder diversen Linux-Distributionen vor oder bilden die Grundlage von Verifikationstools. Solche Anwendungen können genauso Themen des Seminars sein wie clevere Suchstrategien und Implementierungsaspekte von Solvern.
Themenvorschläge:- Nicht-chronologisches Backtracking und Lernen von Klauseln in SAT- oder QBF-Solvern
J. Marques-Silva, I. Lynce and S. Malik. Conflict-Driven Clause Learning SAT Solvers, Handbook of Satisfiability, IOS Press, 2009 - Redundanzerkennung und Vereinfachungstechniken in SAT- oder QBF-Solvern (Breitlauch)
M. Heule, M. Järvisalo and A. Biere. Efficient CNF Simplification based on Binary Implication Graphs, Proc. Theory and Applications of Satisfiability Testing (SAT 2011), Springer LNCS 6695, pp. 201-215, 2011 - Effiziente Datenstrukturen in modernen SAT-Solvern (Martens)
A. Biere. PicoSAT Essentials, Journal on Satisfiability, Boolean Modeling and Computation 4: 75-97, 2008
I. Lynce and J. Marques-Silva. Efficient data structures for backtrack search SAT solvers, Annals of Mathematics and Artificial Intelligence 43(1):137-152, 2005 - Maschinelle Lernverfahren zur Algorithmenauswahl in Portfolio-basierten SAT-Solvern (Lüers)
L. Xu, F. Hutter, H. H. Hoos and K. Leyton-Brown. SATzilla: Portfolio-based Algorithm Selection for SAT, Journal of Artificial Intelligence Research, 32:565-606, 2008 - Bestimmung minimal unerfüllbarer Teilformeln
J. Marques-Silva and I. Lynce. On Improving MUS Extraction Algorithms, Proc. Theory and Applications of Satisfiability Testing (SAT 2011), Springer LNCS 6695, pp. 159-173, 2011 - Schaltkreisverifikation durch Black-Box-Äquivalenztests
C. Scholl and B. Becker. Checking Equivalence for Partial Implementations, Proc. IEEE Design Automation Conference (DAC 2001), 238-243, 2001 - Bounded Model Checking mit partiellen Kripke-Strukturen
H. Wehrheim. Bounded Model Checking for Partial Kripke Structures, Proc. 5th Intl. Coll. on Theoretical Aspects of Computing (ICTAC 2008), Springer LNCS 5160, pp. 380-394, 2008 - 01X-Logik und QBF
M. Herbstritt and B. Becker, On Combining 01X-Logic and QBF, Proc. Computer Aided Systems Theory (EUROCAST 2007), Springer LNCS 4739, pp. 531-538, 2007 - Zertifikate für die Antworten von QBF-Solvern (Phan)
V. Balabanov, J. Jiang, Resolution Proofs and Skolem Functions in QBF Evaluation and Applications, Proc. 23rd Intl. Conf. on Computer Aided Verification (CAV 2011), Springer LNCS 6806, pp. 149-164, 2011 - Quantorexpansion in QBF
U. Bubeck and H. Kleine Büning. Bounded Universal Expansion for Preprocessing QBF, Proc. Theory and Applications of Satisfiability Testing (SAT 2007), Springer LNCS 4501, pp. 244-257, 2007
- Satisfiability Modulo Theories
H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras and C. Tinelli. DPLL(T): Fast Decision Procedures, Proc. 16th Intl. Conf. on Computer Aided Verification (CAV 2004), Springer LNCS 3114, pp. 175-188, 2004 - Schaltkreisbasierte SAT-Solver
A. Kuehlmann, M. Ganai and V. Paruthi. Circuit-based Boolean Reasoning, Proc. Design Automation Conference (DAC 2001), pp. 232-237, 2001
Bei der Auswahl von Themen ist zu berücksichtigen, daß ein Thema in Breite und Tiefe bearbeitet werden sollte, d.h. zur Bearbeitung gehört z.B.
- ein Überblick über mögliche Methoden (oder notwendige Schritte) zur Bearbeitung einer Aufgabenstellung mit Erläuterungen, Vor- und Nachteilen,
- eine detaillierte Beschreibung einer Methode (eines Aspektes) mit Vorstellung von Theorie, Algorithmen, Komplexitäten, ...
Organisation
PrüfungsmodalitätenFür das Seminar ist je nach Studiengang und Art der Prüfung eine Anmeldung über PAUL oder das Prüfungssekretariat erforderlich. Dies gilt z.B. für Master Informatik (2004), die Einzelprüfungen ablegen, und für Winfos. Im Zweifelsfall bitte beim Prüfungssekretariat nachfragen.
Modulprüfungen Master Informatik werden in den normalen Anmeldefristen angemeldet.
Für eine Modulprüfung mit einem Seminar geht die sogenannte Seminarvornote in die Gesamtbewertung ein. Die Seminarvornote wird über die Leistungen während des Seminars erworben, insbesondere durch Ausarbeitung und Vortrag (siehe unten). Die Seminarvornote für eine Modulprüfung bei Herrn Kleine Büning muss mindestens 4.0 sein. Für die Prüfung eines Seminars im Rahmen einer Modulprüfung für Informatik Master 2009 ist keine separate Prüfungsanmeldung für das Seminar erforderlich, sondern nur eine Anmeldung zur Modulprüfung.
Für eine Seminarvornote von mindestens 4.0 sind folgende Leistungen erforderlich:
- termingerechte Abgabe einer sinnvollen Gliederung,
- termingerechte Abgabe der schriftlichen Ausarbeitung,
- termingerechte Abgabe der Peer-Reviews zu 2 anderen Ausarbeitungen,
- Anwesenheit und Beteiligung an den Diskussionen während der Blocktermine,
- Vortrag von 35-45 Minuten Dauer anhand von Folien,
- termingerechte Abgabe der entsprechend der Reviews überarbeiteten Ausarbeitung.
Werden diese Bedingungen nicht eingehalten, erfolgt eine Bewertung mit 5.0, falls keine stichhaltigen Gründe vorgebracht werden können (z.B. Attest).
Die Seminarvornote wird dann folgendermaßen berechnet:
- 45% Note für Ausarbeitung,
- 45% Note für Vortrag + Folien + Diskussion zum eigenen Vortrag,
- 10% Note für eigene Peer-Reviews und Berücksichtigung anderer Reviews in überarbeiteter Ausarbeitung.
Zeitplan
- 19.10.2011 Vorbesprechung
- bis 26.10.2011 Veröffentlichung von Themenvorschlägen und Diskussion eigener Vorschläge
- bis 02.11.2011 Themenauswahl und -zuordnung
- bis 16.11.2011 Abgabe der Gliederung (Prüfungsleistung)
- bis 19.12.2011 Abgabe der schriftlichen Ausarbeitung (Prüfungsleistung)
- bis 12.01.2012 Einreichen der Peer Reviews (Prüfungsleistung)
- 27.01.2012 Blockseminartage mit Vorträgen (Prüfungsleistung)
- bis 17.02.2012 Abgabe der überarbeiteten Ausarbeitungen (Prüfungsleistung)
Dokumente
- Gliederung: (ca. 2-3 Seiten)
- Angabe des Titels und des Verfassers,
- Vorbemerkungen zu Thema und Konzeption,
- Kapitelüberschriften mit stichwortartiger Beschreibung des vorgesehenen Inhalts und des vorgesehenen Umfangs,
- Literaturverzeichnis mit Angabe der wichtigen Quellen für Breite (Überblick) und Tiefe (spezielle Aspekte).
- Ausarbeitung:
- Umfang 13 - 16 Seiten Text ohne Literaturverzeichnis und Zusammenfassung und Titel (Abweichungen nach oben eingeschränkt möglich, bitte rückfragen),
- Einbinden von Bildern ist häufig sehr sinnvoll, je nach Schöpfungshöhe können sie auch auf den Text angerechnet werden (nicht bei Copy und Paste),
- Ausarbeitungen sollten nach Möglichkeit dem Springer LLNCS-Stil entsprechen. Vorlagen für LaTeX und Word kann man bei Springer herunterladen.