[  sat | bdds | qbf | qbf ]

Projects

This page lists proposals for practical projects and thesis work in both the computational engineering specialization of the computer science master as well as the master in artificial intelligence.

Most of them have a more theoretical background but also more often than not require good low-level implementation skills.

If you are interested to work with us, please contact any member of FMV.

SAT

Satisfiability checking (SAT) is a fast moving technology and is used in many applications, from hardware verification to device driver verification. We are particularly interested in combining structural and high-level reasoning with SAT solving, such as parity reasoning for formulas with many XOR constraints as well as algebraic techniques using techniques from computer algebra. Related to this are different forms of parallel SAT solving (GPU, threaded, cluster, cloud).

BDDs

Even though binary decision diagrams played an important role in the late 20ties century, they became out-fashion due to the SAT revolution we witnessed in the last 20 years. There are however certain problems for which BDD based techniques seem to be a better fit, and thus we want to revisits BDDs and related formalism, such as ZDDs both for verification as well as optimization.

QBF

Decision procedures for Quantified Boolean Formulas (QBF) can be used to handle various verification problems. Recently these procedures became much more powerful, though benchmarking in the real world and adapting QBF solvers to real problem domains has not been investigated much. In this context it is also possible to work on ideas to improve QBF solver technology.

Educational Games