Coprocessor - a Standalone SAT Preprocessor

TL;DR

Coprocessor is a standalone SAT preprocessor that enhances formula reduction by implementing advanced techniques, leading to improved solving performance in SAT solvers like riss and MiniSat 2.2.

Contribution

It introduces a comprehensive, standalone preprocessor for SAT that incorporates recent preprocessing techniques not present in existing tools.

Findings

Reduces redundancy in SAT formulas more effectively.

Improves overall SAT solving performance.

Compatible with riss and MiniSat 2.2.

Abstract

In this work a stand-alone preprocessor for SAT is presented that is able to perform most of the known preprocessing techniques. Preprocessing a formula in SAT is important for performance since redundancy can be removed. The preprocessor is part of the SAT solver riss and is called Coprocessor. Not only riss, but also MiniSat 2.2 benefit from it, because the SatELite preprocessor of MiniSat does not implement recent techniques. By using more advanced techniques, Coprocessor is able to reduce the redundancy in a formula further and improves the overall solving performance.