SSP Group Meeting
Wednesday, April 12th, 11am-12pm
Division of Informatics, 80 South Bridge, Room F13


Local Search Cost on Random SAT

Josh Singer

The cross-university research group APES ( to which I am affiliated studies search and search control, particularly via empirical methods. We tend to look at simple NP-complete problems like constraint satisfaction. This area has IMHO had quite a resurgence in the last decade or so, as people have come to find that despite the NP-completeness of these problems, real-world instances of a useful size can actually be solved in a reasonable time by the right algorithm. I'll introduce the idea of "satisfiability thresholds" in random problems before concentrating on my own work.

The abstract from the relevant report on this work is:

The local search algorithm WSat is one of the most successful algorithms for solving the satisfiability (SAT) problem. It is notably effective at solving hard Random 3-SAT instances near the so-called `satisfiability threshold', but still shows a peak in search cost near the threshold and large variations in cost over different instances. We make a number of significant contributions to the analysis of WSat on high-cost random instances, using the recently-introduced concept of the backbone of a SAT instance. The backbone is the set of literals which are entailed by an instance. We find that the number of solutions predicts the cost well for small-backbone instances but is much less relevant for the large-backbone instances which appear near the threshold and dominate in the overconstrained region. We show a very strong correlation between search cost and the Hamming distance to the nearest solution early in WSat's search. This pattern leads us to introduce a measure of the backbone fragility of an instance, which indicates how persistent the backbone is as clauses are removed. We propose that high-cost random instances for local search are those with very large backbones which are also backbone-fragile. We suggest that the decay in cost beyond the satisfiability threshold is due to increasing backbone robustness (the opposite of backbone fragility). Our hypothesis makes three correct predictions. First, that the backbone robustness of an instance is negatively correlated with the local search cost when other factors are controlled for. Second, that backbone-minimal instances (which are 3-SAT instances altered so as to be more backbone-fragile) are unusually hard for WSat. Third, that the clauses most often unsatisfied during search are those whose deletion has the most effect on the backbone. In understanding the pathologies of local search methods, we hope to contribute to the development of new and better techniques.