View Related Documents

Abstract

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 lsquohardnessrsquo. 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

Fulltext Preview

Image of the first page of the fulltext document