Efficient All-UIP Learned Clause Minimization (Extended Version)

In 2020 Feng & Bacchus revisited variants of the all-UIP learning strategy, which considerably improved performance of their ver- sion of CaDiCaL submitted to the SAT Competition 2020, particularly on large planning instances. We improve on their algorithm by tightly integrating this idea with learned clause minimization. This yields a clean shrinking algorithm with complexity linear in the size of the impli- cation graph. It is fast enough to unconditionally shrink learned clauses until completion. We further define trail redundancy and show that our version of shrinking removes all redundant literals. Independent experi- ments with the three SAT solvers CaDiCaL, Kissat, and Satch confirm the effectiveness of our approach.