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 below, 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.
This is a small list, since (status 2026-SS) we are doing 10+ projects and theses since 2024, and 20+ since 2025.
2026
Pastèque, the verified PAC Checker in Isabelle-LLVM with Arbitrarily Large Integers, Milan Müller (Bachelorthesis)
Abstract:
Proof certificates can increase trust in an automated reasoning tool by providing justification of its deductions that can be validated by a third-party checker. The practical algebraic calculus (PAC) defines such proof certificates for verification of digital circuits, in particular multipliers, based on algebraic reasoning. I migrate the formally verified PAC checker Pastèque from its original Standard ML backend to a newer LLVM backend, using the Isabelle-LLVM framework for implementing and formally verifying imperative programs with manual memory management in the theorem prover Isabelle. To enable this migration, I extend a native multiple precision arithmetic library for Isabelle/LLVM for use in Pastèque and implement fundamental low-level datatypes, including hashmaps and nestable linked lists, for Isabelle-LLVM. I evaluate the performance of the LLVM migration, comparing it to the original Standard ML implementation and the Pacheck PAC checker written in C++, observing a performance improvement for smaller instances and a performance decline for large 512-bit multipliers, compared to the Standard ML backend.
Formalizing and Verifying Mastermind Strategies in Lean, Nils Steuernagel (Bachelorthesis)
Abstract:
Mastermind is a code breaking board game in which a player must find a secret code. The player guesses based on feedback from previous guesses. This thesis formalizes Mastermind in Lean 4 and proves that three different strategies find any secret. The formalization includes codes, feedback, turns, histories, and game execution.
The thesis proves that exhaustive search and guessing without repetition return the secret for Mastermind games of any numbers of positions and colors. For a game size of four positions and six colors, this thesis generates a decision tree based on Knuth’s strategy. It then verifies that all 1,296 possible secrets can be found within five guesses using only this tree.
Autarky Identification during Local Search in CaDiCaL, Sebastian Köbke (Bachelorthesis)
Abstract:
Modern CDCL solvers, such as CaDiCaL, run a local search during rephasing to improve their saved phases. Besides local search, rephasing can also randomize or invert the saved phases, which can discard assignments that already satisfy parts of the formula. This is particularly unfortunate for partial assignments that satisfy every clause they touch, so-called autarkies. Eliminating an autarky does not change the satisfiability of the formula but reduces its size, so autarkies should be preserved. In this thesis, we implement the local search solver PALSAT in CaDiCaL’s rephasing.
The structure of PALSAT is well suited to identify and eliminate autarkies. We present an autarky peeling algorithm that uses occurrence lists and a satisfied counter per clause and runs in linear time in the size of the formula. Marking identified autarkies allows peeling several times during one run, and by composition all collected literals form a single autarky. To identify larger autarkies, we modify PALSAT’s stagnation handling, increase its tick limit and add pure literals and pseudo pure literal elimination (PPLE). On the 400 instances of the main track of the SAT Competition 2025, these optimizations raise the number of autarky literals identified by PALSAT to 84 % of those found by CaDiCaL’s own autarky identification. We further show that a local search which only flips literals of broken clauses cannot destroy an autarky contained in its assignment. According to our experiments, the influence of local search on autarky identification is limited to a few instances. Nevertheless, the identification and marking of autarkies presented in this thesis can be generalized to CDCL solvers and to local search SAT solvers in order to protect autarkies against rephasing and restarts.
Integrating Graph-Based Reasoning into Max-SAT Solving: A CaDiCaL-Based Approach to the Minimum Feedback Vertex Set Problem, Lukas Dekorsy (Bachelorthesis)
Abstract:
The Minimum Feedback Vertex Set (MFVS) problem in directed graphs is a fundamental NP-hard graph optimization problem with applications in areas such as VLSI circuit design or the control of complex networks. In the optimization version considered here, finding an arbitrary feedback vertex set is insufficient, since the objective is to minimize the number of removed vertices. Its computational complexity makes the development of efficient exact algorithms a challenging task.
The 2022 PACE Challenge focused on the Directed Feedback Vertex Set problem and included several exact and heuristic approaches. The winning solver of the exact track, DAGer, combined the MaxSAT framework EvalMaxSAT with the SAT solver Glucose and a dedicated mechanism for dynamically detecting cycles during the search.
Recent developments in SAT solving have introduced the IPASIR-UP interface, which enables SAT solvers to support user-defined propagators in a standardized way. This interface allows domain-specific reasoning to be integrated directly into the SAT solver without requiring changes to the solver’s core implementation.
The primary objective of this thesis is to investigate whether the graph-based reasoning mechanism of DAGer can be implemented using the standardized IPASIR-UP interface. The original solver combines SAT solving with dynamic cycle detection to solve instances of the Minimum Feedback Vertex Set problem. This work reimplements the graph reasoning component as an IPASIR-UP user propagator and integrates it into the EvalMaxSAT framework using CaDiCaL as the underlying SAT solver.
SAT-Kodierung des längsten Pfades in Graphen, Dennis Hämmerle (Bachelorthesis)
Abstract:
Die Berechnung des längsten einfachen Pfades in einem Graphen ist ein NP-schweres Problem, das sich aufgrund seiner kombinatorischen Komplexität für die Lösung mit SAT-Solvern eignet. In dieser Arbeit wird untersucht, wie das Problem als Erfüllbarkeitsproblem der Aussagenlogik modelliert und effizient gelöst werden kann. Hierzu werden zwei unterschiedliche Kodierungen entwickelt, mit denen sowohl die Existenz eines Pfades mit vorgegebener Länge als auch eines Pfades ab einer Mindestlänge modelliert werden kann. Zur Bestimmung der maximalen Pfadlänge werden anschließend verschiedene Suchstrategien untersucht. Darüber hinaus werden Verfahren zur Vorver arbeitung von Graphen eingesetzt, um die strukturellen Eigenschaften der Graphen zu nutzen und die nachfolgende Berechnung zu vereinfachen. Die entwickelten Ansätze werden anhand verschiedener Instanzklassen für gerichtete und ungerichtete Graphen experimentell untersucht. Die Ergebnisse veranschaulichen, dass die Leistungsfähigkeit von der Kombination aus Kodierung, Suchstrategie und Graph Preprocessing abhängt. Die geeignete Kombination hängt dabei von der Struktur der Graphinstanz ab. Insge samt zeigen die Untersuchungen, dass SAT-Solver eine geeignete und leistungsfähige Methode zur Berechnung des längsten einfachen Pfades darstellen.
Model Enumeration using IPASIR-UP without Blocking Clauses, Timple Hörig (Masterthesis)
Abstract:
The Boolean satisfiability problem (SAT) is a fundamental NP-complete problem with numerous applications in verification and reasoning. While modern Conflict-Driven Clause Learning (CDCL) based SAT solvers efficiently compute single satisfying assignments, many applications require enumerating all solutions (AllSAT). This is challenging due to their potentially exponential number and the inefficiency of standard techniques such as blocking clauses.
Implementing a model enumerator through the IPASIR-UP interface allows to leverage highly optimized SAT solvers such as CaDiCaL while maintaining a clear separation between the solver and the enumeration logic. This modular approach ensures that the enumerator remains independent of a specific solver implementation, requiring only com pliance with the interface. As a result, improvements in underlying solvers can be directly utilized without modifying the enumerator, enabling both flexibility and long-term maintainability. This thesis presents CaDiCAll: a model enumerator without blocking clauses using the IPASIR-UP interface.
Improving babywalk and babysat with Yal-lin, Johannes Gröber, Rico Andris, Jakob Peterse (Lab)
Abstract:
The latest improvement of local search in SAT solving is Yal-lin / TaSSat. We reimplemented the algorithm in babywalk, simplifying the implementation along the way.
We also included the local search and put it into babysat, the solver used for the SAT solving lecture.
Note: CaDiCaL now has both Yal-lin and the successor paper, TaSSAT, based on the code from Lab. The implementation was described in a Pragmatics of SAT paper 2026 paper.
Predicting Kissat Performance with Satzilla, Paulo Rosas (Bachelorthesis)
This thesis investigates the use of SATzilla, a machine learning-based algorithm portfolio system, to predict the performance of various configurations of the Kissat SAT solver. The research focuses on enhancing solver selection by extracting structural features from Boolean formulas in Conjunctive Normal Form (CNF) and employing a Random Forest classifier to identify the most efficient solver for a given instance.
A central contribution of the work is the analysis of how different levels of preprocessing—specifically “Pre10k” (running Kissat with a limit of 10,000 conflicts) and “Pre100k” (running Kissat with a limit of 100,000 conflicts)—affect SATzilla’s predictions and the resulting solver performance. The author analyzes the importance of various feature categories, concluding that the Clause Graph (connection structure of clauses) is the most significant predictor, followed by preprocessing results, polarity, and clause length distribution.
The experimental results indicate that while preprocessing can lead to significant improvements in specific cases, it can also cause extreme performance degradation in others, leading to a negative average improvement across the tested benchmarks. The thesis concludes that while aggressive preprocessing (Pre100k) slightly increases the success rate of faster solving compared to Pre10k, it does not provide a significant overall advantage and may introduce substantial risks of performance volatility.
Comment: AI generated abstract by Gemma 4 31B (“UFR: Standard Chat”) using https://openwebui.uni-freiburg.de/, with minor fixes
Analyzing Mastermind Solving Policies with #SAT, Manuel Di Biase (Bachelorthesis)
Abstract:
Mastermind is a code-breaking game in which a player must identify a hidden code through repeated guesses and feedback. Selecting strong guesses is computationally challenging because each move must reason about many candidate secrets and possible feedback outcomes.
This thesis studies Mastermind through propositional reasoning and model counting. The current game state is encoded as a propositional formula whose satisfying assignments are exactly the secret codes consistent with the observed history. Model counting is used to determine how many candidate secrets remain under actual or hypothetical feedback.
The thesis compares an iterative #SAT-based solver, a knowledge-compilation-based approach using a reusable d-DNNF representation, and Knuth’s minimax algorithm as a baseline. Its main contribution is the adaptation of d-DNNF-based query reuse to Mastermind, together with an empirical comparison of enumerative, #SAT-based, and compiled reasoning approaches.
The experimental results show that Knuth’s algorithm performs best overall across the tested configurations, while the reusable d-DNNF-based approach is advantageous only in restricted settings, most notably for 8-peg instances with a small color set, where repeated queries can amortize the compilation cost.
Comment: The encoding to #SAT was part of the bachelorproject, which was extended to use more tools.
PyZort - Optimiertes Benchmark Scheduling mit MaxSAT, Jann Ehses (Bachelor thesis)
Abstract:
PyZort is a program that was developed as part of this thesis for the Chair of Computer Architecture in Freiburg. Until now, the chair has been transferring complex computing operations to the high-performance computer “Helix” located in Heidelberg. These so-called benchmarks are resource-intensive and keep the computer busy for several hours. Based on the program Zort[1] developed by Ar- min Biere, PyZort uses maximum satisfiability encoding to compute an optimized execution order. This method reduces the total execution time of benchmarks on the high-performance computer, thereby reducing power consumption and runtime.
Comment: This is an extension of the bachelor project, including a very time-consuming bug fix to get the encoding to work.
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
LRU Cache Visualization, Mirai Matsuura (Masterproject Ed. thesis )
https://cca.informatik.uni-freiburg.de/cache-visualization/
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.
Note: The implementation is part of the official CaDiCaL and was described in a Pragmatics of SAT paper 2026 paper.
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 verification, 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.