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.
Sprache der Kurzfassung:
Englisch
Veröffentlicher:
Institute for Formal Models and Verification, Johannes Kepler University