This list is not exhaustive. Please contact us for your ideas!

The index below lists some prepared topics that could serve as a starter. Every entry has an indicator for the difficulty of the project and at which level we advise you to take it on.

Different Categories for the Index Below

PR

Topic suitable for Master’s projects.

BS

Topic suitable for Bachelor’s theses.

MS

Topic suitable for Master’s theses.

Index

Analysis of Differences Between Time Tracking APIs (BS/PR/MS)

The many different ways operating systems provide to keep track of time look different enough that they could even give different results. But do they really differ, and what are their advantages and disadvantages?

Minimal Unsatisfiable Cores (BS/MS)

Even though the certification of the unsatisfiable property of an propositonal formula is a computationally hard problem, many industrial settings use this property in a variety of application fields. Hereby most state-of-the-art SAT/QBF solvers produce a unsatisfiablity proof, that guarantees the correctness of the solvers result, which can also be directly used in some practical applications.

Non-literal CDCL trails (MS)

In CDCL SAT solving, the trail contains the current partial assignment that the solver is testing; it can also be seen as a stack representing the position in the search space. However, in principle, one could imagine writing logical constraints other than literals in the trail. For example, the constraint x1 XOR x2 effectively partitions the search space in two. In this project we would like to determine how this could be implemented in a modern CDCL SAT solver.

Sampling for Constrained Procedural Generation (BS/PR/MS)

Procedurally generated content has become ubiquitous over the last decade, with applications in video game design and generative art for films. Automated reasoning tools, including SAT, QBF and SMT solvers, open new opportunities for complex procedural design. However, these tools are often designed to be deterministic, and introduce biases in the solution space. In this project, we analyze how constrained sampling techniques can help alleviate this caveat.

Slurm Cluster Load Visualizer (BS/PR/MS)

Implement a cluster workload visualizer for SLURM that helps debugging inconsistent runs by querying the slurm accounting database using some API. The View should couple SLURM accounting data with temperature, time, and other data from IPMI, so the system load is not affected by this additional information gathering.

Symbolic Encodings (PR/BS/MS)

Encode reasoning problems in SAT, QBF or SMT and solve some application problems from formal verification, planning, game playing, etc.