On this page we list some of the old projects and theses we have given. Most of the time, the thesis is the continuation of the project. Therefore, mostly theses are included in the list, being the result of both the project and the thesis. For example, Vanessa Lienhart solved Rush Hour during her Bachelor project, before solving it (better!) incrementally during her Bachelor thesis.

2026

Learned Clause Strengthening with Kitten, Emil Landbeck (Bachelor thesis)

Abstract:

Modern SAT solvers rely on clause minimization techniques to reduce the size of learned clauses and improve solving performance. In this thesis, we extend the SAT solver CaDiCaL with a novel minimization method that explores additional opportunities for reducing learned clauses beyond existing recursive minimization and All-UIP minimization approaches. The method colllects all clauses involved in producing a learned clause, and also additional clauses which may comprise shorter or different ways of deriving a conflict. These clauses are submitted to CaDiCaL’s internal SAT solver kitten. By assuming the negated literals of the learned clause in different orders, kitten can derive alternative or smaller unsatisfiable cores. These cores may reveal that only a subset of the original assumptions is necessary to re- establish a conflict, enabling further minimization of the learned clause. Experimental results show that this approach can reduce clause size even further and, importantly, achieve reductions in literal blocks distance (LBD) that are not possible with standard minimization or shrinking techniques.

Comment: This was an advanced Bachelor thesis from someone who already passed the SAT lecture.

2025

Limiting walk with ticks in the CaDiCaL SAT Solver, Lea Hohl (Master project)

Random walk is a common inprocessing technique in SAT solvers that aims to find the solution of SAT instances by using a random assignment as a starting model and flipping variables in broken clauses until either a solution is found or tit reaches a limit. Scheduling walk times has previously been done by counting propagations, since this is usually the hotspot of the solver. However, in the current 2.1.3 version of Cadical, x% of the solvable instances perform significantly more walk with walk using up to 77% of the total run time.

To limit walk more effectively, this project aimed to implement ticks as a counter of cache misses in the walk algorithm to approximate the run time of walk more precisely. With a more precise estimation of walk run-time, it was possible to rule out outliers and limit walk to <= 10% of the total run time of the solver.

However, implementing ticks was not trivial, since cache misses vary across the instances due to different size and complexity of the problems. This project therefore analysed the different regions of the walk algorithm in order to find its hot-spots and improve the ticksing. Furthermore, a comparison between different settings and versions was analysed.

Benchmark of RISC-V in BTOR2, Jan Krister Möller (Bachelor thesis)

Abstract:

RISC-V is an open-source instruction set architecture that is increasingly adopted in both research and industry due to its flexibility and extensibility. Formal verifi- cation, particularly bounded model checking, is essential for ensuring the correctness of such architectures in safety-critical contexts. BTOR2 has become a standard format for word-level hardware model checking.

This thesis presents tools for translating RISC-V processor states into BTOR2 models and reconstructing states from model checker witnesses. The correctness of the models is validated by comparing single-instruction execution against a reference RISC-V simulator [6]. Benchmarking is performed to evaluate the feasibility of this approach using the model checkers btormc, AVR, and Pono, with respect to instruction count, address space, and memory initialization. The results show that model checkers which perform best in general competitions do not necessarily excel for my iteration-heavy RISC-V models.

ReTI-Tools: A VSCode Extension for ReTI Assembly Programming, Malte Pullich (Bachelor thesis)

Abstract:

The Rechner Technische Informatik (ReTI), is a simplified von Neumann–type computer system used in Technical Informatics and Operating Systems lectures at the University of Freiburg to demonstrate various concepts of computer engineering. Currently, working with this architecture requires students to use disparate command- line and web-based applications for code execution, debugging, and instruction visualization. These tools vary in functionality, lack a consistent user experience, and either require students to work in an unfamiliar development environment or do not provide a complete set of features to be usable in the lecture. This increases cognitive load and subtracts from the learning effect. To overcome these limitations, this work extends a previously developed Visual Studio Code (VS Code) extension (ReTI-Tools), which provides its features for the Technical Informatics course version of ReTI, and generalizes it to provide these features for both architectures. The resulting extension integrates an emulator, a debugger, and a language server into a single, intuitive environment to streamline the learning process. In this thesis, we present the differences between the two ReTI architectures, derive requirements from shortcomings in existing tools, explain the implementation and the architectural concept behind it, and evaluate the resulting extensions feature set in relation to the existing tools. The resulting extension is open source and provides a comprehensive, uniform development environment for both courses. This improves usability and lowers entry barriers for students. In the final chapter of this thesis, we discuss remaining limitations and opportunities for future improvement, providing starting points for further development.

Comparison of Binary Adders and the Solution of MAXSAT Problems, Mathias Bischoff (Bachelor thesis)

The MaxSAT solver Pacose calls SAT solver to find the optimal solution. To do so, it needs adders to encode the additions of the costs. The aim of this work was to changing the existing adders into Wallace-Tree adders.

Incremental Solving and Generating Levels of the ’Rush Hour’ Puzzle, Vanessa Lienhart (Bachelor thesis)

Abstract:

This thesis explores efficient approaches to solving the logic puzzle ’Rush Hour’ using SAT-based methods. The goal is to find solutions in as few steps as possible through automated solving of different game levels. We compare incremental and non-incremental SAT solvers, evaluate various solver implementations, and analyse different algorithms for determining the minimum number of required moves.

The results show that incremental solving is significantly faster than non-incremental approaches. Furthermore, the choice of SAT solver has a notable impact on perfor- mance. Our evaluation of search algorithms reveals that the binary search method is considerably slower than iterative approaches. Overall, the benchmarks on human- sized puzzles are easy to solve for a SAT solver.

This work validates the approach of applying SAT solvers to planning-based logic games and lays the groundwork for future performance optimisations.

Variable Clustering in CNFs, Aria Ranjbar (Master’s thesis)

Abstract:

The Boolean satisfiability (SAT) problem is central to computer science, with uses in verification, planning, and optimization. Classifying SAT instances helps select effective solver configurations, yet prevailing methods rely mainly on raw formula statistics (e.g., variable counts, clause ratios, and literal frequencies).

This thesis investigates variable incidence graph (VIG) segmentation as a feature extrac- tion method for SAT instance classification, and explores a novel approach to generating this segmentation. The premise is that VIG structure encodes information about a for- mula’s origin and internal organization that simple metrics miss.

We present an algorithm for efficient segmentation of large VIGs, building on established graph clustering while addressing two practical challenges: memory- and time-efficient VIG construction, and avoidance of monolithic clusters. Our implementation is designed for industrial-scale instances with millions of variables and clauses, and includes safe- guards that cap segment growth during clustering.

Experiments on SAT competition benchmarks reveal recurring segmentation patterns within specific problem domains, indicating that VIG-based features capture meaning- ful structural properties. These findings suggest that variable clustering can support more informative SAT instance characterizations and, ultimately, more targeted solving strategies.

From MiniSat to MiniSatUP and its Integration with cvc5 via IPASIR-UP, Chenqi Hao (Master’s thesis)

Abstract:

SAT solvers play an important role in many formal verification and reasoning systems, usually serving as the reasoning core for more complex tools like SMT solvers. Such applications often demand a more fine-grained interaction with SAT solvers that goes beyond IPASIR, the standard but simple incremental SAT solving API. IPASIR-UP interface extends IPASIR, enabling more control from user appli- cations on the SAT solvers, but it has been so far only implemented on CaDiCaL, therefore, its practicality and capabilities are yet to be fully demonstrated. This thesis introduces MiniSatUP, an adaptation of the well-established SAT solver MiniSat to IPASIR-UP interface, supporting user-guided decision, propagation, and clause addition during solving while emphasizing minimal disruption to the original architecture of MiniSat. As the second IPASIR-UP implementation af- ter CaDiCaL, MiniSatUP demonstrates the feasibility of extending mature SAT solvers with IPASIR-UP, and its integration with SMT solver cvc5 confirms the interface’s practicality and validates IPASIR-UP as a potential standard for inte- grating SAT solvers into modern applications.

SCIP in MaxHS, Edgar Justus (Master’s thesis)

Abstract:

This thesis presents the integration of the open-source solver SCIP into MaxHS, replacing the previously used commercial solver CPLEX. MaxHS is a MaxSAT solver that combines SAT solving with Mixed Integer Programming (MIP) to find optimal solutions. While CPLEX offers high performance, its licensing restrictions limit its suitability for solver competitions and restrict open-source distribution, making it less convenient for academic research.

The integration required a detailed understanding of both MaxHS and SCIP. Before starting, I used fuzz testing with WCNFuzz to identify and fix several bugs in the MaxHS codebase. After the fixes, SCIP was added as a replacement for CPLEX with minimal changes to the existing structure.

The resulting solver was tested on standard benchmarks and compared to various CPLEX-based variants. While CPLEX still performs better in most cases, the SCIP- based version works reliably and produces correct results. An exact SCIP integration was also tested and may be valuable for instances with large clause weights. This work makes MaxHS more accessible by removing its dependency on commercial software and improving its robustness through extensive testing and debugging.

Eager Redundancy Elimination in CaDiCaL, Emil Landbeck (Bachelorprojekt)

Abstract:

Ziel des Projekts war es, die Simplification Technique Eager Redundancy Elimination (ERE) in den SAT-Solver CaDiCaL zu implementieren. Im Anschluss wurden noch einige Optimierungsversuche vorgenommen. Zur Methode: ERE soll mit Hilfe von Resolution Redundante Klauseln finden. Eine Redundante Klausel ist bereits durch andere Klauseln impliziert und kann eliminiert werden. Das Ziel ist es, die vorhandene CNF dadurch zu vereinfachen.

2024

Model-Based API Fuzzing for the Java SAT Solving Library SAT4J, Iris Parruca (Master’s thesis)

Abstract:

Building trust in SAT solvers is crucial for their effective application in complex problem-solving tasks. Model-based API fuzzing has been demonstrated to be effective in identifying issues in SAT and SMT solvers. Additionally, recent developments have introduced a proof system for incremental calls, though this technology has thus far been implemented only in C++ solvers. This thesis focuses on implementing these advancements in Sat4j, the only competitive SAT solver available in Java. Despite Sat4j’s extensive testing over the years, integrating model-based API fuzzing and incremental proof-checking proved to be a substantial enhancement. The tool revealed five previously undetected bugs ranging from “Null Pointer Exceptions” and “Assertion Errors” to wrong models returned by the solver. This work improves the robustness of Sat4j and sets a new benchmark for Java-based SAT solvers.

Hendrick Jansen (Bachelor thesis)

Abstract:

Exploiting symmetries of CNF formulas through symmetry breaking, has been shown to be an effective tool for SAT solving on specific SAT instances. However, while detecting symmetries can be used to decrease the search space for solving SAT, limitations of symmetry breaking techniques have so far prevented their widespread adoption in SAT solvers. In this thesis we propose two new methods for detecting symmetries, which restrict themselves to symmetries involving only two variables, which we call binary symmetries. We show that our methods slightly faster than state-of-the-art general symmetry detection techniques. The empirical evaluation also shows, however, that breaking these binary symmetries is unable to improve overall SAT solving performance.