Life span of SAT techniques
Mathias Fleury, Daniela Kaufmann
TL;DR
This paper systematically ablates four inprocessing techniques (BCE, OTFS, BVE+, Vivification) on the CaDiCaL SAT solver across SAT Competition benchmarks from 2009–2022 to study their individual and combined effects. It tests two ablation regimes (base vs. single-feature activations and baseline variants) and compares results across three configurations, revealing no consistent support for hypotheses about harm, finite lifespans, or mutual simulation. The findings show substantial interaction among features, with no single technique reliably dominating or fading, and they suggest that causal analyses are needed to disentangle effects. The work highlights practical implications for evaluating solver features and calls for more rigorous methods to understand feature interactions in SAT solvers.
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.