Symbiosis of Search and Heuristics for Random 3-SAT
Symbiosis of Search and Heuristics for Random 3-SAT
复制标题
随机 3-SAT 的搜索和启发式共生
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Marijn J. H. Heule
中科院分区：
文献类型：
--
作者：
S. Mijnders;B. D. Wilde;Marijn J. H. Heule
代尔夫特理工大学，代尔夫特，荷兰当正确组合时，搜索技术可以揭示复杂的分支启发法的全部潜力。我们在著名的随机 3-SAT 公式中证明了这一观察结果。首先，提出了一种新的分支启发式，它概括了此类的现有工作。使用这种启发式可以构建更小的搜索树。其次，我们介绍差异搜索的一种变体，称为 ALDS。理论和实践证据表明，当与新的启发式方法相结合时，ALDS 会以接近最优的顺序遍历搜索树。搜索和启发式这两种技术都已在前瞻求解器中实现。 SAT 2009 竞赛结果表明，march 是迄今为止随机 k-SAT 公式上最强的完整求解器。
Delft University of Technology, Delft, The NetherlandsAbstract. When combined properly, search techniques can reveal the full poten-tial of sophisticated branching heuristics. We demonstrate this observation on thewell-known class of random 3-SAT formulae. First, a new branching heuristic ispresented, which generalizes existing work on this class. Much smaller searchtrees can be constructed by using this heuristic. Second, we introduce a variantof discrepancy search, called ALDS. Theoretical and practical evidence supportthat ALDS traverses the search tree in a near-optimal order when combined withthe new heuristic. Both techniques, search and heuristic, have been implementedin the look-ahead solvermarch. The SAT 2009 competition results show thatmarch is by far the strongest complete solver on random k-SAT formulae.