Restart Strategy Selection using Machine Learning Techniques 5

![0_image_0.png](0_image_0.png)

| Set III: 26-29. Backjump Size: mean, variation coefficient, min and max 30-33. Search Depth: mean, variation coefficient, min and max 34-37. log(WBE) value : mean, variation coefficient, min and max Set IV: 38. Number of variable 39. Number of clauses 40. Variable to clauses ratio 41. Number of binary clauses 42. Number of ternary clauses 43. Number of horn clauses 44-47. VCG - Variable nodes degree statistics:   |
|---|

Set IV:

![0_image_1.png](0_image_1.png)

44-47. **VCG - Variable nodes degree statistics**:
48-51. **VCG - Clause nodes degree statistics**: 52-55. **Number of occurrences in Horn** clauses**: mean, variation coefficient, min and max**
56-59. Ratio of positive and negative occurrences of variables**: mean, variation coefficient,**
Since in most cases we do not know whether a given instance is satisfiable or not we need to determine which of the models is the correct one to query for a given instance according to its probability to be satisfiable. Previous work ([26],[4]) suggests that machine learning can be successfully used for **this task** as well. A classifier can be trained to estimate the probability of an instance to be satisfiable. Some classification techniques perform better than **others, but it** seems that for most benchmark families, a classifier with 80% accuracy or more is achievable.

Using supervised machine learning, we train models offline in order to use them for predictions online. For every training example t ∈ T , where T **is the**
training set, we gather the feature vector x = {x1, x2, . . . , xn} **using the features**
presented in section 3.3. Once the raw data is gathered, we perform a feature selection. We repeatedly remove the feature with the smallest standardised coefficient until no improvement is observed based on the standard AIC (Akaike Information Criterion). We then searched and eliminate co-linear features in the chosen set. The reduced feature vector ˆx **is then used to train a classifier and**
several runtime prediction models. The classifier predicts the probability of an instance to be satisfiable and the runtime models predict cpu-runtime. *LMPick* trains one classifier, but two runtime models for each restart strategy s ∈ S (where S is the set of all participating strategies) to the total of 2|S| **models.**
Each training instance is used to train the satisfiability classifier, labeled with its satisfiability class, and |S| **runtime models, for each model it is labeled with**
the appropriate runtime.

As the classifier, we used a Logistic Regression technique. Any classifier that returns probabilities would be suitable. We found Logistic Regression to be a