Symbolic AI Thesis Topics and Ideas

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.

More Details

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.

More Details

Gaussian elimination for transforming a matrix into (reduced) row echelon form is undoubtely one of the most central algorithms in mathematics, computer science, and other disciplines. Thus, a lot of effort has been put into making this algorithm as efficient as possible. In this project, we want to investigate whether we can improve upon the classical Gaussian elimination by exploiting a particular structure of certain matrices.

More Details

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!

More Details

The classical algorithm for multiplying two 2 x 2 matrices requires 8 multiplications and for a long time people believed that this was optimal. However, in 1969 Volker Strassen showed that it can also be done with just 7 multiplications, using, what is now known as Strassen’s algorithm. In this project, we want to investigate whether we can find better algorithms also for multiplying 3x3 matrices (or matrices of even larger size) using symbolic AI. The problem of finding a better algorithm for matrix multiplication can be encoded as a SAT- or QBF-formula and any model of that formula yields a matrix multiplication algorithm. We can try different encodings and compare them.

More Details

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.

More Details

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.

More Details

One way to build quantum computers is via so-called "trapped ions". Within such "Trapped-Ion Quantum Computers", ions can be moved through different dedicated zones (e.g., a memory zone for storage and a processing zone for the actual computation). However, this movement incurs a cost in terms of required time steps, which should be minimized. People have used SAT-solving techniques in order to determine the minimal number of time steps needed for these movements, see the reference below. However, it seems that the underlying problem could be better encoded with a QBF-formula.

In this project, we want to investigate whether this is indeed the case, try different QBF-encodings of the underlying quantum problem, and see if we can improve upon the state-of-the-art SAT-encoding.

More Details

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>.

More Details

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.

More Details

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.

More Details

Automated formal verification of arithmetic circuits, most prominently multiplier circuits, poses an important problem, which in practice still requires substantial manual effort. Recently, an idea emerged to identify sub-circuits of a larger circuit, which can be simplified easily and which then in turn allow to simplify the overall computation. Thus far, man-made heuristics are used to detect such sub-circuits. In this project, we want to investigate whether a neural network can learn better heuristics.

More Details

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

More Details

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.

More Details

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.

More Details