Life span of SAT techniques

TL;DR

This paper investigates the effectiveness and interactions of four SAT solver optimization techniques over a span of years, challenging common assumptions about their benefits and longevity.

Contribution

It provides an empirical analysis of four SAT solver features, testing their individual and combined impacts, and refutes three prevalent hypotheses about their utility and lifespan.

Findings

Disabling features does not always harm solver performance.

The lifespan of these techniques is not limited as previously assumed.

Features do not fully simulate each other, indicating unique contributions.

Abstract

In this paper we take 4 different features of the SAT solver CaDiCaL, blocked clause elimination, vivification, on-the-fly self subsumption, and increasing the bound of variable elimination over the SAT Competitions benchmarks between 2009 and 2022. We study these features by both activating them one-by-one and deactivating them one-by-one. We have three hypothesis regarding the experiments: (i) disabling features is always harmful; (ii) the life span of the techniques is limited; and (iii) features simulate each other. Our experiments cannot confirm any of the hypothesis.