随机3- SAT搜索与启发式的共生
Symbiosis of Search and Heuristics for Random 3-SAT
摘要：
当适当地结合时，搜索技术可以揭示复杂分支算法的全部潜力。我们证明了这一观察的著名类随机3-SAT公式。首先，提出了一个新的分支启发式，概括了现有的工作在这个类。使用这种启发式算法可以构造更小的搜索树。其次，我们介绍了差异搜索的一个变种，称为ALDS。理论和实践的证据支持ALDS遍历搜索树在一个接近最优的顺序时，结合新的启发式。这两种技术，搜索和启发式，已经在前瞻求解器中实现。SAT 2009竞赛结果显示，March是迄今为止随机k-SAT公式最强的完整求解器。
英文摘要：
When combined properly, search techniques can reveal the full potential of sophisticated branching heuristics. We demonstrate this observation on the well-known class of random 3-SAT formulae. First, a new branching heuristic is presented, which generalizes existing work on this class. Much smaller search trees can be constructed by using this heuristic. Second, we introduce a variant of discrepancy search, called ALDS. Theoretical and practical evidence support that ALDS traverses the search tree in a near-optimal order when combined with the new heuristic. Both techniques, search and heuristic, have been implemented in the look-ahead solver march. The SAT 2009 competition results show that march is by far the strongest complete solver on random k-SAT formulae.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
