ResearchWe understand automated reasoning as the algorithmic exploration of a formal rule set in order to deduce relevant properties. The many use cases of automated reasoning include electronic hardware design, mathematical theorem proving, and verifying the security, correctness, and fairness of critical systems. Our aim is to study and advance the algorithmic toolbox at the core of automated reasoning with a distinct focus on parallel and distributed algorithms. Notable examples for such tools include propositional satisfiability (SAT) solving, Satisfiability Modulo Theories (SMT), Bounded Model Checking (BMC), combinatorial optimization (e.g., MaxSAT), and automated planning and scheduling.
The proposal From Mavericks to Teamplayers: Fostering Solver Cooperation in Distributed SAT Solving was awarded with a 2024 Amazon Research Award, with Prof. Armin Biere (University of Freiburg) as Principal Investigator, Dominik Schreiber (SAtRes) as associated personnel and (de facto) Co-PI, and Prof. Peter Sanders (Algorithm Engineering, ITI, KIT) as cooperation partner.
KiKIT is a pilot programme in the Helmholtz Association to evaluate the potential and the need of an integration of basic and foundational research into Helmholtz’ mission of provisional research.
The platform Mallob (Malleable Load Balancer, or Massively Parallel Logic Backend) is a distributed platform for processing automated reasoning tasks in modern large-scale HPC and cloud environments.