Mathias Fleury, Armin Biere,
"Efficient All-UIP Learned Clause Minimization"
, in Li, Chu-Minand Many\`a, Felip: Proc. 24rd Intl. Conf. on Theory and Applications of Satisfiability Testing -- SAT 2021, in Theory and Applications of Satisfiability Testing ? SAT 2021, Serie Lecture Notes in Computer Science, Vol. volume 12831, Springer International Publishing, Cham, Seite(n) 171-187, 7-2021, ISBN: 978-3-030-80223-3
Original Titel:
Efficient All-UIP Learned Clause Minimization
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 24rd Intl. Conf. on Theory and Applications of Satisfiability Testing -- SAT 2021
Original Kurzfassung:
In 2020 Feng & Bacchus revisited variants of the all-UIP learning strategy, which considerably improved performance of their version 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 implication 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 experiments with the three SAT solvers CaDiCaL, Kissat, and Satch confirm the effectiveness of our approach.
Sprache der Kurzfassung:
Englisch
Journal:
Theory and Applications of Satisfiability Testing ? SAT 2021
Forschungs-