SAtRes    News    Parallel Constraint Solving Tutorial at CP'25

Parallel Constraint Solving Tutorial at CP'25

June 27, 2025

This summer, Shaowei Cai (Chinese Academy of Sciences, Beijing, China) and Dominik Schreiber (SAtRes) will jointly present a tutorial on parallel constraint solving at the 31st Conference on Principles and Practice of Constraint Programming in Glasgow, UK (August 10-15, 2025).

Motivation

Over the last years, we have witnessed significant advances in the effective and efficient parallelization of crucial constraint solving frameworks, such as propositional satisfiability (SAT) and mixed integer programming (MIP). At times exploiting several thousand cores at once, modern parallel constraint solvers are capable of solving many challenging and relevant problem instances dozens to hundreds of times faster than their best available sequential counterparts. Distributed solvers can also be used to conquer otherwise infeasible application instances and even to solve long-standing open problems of mathematics. At the same time, parallel and distributed tools are generally less accessible than their sequential counterparts and come with a non-negligible barrier of entry. As a consequence, the use of parallel constraint solving for application-oriented research is still more of an exception than a rule, which is in stark contrast to today’s increasingly parallel computing environments and the central role they play in other fields with more well-established parallelization methods (e.g., in Machine Learning and LLMs).

Overview

Our tutorial addresses researchers, authors, and users of constraint solvers. It provides a self-contained (in terms of parallel computing) introduction and overview of parallel constraint solving and highlights some of its most crucial tools. We will provide surveys of parallelization techniques for some of the most crucial constraint problem frameworks and inform industrial practitioners on recent developments in the field to promote the use of the according parallel tools.

Given that this year’s Constraint Programming conference is co-located with the SAT Solving and Combinatorial Search conferences SAT'2025 and SoCS'2025, we hope to bring together these three related communities and foster some insightful exchanges and discussions on parallel constraint solving.

Part I of the tutorial (D. Schreiber) introduces foundations of (massively) parallel computing, scheduling methods for irregular and unpredictable tasks, and evaluation methodology for parallel constraint solving. Part II (D. Schreiber) disseminates parallel propositional satisfiability (SAT), interspersed with cross-considerations and perspectives on parallel CP solving. Part III (S. Cai) provides an in-depth overview of parallelizations of SMT solving while Part IV (S. Cai) covers recent advances on parallel MIP solving.

The (tentative) structure of the tutorial is as follows:

• Part I: General considerations (D.S.): Foundations of parallel and distributed computing, scheduling of irregular and unpredictable tasks, evaluation methodology for parallel constraint solvers
• Part II: Parallel SAT Solving (D.S.): Overview of paradigms (search space splitting, portfolio, clause sharing), Cube&Conquer, cutting-edge general-purpose parallel solvers (a.k.a. clause-sharing solvers), proof production, connections to related frameworks (CP, incremental SAT, MaxSAT) and future challenges
• Part III: Parallel SMT Solving (S.C.): Brief introduction of SMT, partition methods, portfolio methods, typical parallel SMT solvers, future challenges
• Part IV: Parallel MIP Solving (S.C.): Brief introduction of MIP, parallel local search, parallel branch-and-bound, parallel LLM aided developing paradigms

Presenters

Shaowei Cai is a Professor at Institute of Software, Chinese Academy of Sciences, leader of the Constraint Solving group. He received his PhD degree from Peking University with Distinguished Doctoral Dissertation Award. His research interests include constraint solving and formal methods. Particularly, he has regularly won Gold/Silver medals in recent SAT Competitions, including 5 Gold medals in Parallel tracks won by the PRS solver in his team. The SMT solvers Z3++ and Parti-Z3++ has won “largest contribution” award and “largest leading” awards in Model Validation track and Cloud track in SMT Competitions. He has received the Best/Distiguished Paper Award at SAT 2021, CP 2024 and CAV 2024. He has given tutorials at FMCAD and SoCS conferences.

Dominik Schreiber is a Young Investigator at Karlsruhe Institute of Technology (KIT), Germany. His Scalable Automated Reasoning group conducts research at the intersection of algorithm engineering, formal methods, and parallel/distributed systems. His work, which substantially advanced the state of the art in scalable and efficient large-scale SAT solving, earned him the German, Austrian, and Swiss Informatics Societies’ joint Dissertation Award as well as the SAT Association’s Fahiem Bacchus Award. His parallel and distributed system Mallob consistently scores top rankings at the International SAT Competitions. He has given talks and guest lectures on his work at ETH Zurich, University of Freiburg, JKU Linz, and Schloss Dagstuhl.