Restart Strategy Selection using Machine Learning Techniques 7 1. Gather information for features sets I and II. 2. Run a first restart for 100 conflicts.

3. Run a second restart for 2000 conflicts, this restart hosts the observation window, during which feature set III is gathered. At the end of the observation window, feature set IV is gathered.

4. Predict instance's probability of satisfiability using satisfiability classifier.

5. Predict runtime with each of the Models, weighing according to the probability of satisfiability.

6. Choose the strategy with the minimal weighted runtime.

have noticed that the first restart tends to be very noisy, and that results are better if data is collected in the second restart onwards. We have tried several options for the observation window location and size, eventually we opted for a first restart which is very short (100 conflicts), followed by a second restart (of size 2000) which hosts the observation window. Hence the observation window is closed and all data is gathered after 2100 conflicts.

Once the feature vector x is gathered it is used with the classifier to determine the probability of the instance to be satisfiable, P(sat|x**). For each of the**
strategies, both models are queried and a best strategy sb(x**) is picked using**

## Sb(X**) = Arg Min** S∈S [P(Sat|X) · Msat,S(X) + P(**Unsat**|X) · Munsat,S(X)].

The restart strategy which is predicted to be the first to terminate is picked, and the solver starts following this strategy from the next restart onwards. Although restart strategies are usually followed from the beginning of the search, we do not want to lose the learned clauses from the first 2100 conflicts. Therefore, we continue the current solving process and keep the already learnt clauses. We denote the restart sequence that takes place from the first restart to termination as **LMP ick**sb

. It is important to note that sb 6= **LMP ick**sb

.

## 4 Results 4.1 Experiment Settings

In this study we used TiniSat (version 0.22) [12] as the basic solver. TiniSat is a lightweight DPLL style solver that was first presented in the SAT Race of 2006. TiniSat is a modern solver that uses clause learning and a unique **decision** heuristic that generally favours variables from recent assignments (as in BerkMin
[8]) and uses VSIDS [17] over the literals as a backup. We chose to use **TiniSat** since (i) it is tuned in a way that would make comparison of restart strategies more meaningful [11] and (ii) it is a compact and straightforward implementation which allows for greater ease of use. TiniSat is not equipped with a pre-processor, and we have not used any in our study. By default, TiniSat uses a Luby restart strategy with a run unit of 512 conflicts.