SATbed: A Configurable Environment for Reliable Performance Experiments with SAT Instance Classes and Algorithms

Analysis of our recent experiments for a group of SAT solvers and several classes of problem instances suggests a common mathemat- ical framework with experiments in component reliability. In the latter, we observe the distribution of component lifetime; in the former, we observe the distribution of execution time (runtime). A lifetime distri- bution for hardware components is frequently found to have an expo- nential, Weibull, Pareto, or gamma distribution. Our experiments with state-of-the-art SAT solvers reveal normal distributions and exponential distributions of runtime and other related random variables, as well as other distributions commonly observed in reliability applications. SATbed, an experimental testbed for SAT solvers, emulates the reli- ability framework: equivalence classes of isomorphic problem instances (replicated hardware components), subjected to tests with specific SAT solvers (specifically controlled environments), observations of runtime, implications, etc. (lifetime), statistical analysis and modeling, based on random variable samples. The testbed not only facilitates systematic study and reliable improvement of any SAT solver but also supports the introduction and validation of new problem instance classes.