Random 3-SAT: The plot thickens

Abstract

This paper presents an experimental investigation of the following questions: how does the average-case complexity of random 3- SAT, understood as a function of the order (number of variables) for fixed density (ratio of number of clauses to order) instances, depend on the density? Is there a phase transition in which the complexity shifts from polynomial to exponential? Is the transition dependent or independent of the solver? To study these questions, we gather median and mean running times for a large collection of random 3-SAT problems while systematically varying both densities and the order of the instances. We use three different complete SAT solvers, embodying very different underlying algorithms: GRASP, CPLEX, and CUDD. We observe new phase transitions for all three solvers, where the median running time shifts from polynomial in the order to exponential. The location of the phase transition appears to be solver-dependent. While GRASP and CUDD shift from polynomial to exponential complexity at a density of about 3.8, CUDD exhibits this transition between densities of 0.1 and 0.5. We believe these experimental observations are important for understanding the computational complexity of random 3-SAT, and can be used as a justification for developing density-aware solvers for 3-SAT.