2014/02/18 by Sid Mijnders, Boris de Wilde, Mijnders, Sid +4
Computer Science · Engineering · #Artificial Intelligence (cs.AI) #Constraint Satisfaction and Optimization #Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences #Manufacturing Process and Optimization #Rough Sets and Fuzzy Logic #cs.AI #cs.DS
paper · pdf · doi:10.48550/arxiv.1402.4455
Proceedings of the Third International Workshop on Logic and Search (LaSh 2010)
arxiv created 2014/02/18 · openalex publication_date 2014/02/18 · arxiv updated 2014/02/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.