Universität zu Köln

Wotzlaw, Andreas, van der Grinten, Alexander and Speckenmeyer, Ewald (2013). Effectiveness of pre- and inprocessing for CDCL-based SAT solving. Technical Report.

Preview

PDF submitted.pdf Download (298kB) | Preview

Abstract

Applying pre- and inprocessing techniques to simplify CNF formulas both before and during search can considerably improve the performance of modern SAT solvers. These algorithms mostly aim at reducing the number of clauses, literals, and variables in the formula. However, to be worthwhile, it is necessary that their additional runtime does not exceed the runtime saved during the subsequent SAT solver execution. In this paper we investigate the efficiency and the practicability of selected simplification algorithms for CDCL-based SAT solving. We first analyze them by means of their expected impact on the CNF formula and SAT solving at all. While testing them on real-world and combinatorial SAT instances, we show which techniques and combinations of them yield a desirable speedup and which ones should be avoided.

Item Type:	Monograph (Technical Report)
Creators:	Creators Email ORCID ORCID Put Code Wotzlaw, Andreas UNSPECIFIED UNSPECIFIED UNSPECIFIED van der Grinten, Alexander UNSPECIFIED UNSPECIFIED UNSPECIFIED Speckenmeyer, Ewald UNSPECIFIED UNSPECIFIED UNSPECIFIED
URN:	urn:nbn:de:hbz:38-550459
Date:	March 2013
Language:	English
Faculty:	Faculty of Mathematics and Natural Sciences
Divisions:	Faculty of Mathematics and Natural Sciences > Department of Mathematics and Computer Science > Institute of Computer Science
Subjects:	Data processing Computer science
Uncontrolled Keywords:	Keywords Language ARRAY(0x55e9335425f8) UNSPECIFIED
Refereed:	No
URI:	http://kups.ub.uni-koeln.de/id/eprint/55045