Projects and Teaching

Open and Running Theses

• Graph-Hashes for Benchmark Instance Isomorphism (Bachelor Thesis)
  The equivalence class of isomorphic SAT instances, usually given in conjunctive normal form (CNF), includes associative permutation of operands, renaming of variables, and inversion of literal polarities. One way to over-approximate the class of isomorphic CNF instances is to compare the hashes of their sorted degree sequences [1]. The task of this thesis is to implement tighter approximations that take into account ordered degree sequences of node neighborhoods according to [2]. The variants should be analyzed by false positive rates, which can be estimated based on normal forms that can be generated with existing tools like Saucy [3].
  [1] Isohash for CNF Instances
  [2] Weisfeiler-Lehman Graph Kernels
  [3] https://github.com/hrbrmstr/saucy
  Instance isomorphism and similarity are also interesting topics in related problems such as MaxSAT or Pseudo-Boolean Optimization. We can extend the topic to such other areas on request and based on an initial discussion.
• Fast and Optimal Compression Algorithms for Propositional Models (Bachelor Thesis)
  The task in this thesis is to compress propositional models, i.e., satisfying assignments to the variables in a propositional formula. Compression can be achieved by omitting values that can be derived by unit propagation. The goal of this thesis is to implement efficient (de-)compression algorithms, to evaluate their efficiency, and to evaluate different variable ordering heuristics with respect to the resulting compressed model sizes.
• Localized Clause Scores for Parallel SAT Solvers (Bachelor Thesis)
  Heuristic scoring of clauses 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 used when exchanging clauses between solvers to decide which clauses to reject. The use of these heuristics in parallel SAT solvers is not necessarily meaningful due to their state dependency, i.e., at the time of exchange, a clause may be important in one solver but useless in another solver. The goal of this thesis is to explore different state-dependent ways to locally re-evaluate and discard clauses when 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 upon request.
• Explaining Tree Ensembles with SAT-based Automated Reasoning (Master Thesis)
  Efficient automated reasoning tools are key to some of the most promising rigorous approaches to explainability of machine learning (ML) models, and thus a central component of the young but rapidly growing field of Explainable Artificial Intelligence (XAI). SAT-based automated reasoning for XAI can help debug AI systems, prevent accidents, and ensure that AI systems are not used in a discriminatory manner [1]. Most existing approaches aim to explain the cause of a single prediction, and few deal with enumerating them. However, due to the exponential number of explanations in the worst case, enumeration is often infeasible. The goal of this work is to formalize some objective functions of the problem taxonomy specified in [1] as a MaxSAT objective function, and to enumerate optimal explanations with respect to this function.
  [1] https://arxiv.org/pdf/2407.17454

Courses

Publications

Supervised Theses