Backbone of Satisfiability

The backbone of satisfiability is the set of variables that take the same value in every satisfying assignment of a Boolean formula. In the underconstrained regime, the backbone is small — variables are free to vary across solutions. As a constraint satisfaction problem approaches the critical threshold, the backbone grows rapidly, freezing variables into fixed values that must be respected by any solution. The backbone is the skeletal structure of a problem instance: it captures what is non-negotiable, what the constraints have already decided before the search algorithm begins.

The growth of the backbone correlates with algorithmic hardness. When the backbone is small, local search can wander freely. When the backbone is large, wrong choices early in the search propagate into unavoidable contradictions. The backbone is therefore not merely a structural curiosity; it is a diagnostic tool for predicting where an instance lies in the phase transition landscape and which algorithms are likely to succeed. The backbone also connects to the concept of frozen variables in statistical mechanics, where variables become locked into single values by the geometry of the energy landscape.