5 Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning
111
(1)
root
n 2
n 1
n 4
n 3
·
·
·
·
·
·
UCT (n 1 ) ≥ UCT (n 2 )
(2)
root
n 4
·
·
·
n
(3)
root
·
·
·
n
h(f, a)
(4)
root
·
·
·
n
h(f, a)
n.counter = n.counter + 1
n.value = n.value + h(f, a)
Fig. 5.2 Illustration of one iteration through the four MCTS phases. (1) Selection phase: the graph
is traversed starting from the root node along edges to nodes with higher UCT value until node n 4 is
reached (square-shaped nodes). (2) Expansion phase: a new child node representing an assignment
for the variable of the parent node is added (diamond-shaped nodes). After the creation of the node,
unit propagation is performed. (3) Simulation phase: starting from the partial assignment created
by the new node, a simulation is started to compute the value h(f, a) that estimates the value of
the new node. (4) Backpropagation phase: the estimation computed in the last step is propagated
back through the nodes previously traversed to find the expansion point (square-shaped nodes)
in conflicts. If such a node occurs, it is marked as conflicting and removed from
the search tree.
In Fig. 5.2(1), the selection phase is illustrated. The square-shaped nodes are
the nodes that are selected in the selection phase. We see that they form a path
from the root to the fringe of the tree. In the example, n 1 was selected instead of
n 2 because it has the higher UCT value. The selection phase stopped at node n 4 ,
because n 4 only has one of the two possible children.
2. After the expansion point of the tree is determined, the expansion phase of the
algorithm is executed. In this phase a new child of the selected node is added
to the search tree which assigns the variable of the selected node to a value
that has not been tried yet. If that assignment proves to result in a conflict, the
111
(1)
root
n 2
n 1
n 4
n 3
·
·
·
·
·
·
UCT (n 1 ) ≥ UCT (n 2 )
(2)
root
n 4
·
·
·
n
(3)
root
·
·
·
n
h(f, a)
(4)
root
·
·
·
n
h(f, a)
n.counter = n.counter + 1
n.value = n.value + h(f, a)
Fig. 5.2 Illustration of one iteration through the four MCTS phases. (1) Selection phase: the graph
is traversed starting from the root node along edges to nodes with higher UCT value until node n 4 is
reached (square-shaped nodes). (2) Expansion phase: a new child node representing an assignment
for the variable of the parent node is added (diamond-shaped nodes). After the creation of the node,
unit propagation is performed. (3) Simulation phase: starting from the partial assignment created
by the new node, a simulation is started to compute the value h(f, a) that estimates the value of
the new node. (4) Backpropagation phase: the estimation computed in the last step is propagated
back through the nodes previously traversed to find the expansion point (square-shaped nodes)
in conflicts. If such a node occurs, it is marked as conflicting and removed from
the search tree.
In Fig. 5.2(1), the selection phase is illustrated. The square-shaped nodes are
the nodes that are selected in the selection phase. We see that they form a path
from the root to the fringe of the tree. In the example, n 1 was selected instead of
n 2 because it has the higher UCT value. The selection phase stopped at node n 4 ,
because n 4 only has one of the two possible children.
2. After the expansion point of the tree is determined, the expansion phase of the
algorithm is executed. In this phase a new child of the selected node is added
to the search tree which assigns the variable of the selected node to a value
that has not been tried yet. If that assignment proves to result in a conflict, the