On the Empirical Time Complexity of Random 3-SAT at the Phase Transition

Abstract

The time complexity of problems and algorithms, i.e., the scaling of the time required for solving a problem instance as a function of instance size, is of key interest in theoretical computer science and practical applications. In this context, propositional satisfiability (SAT) is one of the most intensely studied problems, and it is generally believed that solving SAT requires exponential time in the worst case. For more than two decades, random 3-SAT at the solubility phase transition has played a pivotal role in the theoretical and empirical investigation of SAT solving, and to this day, it is arguably the most prominent model for difficult SAT instances. Here, we study the empirical scaling of the running time of several prominent, high-performance SAT solvers on random 3-SAT instances from the phase transition region. After introducing a refined model for the location of the phase transition point, we show that the median running time of three incomplete, SLS-based solvers — WalkSAT/SKC, BalancedZ and probSAT — scales polynomially with instance size. An analogous analysis of three complete, DPLL-based solvers — kcnfs, march_hi and march_br — clearly indicates exponential scaling of median running time. Moreover, exponential scaling is witnessed for these DPLL-based solvers when solving only satisfiable and only unsatisfiable instances, and the respective scaling models for each solver differ mostly by a constant factor.