Covered Clause Elimination

TL;DR

This paper introduces new variants of clause elimination procedures for CNF formulas, demonstrating their superior effectiveness over existing methods in reducing formula size for SAT solving.

Contribution

It generalizes and extends clause elimination procedures to explicit, hidden, and asymmetric variants, improving formula reduction techniques.

Findings

CCE, HCCE, and ACCE outperform blocked clause elimination in reducing CNF formulas.

The new procedures are effective as preprocessing techniques for SAT solvers.

Experimental results show significant simplification of formulas.

Abstract

Generalizing the novel clause elimination procedures developed in [M. Heule, M. J\"arvisalo, and A. Biere. Clause elimination procedures for CNF formulas. In Proc. LPAR-17, volume 6397 of LNCS, pages 357-371. Springer, 2010.], we introduce explicit (CCE), hidden (HCCE), and asymmetric (ACCE) variants of a procedure that eliminates covered clauses from CNF formulas. We show that these procedures are more effective in reducing CNF formulas than the respective variants of blocked clause elimination, and may hence be interesting as new preprocessing/simplification techniques for SAT solving.