March_dl: Adding Adaptive Heuristics and a New Branching Strategy

Abstract

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 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.