o
Complexity of random 3-SAT
Complexity of random 3-SAT
This project is funded by the National Science Foundation. Project
members are Moshe Vardi,
Demetrios Demopoulos , and
Devika Subramanian.
The Question
How does the average-case complexity of random 3-SAT vary with
density? Is there a phase transition in which the complexity shifts
from polynomial to exponential? Is the transition dependent or
independent of the solver?
Approach
To study these questions, we systematically sample the
two-dimensional density-order space, gathering median and mean
running times for a large collection of random 3-SAT problems.
We use three different complete SAT solvers, embodying very different
underlying algorithms: GRASP, CPLEX, and CUDD.
Summary of results
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 exhibits this
transition between densities of 0.1 and 0.5. Our experimental results
have been partially confirmed by Achlioptas et. al. recently, who
show that the transition from polynomial to exponential complexity
occurs well before the crossover point for DLL-style solvers.
Our work is one of the first to question the commonly held view that
the complexity transition coincides with the crossover point.
More details are in Random 3-SAT: the
plot thickens, in Proceedings of the
International Conference on Constraint Programming, 2000 (with
M. Vardi, D. Demopolous, A. San Miguel Aguirre, C. Coarfa).
The talk corresponding to the above paper is here.