used machine learning to tune empirical hardness models (Leyton-Brown, Nudelman, and Shoham 2002). Learning mostly used static features of the problem instance. The only exception was a group of features generated by probing the search space using DPLL and stochastic search. Their method gives a probabilistic estimate of runtime and not, as here, an estimate for a specific run. Their search cost estimates were used within a portfolio based SAT solver SATzilla (Xu et al. 2007).

Finally, an online machine learning method has been developed to speed up a QBF solver
(Samulowitz and Memisevic 2007). Having solved different datasets of problems, a multinomial logistic regression model was built to classify each instance to its best heuristic.

This model was used to suggest the best heuristic for new problem instances. Such a technique could also be used dynamically to change the heuristic used by a solver.

## Weighted Backtrack Estimator

We begin by describing how the existing WBE algorithm
(Kilby et al. 2006) can be adapted to cope with modern SAT
solvers. At every point in search, the WBE algorithm estimates the search tree size as:

$$\frac{\sum_{d\in D}p r o b(d)(2^{d+1}-1)}{\sum_{d\in D}p r o b(d)}$$
$$(1)$$

Where **prob**(d) = 2−dis related to the probability that we visit such a depth using random probing, and D is the multiset of branches lengths visited. By storing the numerator and denominator, this estimate can be calculated in constant time and space at every backtrack. The resulting estimate is unbiased assuming we have a proper binary search tree.

Since WBE generate a tree size estimation it is significantly more effective for unsatisfiable instances. Moreover, WBE is not directly applicable to modern SAT solvers as they perform (conflict driven) backjumping. By backjumping over nodes, we no longer have a proper binary tree. A
second problem is that on backtracking to a decision level, modern SAT solvers are not forced to branch on the negated decision. We can instead branch on a new variable. Another challenge for WBE is restarts. At every restart point, a new tree is generated. Any method to estimate search cost must take these factors into account.

In order to construct a proper binary search tree representing the branching decisions of a SAT solver, and to compensate for backjumping, we observe the two atomic operations performed during search.

- *assign(v,b):* when v is a variable and b is a Boolean value.

This action assigns the variable v the value b. This assignment will be kept in the next level of the search stack.

After every assignment a unit propagation process takes place. The values that are assigned in this process are also considered to be assigned in this decision level.

- *backtrack(d):* backtrack back to decision level d. Unassign all variables assigned in any decision level equal to or greater than d. Any backtrack is also followed by unit propagation.

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

Figure 1: Conversion of a DPLL trace into a binary tree. In 1(a), **stack** is the assignment stack before the action, **action** is the action taken, and **conflict** denotes if this generates a conflict. In 1(b), conflicts are numbered, and edges labelled with assignments. Since decisions v2 and v5 are backjumped over, they do not appear as labels.

A binary tree can be generated as follows: we branch left from a node for every **assign** operation, and we branch right when we **backtrack** back to the node, even if the next assignment is at the same decision level. If we backjump over node n, this node is removed. Note that node depths in the binary tree no longer correspond with decision levels, Figure1 shows an example of this technique. In Figure 1(a), we see a list of h**stack, action, conflict**i tuples, representing a sequence of actions and the resulted assignment stack. The tree in Figure 1(b) is the explicit proper binary tree corresponding to the same sequence of steps. Note that in both cases there are 4 conflicts, but note that the node depths change.

## Wbe For Conflict Driven Search

Every time a backjump occurs, WBE needs to update the depths of leaves beneath this backjump. This is not possible if we just store an accumulated sum for the denominator and numerator in the WBE estimation. Fortunately, the WBE estimation can be computed by observing two different parameters which are easy to adjust after backjumping. The first, C, is a simple counter of the nodes encountered so far in an in-order tree search (counting a node only after backtracking from its left subtree). The second, P, is the partial size of the tree explored assuming it is a complete binary tree. At any point in search, the WBE estimate can be generated by