Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Clause Sharing in Parallel MaxSAT
verfasst von : Ruben Martins, Vasco Manquinho, Inês Lynce
Erschienen in: Learning and Intelligent Optimization
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In parallel MaxSAT solving, sharing learned clauses is expected to help to further prune the search space and boost the performance of a parallel solver. However, not all learned clauses should be shared since it could lead to an exponential blow up in memory and to sharing many irrelevant clauses. The main question is which learned clauses should be shared among the different threads. This paper reviews the existing heuristics for sharing learned clauses, namely, static and dynamic heuristics. Moreover, a new heuristic for clause sharing is presented based on
freezing
shared clauses. Shared clauses are only incorporated into the solver when they are expected to be useful in the near future. Experimental results show the importance of clause sharing and that the freezing heuristic outperforms other clause sharing heuristics.