Symbiosis of Search and Heuristics for Random 3-SAT
This work addresses the challenge of efficiently solving random SAT instances, which is important for SAT solver developers and researchers in computational logic, though it is incremental as it builds on existing heuristics and search methods.
The paper tackles the problem of solving random 3-SAT formulae by introducing a new branching heuristic and a variant of discrepancy search (ALDS), which together enable the solver march to achieve state-of-the-art performance, winning the SAT 2009 competition as the strongest complete solver on random 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.