Armin Biere: Model checking, SAT and bit-vectors + Evaluating CDCL restart schemes

PRACTICALITIES

Lunch is served at 12:00 noon (register at this doodle at the latest the Saturday before, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for ca two hours of more technical discussions.

ABSTRACT

The lunch seminar part is titled "Model checking, SAT and bit-vectors" with abstract as follows.

Both SAT solving and Model Checking are considered to have saved the reputation of formal methods. We will highlight how their recent history is actually closely related. We further discuss important developments in both domains, mostly from the historical and practical point of view, but then will delve into the complexity of deciding bit-vector logic. This logic is the most important theory for bit-precise reasoning with SMT solvers and has many practical applications in testing and verification both of Hardware and Software. Related to solving certain bit-vector problems is the challenge to make bit-level arithmetic reasoning work.

After the break, there will be a more technical presentation on evaluating restart schemes for CDCL SAT solvers, which is based on joint work with Andreas Fröhlich.

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.