Thesis and Project Topics

Here is an ongoing chart for the different topics. It is not a flow diagram that will tell you exactly which topic to take, but it gives some ideas of the general topic our group has. If you are really interested in a topic, we might have themes that are available that do not require the full lecture.

We are always happy to hear about other topics (related to our interests however). Although on bachelor level we are more opened to cool-sounding ideas.

Some of our subjects can fit into various topics depending on the approach (for example, hardware verification can be done from the Isabelle side or from the tools side or like a puzzle to verify some properties or as multipliers).

There are fewer Master thesis topics in the graph as we usually taylor them to the student’s interest and it is more work to propose entire topics (and some ideas are research ideas that we do not want to make public).

WARNING: the graph below is not complete nor up to date w.r.t. the other chairs. Many chairs are missing like the one of Prof. Schindelhauer. Do not forget to check other chairs when considering a topic!

WARNING2: this graph is regularly updated (see the start point for the current version)

WARNING3: This graph is zoomable now.

The caption and the co-supervisor is given by the stroke around the box:

flowchart TD classDef mathias stroke:#0f0 classDef tobiasF stroke:#0ff classDef florian stroke:#ff0 classDef andre stroke:#0ff classDef all stroke:#fff Supervision["Supervision
(Armin Biere always involved)"]; Mathias["Mathias Fleury"]; TobiasF["Tobias Faller
partially independent
of the chair"]; Florian["Florian Pollitt"] Andre["André Schidler"] All["Anyone in the group
depending on the exact topic"]; Supervision --> Florian; Supervision --> Mathias; Supervision --> TobiasF; Supervision --> Andre; Supervision --> All; class Mathias mathias; class Bernhard bernhard; class TobiasF tobiasF; class Florian florian; class Andre andre; class All all; class Bernhard_Florian bernhard_florian; class Bernhard_Mathias bernhard_mathias;

Process to register a project and define the goals

General flow to get a project:

You send an email to Armin and get a meeting (mostly online nowadays). In this email you should include: (i) what you are currently studying (ESE / CS / …); (ii) which lectures you heard from us and which you are currently hearing; (iii) what you are interested in (bachelor/master and project/thesis); (iv) your programming skills; and (v) if you are an ESE student, make sure to add if you did you Bachelor in Freiburg (and include relevant information like whether you know verilog)
You look at the chart above and find 2-3 topics that interest you most.
You meet with us now and tell us which topics you are the most interested in. This is also the right moment to tell us if you have favorite topics. We discuss several subjects for each topic (using a list that we do not publish). If you are interested in Scale4Edge, then you need an meeting organized by Tobias Faller.
We assign you a group member (the co-supervisor, not Armin) and a deadline (usually 2 weeks)
Before the deadline you tell the co-supervisor which topic you picked or if you gave up
You register with Frau Moses (see full description here) by putting the group member in CC with a deadline (end of semester) / You fill the form and we meet
We can meet for the first time: Discuss potential milestones (usually 3 + a presentation/writing of the thesis; the first milestone decides if you pass or not)
Second meeting: you write the milestones properly down by email and you start

Some more detailed on topics

We below give some more details in order to make it easier for you to imagine what the topic can look like. This is not a real subject, but should give ideas what to expect.

Representing a puzzle and solving it

The objective of these projects is to encode a game/puzzle and solve it.

Good options for this include games:

with complete information (you know the position of every piece)
with a reasonably small game state (no, you will not solve Go or chess with a SAT solver)
that are not part of Yurichev’s book or have not been solved in the exact same way.

A great example would be Sudoku, although it has already been solved countless times with a SAT solver and it is a bit too easy (just search for it on the internet).

Your task involves:

Selecting a game, preferably one you enjoy.
Encoding the game.
Translating the solution back into a format that can be checked. For instance, you may want to represent a solution and verify it.
Depending on the project, determine some numbers: if you’re working on Mastermind, for example, you might be interested in the average number of solving steps (to compare it with other approaches); how many different solutions exist under the given constraints?

Thilo Langensteiner worked on Ubongo 3D. He solved it using his own encoding and visualized the game to check the solutions. Despite the challenge, he still enjoyed the game at the end of the project.

MaxSAT solving

Many topics are possible, but here is a general description of one that was already given.

The goal is to modify part of the translation into an SAT Solver (like the adder used to represent weights - SAT solvers do not understand numbers, so you need to encode the question).

While there are no prerequisites, you should enjoy coding and debugging in C++. Additionally, as you will also spend time on propositional logic, you should also find it enjoyable.

Teaching tools

We expect you to implement a tool in JavaScript as demonstration tool for our lectures. JavaScript makes it possible for us to host the tool on our webpage, ensure that future students will also be able to use it. See the list.