March dl
Adding Adaptive Heuristics and a New Branching Strategy
More Info
expand_more
expand_more
Abstract
We introduce the march dl satisability (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 pre-processor, 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.
Files
JSAT2_3_Heule.pdf
(pdf | 0.198 Mb)