News
SAT'25 Best Paper AwardSAT'25 Best Paper Award
August 15, 2025
Our publication "Streamlining Distributed SAT Solver Design" (Dominik Schreiber, Niccolò Rigi-Luperti, Armin Biere) has been recognized with the Best Paper Award of the 31st International Conference on Theory and Applications of Satisfiability Testing (SAT) 2025. The awarded work is a collaboration with Prof. Armin Biere (Univ. Freiburg) on some of the more naïve design choices left in distributed SAT solvers and on how to potentially improve upon them.
One of the more surprising insights in our paper is that pre- and inprocessing, crucial for sequential SAT solver performance, actually holds back distributed solving, and simply disabling it improves performance at ≈800 cores. The main reasons for this effect are increasing amounts of redundant work, “language barriers” across solvers induced by differing inprocessing levels, and, potentially, clause sharing subsuming some otherwise effective clause simplifications.
Our proposed streamlined distributed solver design replaces the previously prevalent “portfolio” of diverse, opaque reasoners exchanging insights with a uniform parallel CDCL procedure powered by clause sharing (in the sense of search space pruning) and separate, sequential preprocessing. We show that an according implementation achieves competitive performance at up to 3072 cores, achieving >10% resource efficiency at this scale for sufficiently hard instances. This new design not only reduces the complexity of the SAT solving code run in parallel but also opens up new perspectives on accurately modeling, understanding, and analyzing the according distributed algorithms.
From left to right: Daniel Le Berre, Niccolò Rigi-Luperti, Dominik Schreiber, Armin Biere
As Daniel Le Berre (chair of the Best Paper selection committee) aptly put it during his announcement of the award, “This is not the end of the story” – it is in some sense the beginning, and the Best Paper Award greatly motivates us to continue this line of work on modernizing distributed SAT solving.