112
O. Keszocze et al.
new node is marked as conflicting. The variable of the new node is determined
using the variable order heuristic, which is a common part of SAT solvers and
determines the next variable to be assigned. The current implementation uses a
heuristic similar to the Variable State Independent Decaying Sum (VSIDS) order
heuristic [7].
In Fig. 5.2(2), this phase is illustrated by highlighting the new node n that was
added as the new child of the previously selected node n 4 with a diamond shape.
3. To estimate the value of the new node, the simulation phase is executed, which—
starting with the current formula and the assignment of the new node—selects
variables according to the variable order heuristic and assigns them randomly
until a conflict or a satisfying assignment is reached. Again, unit propagation is
executed after each assignment. The value of a so-called scoring heuristic, in
this case the number of satisfied clauses in the resulting formula, is then used
as an initial estimation on the value of the new node. Note that this is only one
possible heuristic to estimate the value of a node and different scoring heuristics
are presented in Sect. 5.4. During the selection phase, a normalized form of this
value is used in the UCT formula. If the simulation finds a satisfying assignment,
the problem is solved and the algorithm can stop.
In Fig. 5.2(3), the simulation phase is shown by illustrating the iterative
variable assignment with a curved arrow and denoting the scoring heuristic value,
that is determined after the simulation, with h(f, a); f and a indicate that the
heuristic value depends on the formula and the variable assignment that is present
after the iterative variable assignment led to a conflict.
4. After a simulation is executed, its result is backpropagated through the search
tree and the estimated value as well as the counter of every node on the path
from the root to the new node is refreshed, i.e., their counters are increased by
one and their estimated values are increased by the estimated value of the new
node. Afterwards, the algorithm continues with Step 1.
In Fig. 5.2(4), the backpropagation phase is indicated by highlighting all nodes
that are traversed through in the backpropagation phase as squares. Note that
these nodes are exactly the node n that was added in the expansion phase, and
all nodes that were traversed in the selection phase. While iterating through these
nodes, the algorithm will refresh the values of all square-shaped nodes as the
figure exemplary shows for node n.
5.3 Conflict-Driven Clause Learning
As already mentioned, the learning and usage of new clauses is a key aspect of
modern SAT solvers. This section introduces the concept of Conflict-Driven Clause
Learning and shows how it can be used in the MCTS-based algorithm.
Afterwards, we will analyze the behavior of the algorithm by visualizing the
search trees that are produced by the MCTS-based CDCL solver.
O. Keszocze et al.
new node is marked as conflicting. The variable of the new node is determined
using the variable order heuristic, which is a common part of SAT solvers and
determines the next variable to be assigned. The current implementation uses a
heuristic similar to the Variable State Independent Decaying Sum (VSIDS) order
heuristic [7].
In Fig. 5.2(2), this phase is illustrated by highlighting the new node n that was
added as the new child of the previously selected node n 4 with a diamond shape.
3. To estimate the value of the new node, the simulation phase is executed, which—
starting with the current formula and the assignment of the new node—selects
variables according to the variable order heuristic and assigns them randomly
until a conflict or a satisfying assignment is reached. Again, unit propagation is
executed after each assignment. The value of a so-called scoring heuristic, in
this case the number of satisfied clauses in the resulting formula, is then used
as an initial estimation on the value of the new node. Note that this is only one
possible heuristic to estimate the value of a node and different scoring heuristics
are presented in Sect. 5.4. During the selection phase, a normalized form of this
value is used in the UCT formula. If the simulation finds a satisfying assignment,
the problem is solved and the algorithm can stop.
In Fig. 5.2(3), the simulation phase is shown by illustrating the iterative
variable assignment with a curved arrow and denoting the scoring heuristic value,
that is determined after the simulation, with h(f, a); f and a indicate that the
heuristic value depends on the formula and the variable assignment that is present
after the iterative variable assignment led to a conflict.
4. After a simulation is executed, its result is backpropagated through the search
tree and the estimated value as well as the counter of every node on the path
from the root to the new node is refreshed, i.e., their counters are increased by
one and their estimated values are increased by the estimated value of the new
node. Afterwards, the algorithm continues with Step 1.
In Fig. 5.2(4), the backpropagation phase is indicated by highlighting all nodes
that are traversed through in the backpropagation phase as squares. Note that
these nodes are exactly the node n that was added in the expansion phase, and
all nodes that were traversed in the selection phase. While iterating through these
nodes, the algorithm will refresh the values of all square-shaped nodes as the
figure exemplary shows for node n.
5.3 Conflict-Driven Clause Learning
As already mentioned, the learning and usage of new clauses is a key aspect of
modern SAT solvers. This section introduces the concept of Conflict-Driven Clause
Learning and shows how it can be used in the MCTS-based algorithm.
Afterwards, we will analyze the behavior of the algorithm by visualizing the
search trees that are produced by the MCTS-based CDCL solver.