The local search algorithm WSAT is one of the most successful algorithms for solving the archetypal NP-complete problem of satisfiability (SAT). It is notably effective at solving RANDOM-3-SAT instances near the so-called "satisfiability threshold", which are thought to be universally hard. However, WSAT still shows a peak in search cost near the threshold and large variations in cost over different instances. Why are solutions to the threshold instances so hard to find using WSAT? What features characterise threshold instances which make them difficult for WSAT to solve? We make a number of significant contributions to the analysis of WSAT on these high-cost random instances, using the recently-introduced concept of the <i>backbone </i>of a SAT instance. The backbone is the set of literals which are implicates of and 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 undertake a detailed study of the behaviour of the algorithm during search and uncover some interesting patterns. These patterns lead us to introduce a measure of the <i>backbone</i> <i>fragility</i> of an instance, which indicates how persistent the backbone is as clauses are removed. We propose that high-cost random instances for WSAT are those with large backbones which are also backbone-fragile. We suggest that the decay in cost for WSAT beyond the satisfiability threshold, which has perplexed a number of researchers, is due to the decreasing backbone fragility. Our hypothesis makes three correct predictions. First, that a measure of the backbone robustness of an instance (the opposite to backbone fragility) is negatively correlated with the WSAT 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.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:661976 |
| Date | January 2001 |
| Creators | Singer, J. B. |
| Publisher | University of Edinburgh |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
Page generated in 0.0015 seconds