SAT Solving At Scale

The NP-complete propositional satisfiability (SAT) problem is an essential building block at the core of automated reasoning and Symbolic AI, and, in a sense, the canonical "difficult problem" of computer science. Due to the expressivity and genericity of the problem, SAT solvers have become crucial tools for a surprising variety of academic and industrial applications. As such, advancing scalable SAT solving methods bears immense potential for simultaneously advancing a plethora of important disciplines from computer science and real-world applications. Our research allows to efficiently exploit parallel and distributed computational environments, such as supercomuters and clouds, for SAT solving and related tools of automated reasoning.

Correctness Guarantees via Proofs

Our research transfers the concept of proofs of unsatisfiability to distributed solvers in a scalable manner. Such proofs are able to grant full confidence in a claimed result, since they can be independently validated by checker programs that are formally verified down to the machine code level. Parallel and distributed SAT solvers solvers have long been considered much less trustworthy than their sequential counterparts, and rightfully so – due to more complex technology stacks, less comprehensive testing, and no realistic ways to produce proofs. Our latest works enable users to exploit large-scale SAT solving for some of the most safety– or security-critical tasks that arise from applications.

The Mallob System

Mallob (Malleable Load Balancer, or Massively Parallel Logic Backend) is a distributed platform for processing automated reasoning tasks (primarily SAT instances) in modern large-scale HPC and cloud environments. Mallob's flexible and decentralized approach to job scheduling allows to concurrently process many tasks of varying priority by different users. As such, Mallob can drastically improve your academic or industrial workflows tied to automated reasoning. Mallob's tightly integrated distributed general-purpose SAT solving engine, MallobSat, has received a large amount of attention, including five gold medals of the International SAT Competition's Cloud Track in a row. Read more

October 29, 2024

The HPC project “Scalable Discrete Algorithms for Big Data Applications” has received a Golden Spike Award of the Höchstleistungsrechenzentrum Stuttgart (HLRS) Results and Review Workshop 2024 in Karlsruhe, Germany.
Read more

October 2, 2024

The young investigator group on Scalable Automated Reasoning at the Department of Informatics at the Karlsruhe Institute of Technology (KIT, in Germany) is looking for a research assistant (a.k.a. doctoral researcher, PhD student), beginning as soon as possible.
Read more

October 1, 2024

Welcome to the website of the Scalable Automated Reasoning (SAtRes) group. October 1st, 2024 marks the kick-off of this KiKIT-funded young investigator group led by Dominik Schreiber that aims to push the frontiers of automated reasoning in parallel and distributed systems.
Read more

September 27, 2024

Dominik Schreiber has received two high-ranking awards for his doctoral research on scalable SAT Solving: the tri-national dissertation award jointly conferred by the German Informatics Society (GI), the Austrian Computer Society (OCG), and the Swiss Informatics Society (SI); and the 2022-2023 Fahiem Bacchus Award conferred by the SAT Association.
Read more