Parallel Variable Elimination on CNF Formulas

Autor:	Kilian Gebhardt, Norbert Manthey
Rok vydání:	2013
Předmět:	Exclusive access Computer science Parallel algorithm Preprocessor Variable elimination Algorithm Sequential algorithm
Zdroj:	KI 2013: Advances in Artificial Intelligence ISBN: 9783642409417 KI
DOI:	10.1007/978-3-642-40942-4_6
Popis:	Formula simplification is important for the performance of SAT solvers. However, when applied until completion, powerful preprocessing techniques like variable elimination can be very time consuming. Therefore, these techniques are usually used with a resource limit. Although there has been much research on parallel SAT solving, no attention has been given to parallel preprocessing. In this paper we show how the preprocessing techniques subsumption, clause strengthening and variable elimination can be parallelized. For this task either a high-level variable-graph formula partitioning or a fine-grained locking schema can be used. By choosing the latter and enforcing clauses to be ordered, we obtain powerful parallel simplification algorithms. Especially for long preprocessing times, parallelization is beneficial, and helps Minisat to solve 11 % more instances of recent competition benchmarks.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::1af2c53dfcc25fd5625cc820fe35decd https://doi.org/10.1007/978-3-642-40942-4_6 Zobrazit plný text záznamu