114
O. Keszocze et al.
to the conflict and second, the unit propagation after the assignment could lead to
the conflict.
If the variable assignment would directly lead into a conflict, it would mean
that a clause C must exist which is unit in the variable assignment of the current
node and has the unit literal x k . This is an important aspect as the algorithm was
defined to execute unit propagation after each variable assignment, so after assigning
the precursor variables of x k , the unit propagation must have already led to the
assignment x k = 1. Because of that, not only the dashed node becomes unnecessary
but also the diamond-shaped one as its variable must already have been assigned,
so the algorithm can prune both nodes—including the child nodes of the conflicting
node—and continue in the state shown in the right part of Fig. 5.3.
To detect this case, the algorithm only has to check if the variable of the current
node has already been assigned due to unit propagation. If, on the other hand, the
unit propagation after the assignment x k = 0 leads to the conflict, the diamondshaped node does not become redundant as its assignment was not already executed
due to unit propagation in the previous nodes. In this case, the dashed node can
still be pruned, but the diamond-shaped one needs to be retained. This case can
be detected by checking whether a variable assignment led to a conflict during
the selection phase. Note that if this second case occurs, a new conflict was found
and thus a new clause is learned. Because this newly learned clause could lead to
previous visited nodes becoming conflicting, we adjust the algorithm to directly
execute the backpropagation phase and afterwards start a new iteration whenever
this case occurs. The backpropagation phase is modified to take into account that
parts of the search tree can never be reached again. Let v be a node that is removed
from the search tree because it was detected to be conflicting. Another aspect to
consider is that for each iteration i of the algorithm that traversed through v, the
estimated value of i was backpropagated from v to the root node whereupon also
the counter of all nodes on the path from v to the root was increased. Therefore
iterations after the pruning of v would make decisions in the selection phase based
on simulations in parts of the search space that can never be reached again. To
prevent this, we modify the backpropagation phase to subtract the estimated value
and counter of node v from the estimated value and counter of all nodes on the path
from the root to v.
Figure 5.4 illustrates the modification by showing that if a search tree node n p —
and consequently all of it successors, as highlighted by the dotted nodes in the
figure—is pruned, the values of all nodes on the path from the direct predecessor
of n p to the root nodes are refreshed. The affected nodes are indicated by squareshaped nodes. The refreshment of the values is exemplary shown for node n.
Note that starting a new iteration from the root node of the tree instead of
executing a backjump comes with an advantage of being able to choose the most
promising point (according to the UCT formula) to continue the solving process. A
backjump simply continues at the last node that is known to be conflict free.
O. Keszocze et al.
to the conflict and second, the unit propagation after the assignment could lead to
the conflict.
If the variable assignment would directly lead into a conflict, it would mean
that a clause C must exist which is unit in the variable assignment of the current
node and has the unit literal x k . This is an important aspect as the algorithm was
defined to execute unit propagation after each variable assignment, so after assigning
the precursor variables of x k , the unit propagation must have already led to the
assignment x k = 1. Because of that, not only the dashed node becomes unnecessary
but also the diamond-shaped one as its variable must already have been assigned,
so the algorithm can prune both nodes—including the child nodes of the conflicting
node—and continue in the state shown in the right part of Fig. 5.3.
To detect this case, the algorithm only has to check if the variable of the current
node has already been assigned due to unit propagation. If, on the other hand, the
unit propagation after the assignment x k = 0 leads to the conflict, the diamondshaped node does not become redundant as its assignment was not already executed
due to unit propagation in the previous nodes. In this case, the dashed node can
still be pruned, but the diamond-shaped one needs to be retained. This case can
be detected by checking whether a variable assignment led to a conflict during
the selection phase. Note that if this second case occurs, a new conflict was found
and thus a new clause is learned. Because this newly learned clause could lead to
previous visited nodes becoming conflicting, we adjust the algorithm to directly
execute the backpropagation phase and afterwards start a new iteration whenever
this case occurs. The backpropagation phase is modified to take into account that
parts of the search tree can never be reached again. Let v be a node that is removed
from the search tree because it was detected to be conflicting. Another aspect to
consider is that for each iteration i of the algorithm that traversed through v, the
estimated value of i was backpropagated from v to the root node whereupon also
the counter of all nodes on the path from v to the root was increased. Therefore
iterations after the pruning of v would make decisions in the selection phase based
on simulations in parts of the search space that can never be reached again. To
prevent this, we modify the backpropagation phase to subtract the estimated value
and counter of node v from the estimated value and counter of all nodes on the path
from the root to v.
Figure 5.4 illustrates the modification by showing that if a search tree node n p —
and consequently all of it successors, as highlighted by the dotted nodes in the
figure—is pruned, the values of all nodes on the path from the direct predecessor
of n p to the root nodes are refreshed. The affected nodes are indicated by squareshaped nodes. The refreshment of the values is exemplary shown for node n.
Note that starting a new iteration from the root node of the tree instead of
executing a backjump comes with an advantage of being able to choose the most
promising point (according to the UCT formula) to continue the solving process. A
backjump simply continues at the last node that is known to be conflict free.