Topics for a Bachelor or Master thesis
Compression of finite structures using automata (topic for
master thesis)
Automatic structure are relational structures that are
represented in a certain sense by finite automata. Usually,
these structures are assumed to be infinite. There is a rich
theory of automatic structures relating them to areas like
mathematical logic and computability. The concept of automatic
structures can be also used in order to represent finite
structures in a compressed way by automata. The goal of the
project is to compare automatic representations of finite structures with related
concepts like BDDs (binary decision diagrams) and to
investigate the complexity of algorithmic problems for finite
structures when the input structure is given by finite
automata.
Using SAT solver for algorithmic problems on permutation
groups (topic for master thesis)
A permutation on the set {1, 2,…, n} is just a bijective
(one-to-one) function on {1, 2,…, n}. The set of all permutations
on {1, 2,…, n} form a group, the so-called symmetric group on
{1, 2,…, n}, which is also denoted by Sym(n). The multiplication
in Sym(n) is just the composition of functions. An important
computational problem in this context is the so-called
permutation group membership problem:
- The input is: a number
n, a permutation f from Sym(n), and a finite subset S of
Sym(n).
- The question is whether f can be written as a product
(of arbitrary length) of permutations from S.
The classical Schreier-Sims algorithm solves this problem
in polynomial time. A more difficult
problem is the so-called length problem for permutation groups: The input is the same
as in the above permutation group membership problem plus an
additional number m. The question is then whether f can be
written as a product of permutations from S, where the product
must have length at most m. This problem is quite difficult to
solve: it is an NP-complete problem (Even and Goldreich 1981)
The goal of the project is to explore the use of SAT solver in
order to solve instances of the above length problem. SAT
solver a software tools that are used for checking whether a
given boolean formula is satisfiable (the so-called SAT
problem), i.e., whether one can assign truth values to the
variables in the formula such that the fomula becomes true. It
is not difficult to translate an instance of the length
problem for permutation groups into a SAT problem, which then can be
attacked with a SAT solver. There are several freely available
SAT solver that can be used for this.
