Efficient All-UIP learned clause minimization
Abstract: 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
- Standort
-
Deutsche Nationalbibliothek Frankfurt am Main
- Umfang
-
Online-Ressource
- Sprache
-
Englisch
- Anmerkungen
-
ISBN: 978-3-030-80223-3
ISSN: 1611-3349
- Ereignis
-
Veröffentlichung
- (wo)
-
Freiburg
- (wer)
-
Universität
- (wann)
-
2023
- Urheber
- DOI
-
10.1007/978-3-030-80223-3_12
- URN
-
urn:nbn:de:bsz:25-freidok-2393754
- Rechteinformation
-
Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Letzte Aktualisierung
- 14.08.2025, 08:50 UTC
Datenpartner
Deutsche Nationalbibliothek. Bei Fragen zum Objekt wenden Sie sich bitte an den Datenpartner.
Beteiligte
- Fleury, Mathias
- Biere, Armin
- Universität
Entstanden
- 2023
Ähnliche Objekte (12)
Efficient Approximation Algorithms for Adaptive Seed Minimization
Efficient numerical methods for total variation minimization
Efficient partnership dissolution under buy/sell clauses
Data-Efficient Learned Database Components
All for one? EU’s toothless mutual defence clause
6. Finite Complement Clauses and Adverbial Clauses
Clause, Ferdinand
Clause, Adolf
Clause, Adolphe
Clause générale
Relative Clauses and Noun-Modifying Clauses in Chantyal
Clause combining in Semitic : the circumstantial clause and beyond
Efficient Approximation Algorithms for Adaptive Seed Minimization
Efficient numerical methods for total variation minimization
Efficient partnership dissolution under buy/sell clauses
Data-Efficient Learned Database Components
All for one? EU’s toothless mutual defence clause
6. Finite Complement Clauses and Adverbial Clauses
Clause, Ferdinand
Clause, Adolf
Clause, Adolphe
Clause générale
Relative Clauses and Noun-Modifying Clauses in Chantyal
Clause combining in Semitic : the circumstantial clause and beyond
Efficient Approximation Algorithms for Adaptive Seed Minimization
Efficient numerical methods for total variation minimization
Efficient partnership dissolution under buy/sell clauses
Data-Efficient Learned Database Components
All for one? EU’s toothless mutual defence clause
6. Finite Complement Clauses and Adverbial Clauses
Clause, Ferdinand
Clause, Adolf
Clause, Adolphe
Clause générale
Relative Clauses and Noun-Modifying Clauses in Chantyal