Effectiveness of pre- and inprocessing for CDCL-based SAT solving

TL;DR

This paper evaluates the effectiveness of pre- and inprocessing techniques in CDCL-based SAT solvers, analyzing their impact on formula simplification and overall solving performance through experiments on real-world and combinatorial instances.

Contribution

It provides a comprehensive analysis of various simplification algorithms, identifying which techniques improve solver speed and which should be avoided for practical SAT solving.

Findings

Certain simplification techniques significantly reduce solving time.

Some combinations of algorithms lead to speedups, others cause slowdowns.

The impact varies depending on the instance type and algorithm used.

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.