Easy Predictions for the Easy-Hard-Easy Transition

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 18

Satisfiability

We study the scaling properties of sequential and parallel versions of a local search algorithm, WalkSAT, in the easy regions of the easy-hard-easy phase transition (PT) in Random 3SAT. In the underconstrained region, we study scaling of the sequential version of WalkSAT. We find linear scaling at fixed clause/variable ratio. We also study the case in which a parameter inspired by "finite-size scaling" is held constant. The scaling then also appears to be a simple power law. Combining these results gives a simple prediction for the performance of WalkSAT over most of the easy region. The experimental results suggest that WalkSAT is acting as a threshold algorithm, but with threshold below the satisfiability threshold. Performance of a parallel version of WalkSAT is studied in the over-constrained region. This is more difficult because it is an optimization rather than decision problem. We use the solution quality, the number of unsatisfied clauses, obtained by the sequential algorithm to set a target for its parallel version. We find that qualities obtained by the sequential search with O(n) steps, are achievable by the parallel version in O(log(n)) steps. Thus, the parallelization is efficient for these "easy MAXSAT" problems.