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

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

• Prerequisit: no knowledge of Isabelle nor SMT solvers nor Standard ML is required, but knowledge of a functional language and some understanding of proofs is required.
• Theme: The proof assistant Isabelle relies on external tools to prove goals. However, it does not trust those tools and checks the proof that the external tools generate. For this project, we are interesting in the SMT solver veriT. Currently the whole proof returned by veriT is entirely parsed before being checked. This work intends to parse the proof steps before we need them in order to improve performance.
• Outcome: The resulting code should be added to the Isabelle repository.

Updating Z3 in Isabelle

• Prerequisit: no knowledge of Isabelle nor SMT solvers nor Standard ML is required, but knowledge of a functional language and some understanding of proofs is required.
• Theme: The proof assistant Isabelle relies on external tools to prove goals. However, it does not trust those tools and checks the proof that the external tools generate. For this project, we are interesting in the SMT solver Z3. Isabelle relies on a very old version of Z3 and it is known that the latest version does not work with Isabelle due to bugs in the proof output Z3. The aim of this project is to find if we can update Z3 to a newer version. This will require both to fix the proof reconstruction (because some new features were added to the proof output) and check if the generated proofs are correct.
• Outcome: The resulting code should be added to the Isabelle repository.

Testing Infrastructure for IEE754 floats in Isabelle

• Prerequisit: some knowledge of Isabelle is required, but a strong knowledge is definitively a plus (in order to also fix discovered issues)
• Theme: The proof assistant Isabelle does not yet have bindings to generate floating points, but Peter Lammich is working on it. However, it is not clear if the generated code has the same behaviour. The aim of this project is to create a test-suite to check that the behaviour is the same (especially for edge cases involving NaN, infinity, …).
• Warning: this project would be partly co-advised with Peter Lammich. It is also at the edge between developing Isabelle and using 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

• Prerequisit: strong knowledge of Isabelle is required (see my lecture for SS-22). Knowledge of the Refinement Framework is a plus (but it is not too hard to learn). No knowledge of SAT solving is needed
• Theme: IsaSAT currently uses only one decision heuristic, namely variable move to front. The aim for this project is to add a second one targeting satisfiable instances.
• Outcome: The resulting code should be added to IsaSAT.
• Warning: this is a challenging project because it is using Isabelle and the Refinement Framework, but it does not require advanced concepts.

Incremental Reconstruction Stack

• Prerequisit: strong knowledge of Isabelle is required (see my lecture for SS-22). No knowledge of SAT solving is needed.
• Theme: SAT solver simplify the formula they are currently solving in ways that are not equisatsifiable, i.e., a model of the resulting formula must be fixed to be a model of the original formula. The aim of this project is to formalize this process for an incremental SAT solver. This builds on the incremental reconstruction stack for non-incremental stacks
• Outcome: The resulting code should be added to the IsaFoL repository.
• Warning: This project is too large for a bachelor project/thesis.

Unsorted

• OTFS in the CDCL rewrite system
• Model reconstruction for autarkies
• Autarky detection

Isabelle Refinement

Unsorted

• Memory module for sharing of lists for Pastèque

Isabelle LLVM

Unsorted

• Mini-GMP for Isabelle LLVM binding.

Teaching Related

Unsorted

• Visualisation for RISC-V of the pipeline and the dependencies (computer architecture based)

Example of done topic

Encoding the Rummikub for SAT

See the Rummikub game here. Partially given.

Reconstruction Stack

• Prerequisit: strong knowledge of Isabelle is required (see my lecture for SS-22). No knowledge of SAT solving is needed.
• Theme: SAT solver simplify the formula they are currently solving in ways that are not equisatsifiable, i.e., a model of the resulting formula must be fixed to be a model of the original formula. The aim of this project is to formalize this process.
• Outcome: The resulting code should be added to the IsaFoL repository.
• Warning: This project is most likely too large for a bachelor project/thesis.