Armin Biere, Andreas Fröhlich,
"Evaluating CDCL Restart Schemes"
: Proc. Intl. Workshop on Pragmatics of SAT, SAT'15 Austin, Tx, USA, 2015
Original Titel:
Evaluating CDCL Restart Schemes
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. Intl. Workshop on Pragmatics of SAT
Original Kurzfassung:
Modern CDCL (conflict-driven clause learning) SAT solvers are used for many practical applications.
One of the key ingredients of state-of-the-art CDCL solvers are efficient restart schemes. The main
contribution of this work is an extensive empirical evaluation of various restart strategies. We show that
optimal static restart intervals are not only correlated with the satisfiability status of a certain instance,
but also with the more specific problem class of the given benchmark. We further compare uniform
restart intervals with the performance of non-uniform restart schemes, such as Luby restarts. Finally,
we revisit the dynamic restart strategy used in Glucose and propose a new variant thereof, which
is based on the concept of exponential moving averages. The resulting implementation in Lingeling
improves state-of-the-art performance in SAT solving.
Forschungs-