A recent series of experiments with a group of state-of-the-art SAT solvers and several well-defined classes of problem instances reports statistically significant performance variability for the solvers. A systematic analysis of the observed performance data, all openly archived on the Web, reveals distributions which we classify into three broad categories: (1) readily characterized with a simple
RA ( x )\mathcal{R}^A \left( x \right)
(where
x represents the
lifetime) is the complement of the
solvability function
SA ( x ) = 1-RA ( x )\mathcal{S}^A \left( x \right) = 1--\mathcal{R}^A \left( x \right)
where
x may represent
runtime, implications, backtracks, etc. As demonstrated in the paper, a set of unrelated benchmarks or randomly generated SAT instances available today cannot measure the performance of SAT solvers reliably — there is no control on their

hardness

. However, equivalence class instances as defined in this paper are, in effect, replicated instances of a specific reference instance. The proposed method not only provides a common platform for a systematic study and a
reliable improvement of deterministic
and stochastic SAT solvers alike but also supports the introduction and validation of new problem instance classes.
Keywords satisfiability - conjunctive normal form - equivalence classes - experimental design - exponential and heavy-tail distributions - reliability function