Proposed topics
Bachelor's thesis, diploma thesis, Master's thesis or semester project
Single Person Games in General Game Playing
A General Game Playing System is one that can accept a formal definition of a game and play the game effectively without human intervention. Unlike specialized game players, general game players do not rely on algorithms designed in advance for specific games, and they are able to play different kinds of games.
Besides two-player and multi-player games, the games that have to played successfully at the AAAI General Game Playing Competition also include single-player games. Due to algorithmic reasons, it is preferable to develop different modules handling the different kinds of games. Since single-player games described in the Game Description Language (GDL), in which the competition games are encoded, are essentially classical planning problems, it is possible to solve them using according algorithms.
The goal of this thesis is to integrate state-of-the-art algorithms and heuristics used in classical planning into a General Game Playing system currently under development. The resulting system should be evaluated using some of the benchmark games available online.
Requirements:
- Interest in Automated Planning
- Knowledge of C++ or the willingness to learn it
Further information and contact: Thomas Keller
Bachelor's thesis or Master's thesis
Playing Tetris using learning by imitation
Tetris is a famous block game to which many people are addicted. A sequence of blocks falls down unto a playing field. A player has to move the falling block in order to create horizontal lines without gaps as many as possible. Two players can compete against each other by removing N lines at a time and creating N-1 lines of attack for the opponent.
The topic for the paper is about how to make an intelligent agent play Tetris against human players. We want to imitate the strategies of different players and using these when playing against human players.
This topic can be organized as a Bachelor's thesis or a Master's thesis. The prerequisites are
- C++ programming under Linux
- Motivation to invest time and effort
Further information and contact: Dapeng Zhang
Bachelor's thesis, Master's thesis or semester project
Learning with table soccer
Table Soccer Robot KiRo can already win about 90% of games against human players. Challenging real opponents, such as the world-champion, requires extensive study of games played by humans. Therefore, a game recorder KiRe was constructed to record these games. Based on the recorded data, a series of machine learning approaches can be implemented to achieve the following tasks:
- Classifying the actions.
- Calculating the technical statistics of a game.
- Classifying the players.
- Evaluating the quality of the actions.
- Evaluating the skill of a player.
Each topic can be organized as a Bachelor's thesis, Master's thesis, or semester project. The prerequisites for these topics are
- C++ programming under Linux
- Motivation to invest time and effort
Further information and contact: Dapeng Zhang
Semester project
SAT based LTL model checking in NuSMV
Model checking is a method to automatically check whether a given system satisfies a given specification. If this is not the case, a counterexample is generated indicating how and why the specification is violated. NuSMV is a symbolic model checking tool for specifications in the logics CTL and LTL. It implements SAT and BDD based algorithms for LTL model checking. Experiments show that the SAT based algorithm is often less efficient than the BDD based one.
The goal of this work is to implement a given modification of the SAT based algorithm in NuSMV (parallel instead of only sequential transitions), possibly gaining an increase in efficiency. The work should be concluded by an empirical evaluation of the implementation in comparison to other approaches.
Prerequisites:
- Good skills in C programming
- Helpful: basic knowledge about planning as satisfiability and about temporal (modal) logics
Further information and contact: Robert Mattmüller
Bachelor's thesis
Transformation of propositional formulae
into linear pseudo-Boolean constraints
A linear pseudo-Boolean constraint (LPB) is an expression of the form a_1 l_1+...+a_m l_m ≥ d, where each l_i is a literal (it assumes the value 1 or 0 depending on whether a propositional variable x_i is true or false) and the a_1,...,a_m,d are natural numbers. The formalism can be viewed as a generalisation of a propositional clause. LPBs can be used to represent Boolean functions more compactly than the well-known conjunctive or disjunctive normal forms. E.g., the LPB 2x_1+¯x_2+x_3+x_4≥2 corresponds to the DNF x_1\/(¬ x_2/\ x_3)\/(¬ x_2/\ x_4)\/(x_3/\ x_4). Therefore, in the literature one finds several approaches of generalising techniques from SAT solving to LPBs. All these approahes assume that the LPBs arise naturally from some problem domain.
However, one might ask if it is interesting to transform arbitrary propositional formulae into a set of LPBs, so that one can then benefit from the compact representation during the SAT solving. There is an algorithm solving this problem partially: given a propositional formula representable as a single LPB, the algorithm finds this LPB.
The goal of the project is to implement this algorithm and to conduct some experiments to judge how difficult the transformation is in practice.
Further information and contact: Jan-Georg Smaus
Ongoing topics
Semester project
Preferences in syllogistic reasoning
Assigned to: Oliver Klug (since June 2007)
Syllogisms are a kind of logical argument in which a conclusion is inferred from two premises of a certain form (quantified expressions). The syllogism are at the core of deductive reasoning, where facts are determined by combining existing statements, in contrast to inductive reasoning where facts are determined by repeated observations. Human reasoning differs significantly from formal approaches, w.r.t errors.
The objective of this work is to first analyze a result by Chater and Oaksford by means of Euler circles, to develop a computational model, and to explain the preference "rules" by a cognitive complexity measure.
