March dl

Adding Adaptive Heuristics and a New Branching Strategy

Journal article (2006)
Department
Software Technology (EEMCS) (TU Delft)
Copyright: Van Maaren, H.
Look-ahead Adaptive heuristics SAT solving SAT competition
More Info
expand_more

Published Date

01-03-2006

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Source:

Journal on Satisfiability, Boolean Modeling and Computation 2 (2006)

ISSN:

1574-0617

Faculty

Electrical Engineering, Mathematics and Computer Science

Department

Software Technology

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)