|
Abstract:
|
We present an experimental investigation of the following questions:
how does the average-case complexity of random 3-SAT 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 order of 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 CPLEX shift from polynomial to exponential
complexity at a density of about 3.8, CUDD exhibts 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 desity-aware solvers for 3-SAT.
|