Chair of Computer Architecture

University of Freiburg

Here are some ideas. Some of them have been already given, but feel free to find some inspiration. If you are interested in one project (or in something related), please write me an email (following the guidelines!).

The Chair also has an internal list. If you are interested in what we are doing, write Armin Biere an email.

I consider bachelor and master thesis/projects to be community work, so if you have a fun idea that matches my interests, feel free to drop an email.

SAT Encoding

Mastermind encoding

Or “are you the one” solver (yes, the TV reality show) for sharp-SAT to count how many solutions are still possible.


Isabelle is a proof assistant, but not all subjects require any knowledge of it.

Remark that for master projects and master thesis, it is also possible to learn Isabelle as part of the project – however learning Isabelle and Sepref for the code synthesis is too much.

Isabelle Development

While the two projects below do not require to write proofs, you will still spend a lot of time looking at them. So you will have to think about bound variables in the current context and free variables (leading to failed reconstruction).

Improved parsing for veriT proofs in Isabelle

Updating Z3 in Isabelle

Testing Infrastructure for IEE754 floats in Isabelle

IsaSAT improvement (Isabelle usage)

I have several ideas. Two of them are written below. If you have more ideas or want to do something different, feel free to write me.

Implementing ACIDS/VSIDS for IsaSAT

Incremental Reconstruction Stack


Isabelle Refinement


Isabelle LLVM



Example of done topic

Encoding the Rummikub for SAT

See the Rummikub game here. Partially given.

Reconstruction Stack