March_dl: Adding Adaptive Heuristics and a New Branching Strategy
Marijn J. H. Heule, Hans van Maaren · Journal on Satisfiability Boolean Modeling and Computation · 2006
We introduce the march dl satisfiability (SAT) solver, a successor of march eq.The latter was awarded state-of-the-art in two categories during the Sat 2004 competition.The focus lies on presenting those features that are new in march dl.Besides a description, each of these features is illustrated with some experimental results.By extending the preprocessor, using adaptive heuristics, and by using a new branching strategy, march dl is able to solve nearly all benchmarks faster than its predecessor.Moreover, various instances which were beyond the reach of march eq, can now be solved -relatively easily -due to these new features.