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

QCIR Syntax Checker (PR)

This project is for developing a tool that checks non-prenex non-CNF Quantified Boolean formulas. The tool returns if a given formula is encoded as specified in the documentation and if the formula is in cleansed form.

Fuzzer (and Delta-Debugger) for Automated Planning (PR)

Automated planning is the problem of finding a sequence of actions (a plan) to achieve a goal. Fuzzing describes the technique of randomly generating inputs in the hope of triggering a bug in an algorithm or its implementation. Delta Debugging allows to shrink a problematic input (in most cases to just a few lines) until it can be easily understood. Your task would be to write a PDDL fuzzer and use it to evaluate a number of automated planners. If successful, you will be able to generate a handful of small PDDL files that will break most automated planners.

Automated First-Order Theorem Proving (BS/PR/MS)

Automated theorem proving is a subfield of automated reasoning and mathematical logic that deals with proving mathematical theorems by computer programs. In this project, we want to explore the capabilities (and boundaries) of automated theorem provers for first-order logic. In particular, we will try to use first-order theorem provers to prove statements about matrices and other mathematical objects. If we are lucky, we can also automatically prove the exercises from your exercise sheets.

Interactive Formula Tree for the LogBook

This project was created with the goal to develope an interactive tool, where students can practice to create the formula tree of a given propositional formula. The tool should then verify, if the created tree is correct and should be used in the LogBook for the Logic lecture.

Towards Fully Interchangeable SAT Solver Packages using IPASIR2 and Guix (BS/PR/MS)

Each SAT solver traditionally has its own interface. As different solvers are optimized for different things, it is advisable to use multiple SAT solvers in a solving pipeline. The different interfaces hinder adoption, because using another solver means one has to integrate a new interface each time. This issue is acknowledged by the IPASIR standard, which, more recently, has seen development in a new IPASIR2 version. This now defers the work to linking and to a good build system. Guix, the transactional package manager, already provides a system to swap out dependencies. If one can merge these two approaches, swapping SAT solvers or adding more is a matter of changing a package’s recipe in Guix, changing SAT solving for the better!

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.

Personal scheduling application (PR/MS)

Current personal schedulers overly rely on the user knowing beforehand when they want to schedule tasks. The goal of this project is to (eventually) develop a web application for personal task scheduling based on user constraints, so that the scheduler actually makes the decisions instead of simply acting as a reminder. Within this project, there are many tasks that must be solved, including developing a scheduling problem specification language, a low-level representation for scheduling problems, a schedule solver and optimizer, a web-based graphical user interface for the specification language, an LLM-based problem specification generator, and benchmarks for the solver and generator.

SAI Packages (PR,BS)

During research, there is a bunch of software that we repeatedly use and distribute between each other. While sending around links to GitLab repositories is fine for internal software that is actively being worked on, it is less ideal for other groups or individuals using software from the SAI, or for the SAI to use software developed by others. We want to create an APT package repository to make the task of installing software no more than the classic sudo apt install <something>.

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.

Game Encodings (PR)

Harary’s generalized tic-tac-toe is an achievement game, where two players place stones on a grid board, trying to complete a particular polyomino. In this project we try to find a proper encoding of these generalizations in SMT (Satisfiablity modulo theory), in order to count the possible moves in a given state of the game. Depending on the agreed scope of the project an additional implementation of one specific configuration using machine learning might also lead to interesting case studies.

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.

Cube Minimization via Ternary Simulation (PR)

Hardware designs (as in the CPU in your PC) can be described as boolean circuits. These circuits consist of and-gates. The value of a gate depends on its two inputs that may or may not be negated and are themselves gates. You will try to implement something that as efficiently as possible answers the following question:

Given a fixed assignment (true or false) to some of the gates (called a cube) and a gate we will call the output, what part of the cube is necessary to ensure that the value of the output stays the same.

Interactive Feature Model Configurator using Exact Cover Encoding (MS)

Feature models describe product variability based on features and restrictions of combinations thereof. Interactive configurators enable users to select or exclude such features to generate products.

We want to implement an interactive configurator based on encoding feature models as Exact Cover Problems. The aim of the project is to find out whether this alternative paradigm can compete with the state-of-the-art.