Field of Research

The Scalable Automated Reasoning group aims to push the frontiers of automated reasoning by advancing the essential tools at its core, with a distinct focus on scalable parallel and distributed computing.

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

Find further information on our research page.