Active Partial Label Learning for Parallel Benchmarking

Benchmarking is an essential part of algorithm development. This also applies to solvers for the SAT (propositional satisfiability) problem. Comparing a new solver to an established portfolio of solvers often requires benchmarking it on large amounts of difficult instances. Dynamic benchmark selection strategies utilizing AL (active learning) can reduce the number of benchmark instances required to accurately estimate the rank of a new solver. However, these strategies do not run benchmark experiments in parallel, which limits their real world applicability. In this thesis, we present a parallelizable AL strategy for dynamic benchmark selection. We evaluate our approach on the Anniversary Track dataset from the 2022 SAT Competition. Our approach can determine a new solver’s PAR-2 ranking with about 91% accuracy while only needing 13.5% of the CPU-runtime of a full evaluation and running up to 64 benchmark experiments in parallel