The paper Abstract Cores in Implicit Hitting Set MaxSat Solving authored by Jeremias Berg together with Fahiem Bacchus and Alex Poole (University of Toronto, Canada), has won the SAT 2020 Best Paper Award at 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT 2020), the primary international conference in its research area.
The work proposes a technique called abstract cores that provides a compact representation for a potentially exponential number of regular unsatisfiable cores. The authors demonstrate how to incorporate abstract core reasoning into the so-called implicit hitting set (IHS) algorithm for maximum satisfiability (MaxSat) and report on an empirical evaluation demonstrating that including abstract cores into a state-of-the-art IHS solver improves its performance enough to surpass the best performing solvers of the most recent 2019 MaxSat Evaluation.