The Satisfiability Constraint Gap

We describe an experimental investigation of the satisfiability phase transition for several different classes of randomly generated problems. We show that the ''conventional'' picture of easy-hard-easy problem difficulty is inadequate. In particular, there is a region of very variable problem difficulty where problems are typically underconstrained and satisfiable. Within this region, problems can be orders of magnitude harder than problems in the middle of the satisfiability phase transition. These extraordinarily hard problems appear to be associated with a ''constraint gap''. That is, a region where search is a maximum as the amount of constraint propagation is a minimum. We show that the position and shape of this constraint gap change little with problem size. Unlike hard problems in the middle of the satisfiability phase transition, hard problems in the variable region are not critically constrained between satisfiability and unsatisfiability. Indeed, hard problems in the variable region often contain a small and unique minimal unsatisfiable subset or reduce at an early stage in search to a hard unsatisfiable subproblem with a small and unique minimal unsatisfiable subset. The difficulty in solving such problems is thus in identifying the minimal unsatisfiable subset from the many irrelevant clauses. The existence of a constraint gap greatly hinders our ability to find such minimal unsatisfiable subsets. However, it remains open whether these problems remain hard for more intelligent backtracking procedures. We conjecture that these results will generalize both to other SAT problem classes, and to the phase transitions of other NP-hard problems.