Projects and Teaching

Open and Running Theses

• Graph-Hashes for SAT Instance Isomorphism (Bachelor Thesis)
  The equivalence class of isomorphic SAT instances encompasses associative permutation of operands, renaming of variables and inversion of literal polarities. SAT instances are normally given in conjunctive normal form (CNF), and one possibility for over-approximating the class of isomorphic CNF instances is to compare the hashes of their sorted degree sequence [1]. The task is to use ideas from [1] and [2] to devise new efficient implementations of CNF hashes and to evaluate them based on performance as well as their false positive rate.
  [1] Isohash for CNF Instances
  [2] Weisfeiler-Lehman Graph Kernels
• Fast and Optimal Compression Algorithms for Propositional Models (Bachelor Thesis)
  The task is to compress propositional models, i.e. satisfying assignments to the variables in a propositional formula. Compression can be achieved by not saving variable values that can be derived from the formula and other values by unit propagation. The aim of this thesis is to implement efficient (de-)compression algorithms, to evaluate their efficiency and to evaluate different heuristics for variable ordering with respect to the resulting compressed model sizes.
• Localized Clause Scores for Parallel SAT Solvers (Bachelor Thesis)
  The scoring of clauses with the help of heuristics plays an important role in clause-learning SAT solvers. In sequential SAT solvers, such scoring heuristics decide in periodic cleanup steps which of the learned clauses are forgotten. In parallel SAT solver portfolios, such heuristics are also used when clauses are exchanged between solvers to decide which clauses to reject. Heuristics for ranking clauses primarily consider how much a learned clause restricts the search space, such as the size-heuristic, which favors short clause lengths. Modern heuristics like LBD and Activity for sequential CDCL solvers take into account the current state and course of the search. Using these heuristics in parallel SAT solvers is not necessarily meaningful due to the state dependency, i.e. at the time of sharing, a clause can be important in one solver but useless in another solver. The aim of this master thesis is to store the search state and course of all solvers of a parallel SAT solver portfolio in such a way that externally learned clauses can be re-evaluated locally and discarded if necessary.
• Data-Driven Automatic and Optimal Evaluation of SAT Solvers (Bachelor / Master Thesis)
  The project was successfully completed by Tobias Fuchs (see original project description) and resulted in a publication.Further projects based on this are possible and can be discussed and defined on request.
• Explaining Tree Ensembles with SAT-based Automated Reasoning (Master Thesis)
  Efficient tools for automated reasoning are key to some of the most promising rigorous approaches to the explainability of machine-learned (ML) models and thus a central component of the yet young, but rapidly growing field of explainable artificial intelligence (XAI). Despite their problem-solving capabilities, ML models often suffer from opacity, making their inner workings difficult for humans to understand. Developing ways to explain the decisions made by an ML model in a way that humans can understand helps to increase confidence in AI systems beyond their pure predictive accuracy and robustness. The trustworthiness of AI systems is of paramount importance in safety-critical and high-risk applications such as law enforcement and criminal justice, critical infrastructure operations, biometric identification and categorization of natural persons, autonomous vehicles such as self-driving cars or drones, or in healthcare diagnostics and medical devices [2]. SAT-based automated reasoning for XAI helps to debug AI systems, prevent accidents, ensure that AI systems are not used in a discriminatory manner, and facilitates human supervision in collaborative human/AI teams [1].
  [1] From Contrastive to Abductive Explanations and Back Again, Ignatiev et al., 2021
  [2] Explanation in artificial intelligence: Insights from the social sciences, Miller, 2019

Courses

Publications

Supervised Theses