Offene Themen
Bachelorarbeit, Diplomarbeit, Masterarbeit oder Studienarbeit
Ein-Personen-Spiele im General-Game-Playing
Ein General-Game-Playing-System ist in der Lage, mit einer formalen Definition der Regeln eines Spiels als Eingabe dieses effektiv ohne menschlichen Eingriff zu spielen. Im Unterschied zu spezialisierten Game-Playing-Systemen beruhen General-Game-Playing-Systeme nicht auf Algorithmen, die speziell auf bestimmte Spiele zugeschnitten sind, sondern sind in der Lage, unterschiedliche Spiele zu spielen.
Die Spiele, die beim AAAI-General-Game-Playing-Wettbewerb erfolgreich gespielt werden müssen, umfassen neben Zwei- und Mehrpersonenspielen auch Ein-Personenspiele. Aus algorithmischen Gründen ist es bei der Entwicklung eines General-Game-Playing-Systems sinnvoll, Ein- und Mehrpersonenspiele getrennt zu behandeln. Da Ein-Personenspiele im Sinne der Spielbeschreibungssprache GDL, in der die Wettbewerbsspiele kodiert sind, im Wesentlichen klassische Handlungsplanungsprobleme sind, kann man sie auch mit entsprechenden Algorithmen lösen.
Ziel dieser Arbeit ist die Integration erprobter Algorithmen und Heuristiken aus der klassischen Handlungsplanung in ein in der Entwicklung befindliches General-Game-Playing-System. Das resultierende System sollte anhand von online zugänglichen Benchmark-Spielen evaluiert werden.
Voraussetzungen:
- Interesse an Handlungsplanung
- Kenntnisse in C++ oder die Bereitschaft, sich diese zu erarbeiten
Weitere Informationen und Kontakt: Thomas Keller
Bachelorarbeit oder Masterarbeit
Lernen durch Imitation am Beispiel von Tetris
Tetris ist ein berühmtes Blockspiel, nach dem viele Menschen verrückt sind. Eine Sequenz von Blöcken fällt dabei runter auf ein Spielfeld. Ein Spieler muss die fallenden Blöcke so bewegen, dass es so viele horizontale Linien ohne Lücken als möglich entstehen. Zwei Spieler können dabei gegen einander antreten in dem einer N Linien auf einmal löscht und dabei für den Gegner eine N-1 Angriffslinie entsteht.
Das Thema der Arbeit ist, wie man einen intelligenten Agenten dazu bringt, gegen menschliche Gegner Tetris zu spielen. Wir wollen dabei Strategien von verschiedenen Spielern imitieren und diese dann bei menschlichen Gegner anwenden.
Das Thema kann als Bachelor oder Master Arbeit angelegt werden. Die Voraussetzungen sind
- Kenntnisse in C++-Programmierung mit Linux
- Motivation, die nötige Zeit und Arbeit zu investieren
Weitere Informationen und Kontakt: Dapeng Zhang
Bachelorarbeit, Masterarbeit oder Studienarbeit
Lernen mit Tischfußball
Der Tischfußball-Roboter KiRo kann bereits 90% der Spiele gegen menschliche Gegner gewinnen. Um reale Gegner, wie z.B. den Weltmeister, herauszufordern bedarf es eines extensiven Studiums von Spielen mit realen Spielern. Für diese Zwecke wurde der Rekorder KiRe entwickelt, der Tischfußballspiele von realen Spielern aufzeichnet. Mit Hilfe der aufgezeichneten Daten kann eine Serie von Methoden zum maschinellen Lernen implementiert werden, um folgende Aufgaben auszuführen:
- Klassifizierung der Aktionen
- Berechnung der technischen Statistik eines Spiels
- Klassifizierung der Spieler
- Bewertung der Qualität der Aktionen
- Bewertung des Könnens eines Spielers
Jedes Thema kann als Bachelorarbeit, Masterarbeit oder Semesterprojekt aufgebaut werden. Die Voraussetzungen sind:
- Kenntnisse in C++-Programmierung mit Linux
- Motivation, die nötige Zeit und Arbeit zu investieren
Weitere Informationen und Kontakt: Dapeng Zhang
Studienarbeit
SAT-basierte LTL-Modellprüfung in NuSMV
Bei der Modellprüfung wird untersucht, ob ein gegebenes System eine gegebene Spezifikation erfüllt. Ist dies nicht der Fall, wird ein Gegenbeispiel erzeugt, das zeigt, warum die Spezifikation verletzt ist. NuSMV ist ein symbolischer Modellprüfer für Spezifikationen in den Logiken CTL und LTL. Es enthält SAT- und BDD-basierte Algorithmen zur LTL-Modellprüfung, wobei der SAT-basierte Algorithmus in vielen Fällen ineffizienter als der BDD-basierte ist.
Ziel dieser Arbeit ist die Implementierung einer vorgegebenen Modifikation des SAT-basierten Algorithmus in NuSMV (parallele statt nur sequentieller Transitionen), in der Hoffnung, dadurch eine merkliche Effizienzsteigerung zu erzielen. Abschließend soll die Implementierung anhand vorhandener Benchmarks im Vergleich zu anderen Verfahren evaluiert werden.
Voraussetzungen:
- Gute C-Programmierkenntnisse
- Hilfreich: Grundlagen über Planen durch Erfüllbarkeitstests und über Modal- bzw. Temporallogiken
Weitere Informationen und Kontakt: Robert Mattmüller
Bachelorarbeit
Transformation von aussagenlogischen Formeln
in pseudo-Boolesche Constraints
Ein linearer pseudo-Boolescher Constraint (LPB) ist ein Ausdruck der Form a_1 l_1+...+a_m l_m ≥ d. Hierbei ist jedes l_i ein Literal der Form x_i or ¯x_i=1-x_i, d.h., x_i wird 0 wenn x_i falsch ist und 1 wenn x_i wahr ist, und umgekehrt für ¯x_i. Des weiteren sind a_1,...,a_m,d natürliche Zahlen. LPBs sind eine Verallgemeinerung von aussagenlogischen Klauseln. Boolesche Funktionen können mittels LPBs oft kompakter dargestellt werden als mittels konjunktiver oder disjunktiver Normalformen. Z.B. entspricht die LPB 2x_1+¯x_2+x_3+x_4≥2 der DNF x_1\/(¬ x_2/\ x_3)\/(¬ x_2/\ x_4)\/(x_3/\ x_4). Daher gibt es in der Literatur mehrere Ansätze, die Techniken aus dem SAT Solving (aussagenlogische Erfüllbarkeit) auf LPBs zu verallgemeinern. In diesen Arbeiten wird immer davon ausgegangen, dass sich die LPBs aus der Kodierung innerhalb der Problemdomäne natürlich ergeben.
Man kann allerding fragen: könnte es nicht auch interessant sein, beliebige aussagenlogische Formeln in eine äquivalente LPB-Menge zu transformieren, um dann beim Entscheiden der Erfüllbarkeit von der kompakteren Darstellung zu profitieren? Es gibt einen Algorithmus, der dieses Problem teilweise löst: gegeben eine aussagenlogische Formel, die sich als eine einzige LPB darstellen lässt, findet der Algorithmus diese LPB.
Gegenstand der Bachelor-Arbeit ist es, diesen Algorithmus zu implementieren, und einige Experimente zu machen, um abzuschätzen, wie aufwändig die Transformation in der Praxis ist.
Weitere Informationen und Kontakt: Jan-Georg Smaus
Laufende Arbeiten
Studienarbeit
Präferenzen im syllogistischen Schließen
Vergeben an: Oliver Klug (seit Juni 2007)
Syllogismen sind logische Argumente, die immer nach dem gleichen Muster aufgebaut sind: Eine Konklusion wird aus jeweils zwei Prämissen (quantifizierte Ausdrücke) inferiert. Dabei ist das syllogistische Schließen prinzipiell deduktiv. Interessanterweise unterscheiden sich kognitive Resultate wesentlich von Vorhersagen formaler Modelle.
Ziel der Arbeit ist es, die kognitiven Resultate von Chaters und Oaksford einzuordnen, diese mittels Eulerkreisen zu modellieren und zu implementieren und schließlich die Resultate mittels eines kognitiven Komplexitätsmaßes zu erklären.
