Symbiosis of Search and Heuristics for Random 3-SAT
Abstract
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.
Keywords
Cite
@article{arxiv.1402.4455,
title = {Symbiosis of Search and Heuristics for Random 3-SAT},
author = {Sid Mijnders and Boris de Wilde and Marijn Heule},
journal= {arXiv preprint arXiv:1402.4455},
year = {2014}
}
Comments
Proceedings of the Third International Workshop on Logic and Search (LaSh 2010)