110
O. Keszocze et al.
root(x1)
n2(x3)
n1(x2)
n4(x4)
n3(x4)
Node Represented partial assignment
root
-
n1
x1 = 0, x3 = 1
n2
x1 = 1, x2 = 1
n3
x1 = 0, x3 = 1, x2 = 0
n4
x1 = 0, x3 = 1, x2 = 1
Fig. 5.1 Excerpt of a possible search tree and partial variable assignments of the search tree nodes
for the formula f = (¬x 1 ∨ x 2 ) ∧ (x 1 ∨ x 3 ) ∧ (x 4 ∨ x 5 ). The variable of each node is notated in
parenthesis behind the node name and we assume that the left child assigns the parent’s variable to
zero, while the right child assigns it to one
and n.counter, are used to calculate the UCT value of a node n, where the UCT
value of n consists of the exploration value as shown in Eq. (5.1) and the exploitation
value as shown in Eq. (5.2).
UCT Explore (n) =
2 ln n.parent.counter
n.counter
(5.1)
UCT Exploit (n) =
node.estimatedV alue
node.counter
(5.2)
The UCT value of n can be calculated by adding up both values as shown in
Eq. (5.3):
UCT (n) = UCT Exploit (n) + C · UCT Explore (n)
(5.3)
The factor C in Eq. (5.3) is the so-called exploration constant that can be used
to weight the summands. Note that the algorithm never calculates the UCT value of
the root node and thus n.parent.counter can safely be used as stated in Eq. (5.1).
Given a CNF formula, the UCT based solver executes iterations until a satisfying
assignment is found or the formula is proved to be unsatisfiable. In each iteration,
one node is added to the search tree, its value is estimated, and the values of the trees
nodes are refreshed. During the iteration, an instance of the given formula is kept
up to date by executing encountered assignments and—after each assignment—unit
propagation on this formula. The algorithm iterates through four phases—selection,
expansion, simulation, and backpropagation—until a satisfying assignment is found
or the root node is marked as conflicting and thus the formula is unsatisfiable. The
four phases are explained in the following:
1. The selection phase of the algorithm is used to decide at which point to expand
the search tree. To do so, the algorithm starts from the root node and traverses
through the tree until one of its leaves, or a not fully expanded node, is reached.
During this process the next node to be traversed through is always the child of
the current node with the highest UCT value. A node that is encountered during
this phase can have a conflicting assignment if all of its children proved to result
O. Keszocze et al.
root(x1)
n2(x3)
n1(x2)
n4(x4)
n3(x4)
Node Represented partial assignment
root
-
n1
x1 = 0, x3 = 1
n2
x1 = 1, x2 = 1
n3
x1 = 0, x3 = 1, x2 = 0
n4
x1 = 0, x3 = 1, x2 = 1
Fig. 5.1 Excerpt of a possible search tree and partial variable assignments of the search tree nodes
for the formula f = (¬x 1 ∨ x 2 ) ∧ (x 1 ∨ x 3 ) ∧ (x 4 ∨ x 5 ). The variable of each node is notated in
parenthesis behind the node name and we assume that the left child assigns the parent’s variable to
zero, while the right child assigns it to one
and n.counter, are used to calculate the UCT value of a node n, where the UCT
value of n consists of the exploration value as shown in Eq. (5.1) and the exploitation
value as shown in Eq. (5.2).
UCT Explore (n) =
2 ln n.parent.counter
n.counter
(5.1)
UCT Exploit (n) =
node.estimatedV alue
node.counter
(5.2)
The UCT value of n can be calculated by adding up both values as shown in
Eq. (5.3):
UCT (n) = UCT Exploit (n) + C · UCT Explore (n)
(5.3)
The factor C in Eq. (5.3) is the so-called exploration constant that can be used
to weight the summands. Note that the algorithm never calculates the UCT value of
the root node and thus n.parent.counter can safely be used as stated in Eq. (5.1).
Given a CNF formula, the UCT based solver executes iterations until a satisfying
assignment is found or the formula is proved to be unsatisfiable. In each iteration,
one node is added to the search tree, its value is estimated, and the values of the trees
nodes are refreshed. During the iteration, an instance of the given formula is kept
up to date by executing encountered assignments and—after each assignment—unit
propagation on this formula. The algorithm iterates through four phases—selection,
expansion, simulation, and backpropagation—until a satisfying assignment is found
or the root node is marked as conflicting and thus the formula is unsatisfiable. The
four phases are explained in the following:
1. The selection phase of the algorithm is used to decide at which point to expand
the search tree. To do so, the algorithm starts from the root node and traverses
through the tree until one of its leaves, or a not fully expanded node, is reached.
During this process the next node to be traversed through is always the child of
the current node with the highest UCT value. A node that is encountered during
this phase can have a conflicting assignment if all of its children proved to result