performance. We start by discussing the different universal strategies and recent machine learning success in Sect. 2. In Sect. 3 we present *LMPick***, a restart**
strategy portfolio based solver. Experimental results are presented and analyzed in Sect. 4. We conclude and suggest optional future study in Sect. 5.

## 2 Background

Competitive DPLL solvers typically use restarts. Most use "universal" strategies, while some use "dynamic" restart schemes, that induce or delay restarts (such as the ones presented in [1] and [22]).

Currently, the most commonly used universal strategies fall into one of the following categories:

- *Fixed strategy -* **([9]). In this strategy a restart takes place every constant**
number of conflicts. While some solvers allow for a very short interval between restarts, others allow for longer periods, but generally fixed strategies lead to a frequent restart pattern. Examples of its use can be found in BerkMin [8] (where the fixed restart size is 550 conflicts) and Seige [21] (fixed size is 16000 conflicts).

- *Geometric strategy -* **([23]). In this strategy the size of restarts grows geometrically. This strategy is defined using an initial restart size and a geometric**
factor. Wu and van Beek [24] show that the expected runtime of this strategy can be unbounded worse than the optimal fixed strategy in the **worst**
case. They also present several conditions which, if met, guarantee that the geometric strategy would yield a performance improvement. This strategy is used by MiniSat v1.14 [5] with initial restart size of 100 conflicts and a geometric factor of 1.5.

- *Luby Strategy -* ([16]). In this strategy the length of restart i is u · ti **when**
u **is a constant "unit size" and**

$$t_{i}=1$$
$$\begin{cases}2^{k-1},&\text{if}i=2^{k}-1\\ t_{i-2^{k-1}+1},&\text{if}2^{k-1}\leq i<2^{k}-1.\end{cases}$$

The first elements of this sequence are 1,1,2,1,1,2,4,1,1,2,1,1,2,4,8,1,1,... Luby, Sinclair and Zuckerman [16] show that the performance of this strategy is within a logarithmic factor of the true optimal strategy, and that any universal strategy that outperforms their strategy will not do it by **more than**
a constant factor. These results apply to pure Las Vegas algorithms, and do not immediately apply to CDCL solvers in which learnt clauses are kept across restarts. The effectiveness of the strategy in CDCL solvers appears mixed ([11],[20]) and there is still no theoretical work that that analyzes its effectiveness in such solvers. However, Luby's restart strategy is used by several competitive solvers including MiniSat2.1 and TiniSat.

- *Nested Restart strategy -* **([2]) This strategy and can be seen as a simplified**
version of the Luby strategy. After every iteration the restart **length grows** geometrically until it reaches a higher bound, at this point the restart size