主干脆弱性和本地搜索成本峰值
Backbone Fragility and the Local Search Cost Peak
摘要：
局部搜索算法WSat是求解可满足性问题的最成功的算法之一。它在解决所谓的“可满足性阈值”附近的硬随机3-SAT实例时特别有效，但在阈值附近的搜索成本中仍然显示出峰值，并且不同实例的成本变化很大。我们作出了一些重大贡献的分析WSAT的高成本的随机实例，使用最近推出的概念的主干SAT实例。主干是实例所包含的文字的集合。我们发现，解决方案的数量预测成本以及小骨干实例，但相关性小得多的大型骨干实例出现在阈值附近，并在过度约束区域占主导地位。我们显示了一个非常强的相关性搜索成本和汉明距离最近的解决方案早期WSAT的搜索。这个模式引导我们引入一个实例的主干脆弱性的度量，它表明当子句被删除时主干的持久性。我们建议，本地搜索的高成本随机实例是那些具有非常大的骨干，骨干脆弱。我们认为，在满足性阈值以上的成本衰减是由于增加骨干的鲁棒性（骨干脆弱性的相反）。我们的假设做出了三个正确的预测。首先，在控制其他因素的情况下，实例的主干鲁棒性与局部搜索成本呈负相关。第二，最小主干实例（即3-SAT实例，经过修改，使其主干更脆弱）对于WSAT来说异常困难。第三，在搜索过程中最经常不满足的子句是那些删除对主干影响最大的子句。在了解局部搜索方法的病理学，我们希望有助于新的和更好的技术的发展。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
