5 Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning
113
5.3.1 MCTS-Based CDCL Solver
The clause learning usually takes place whenever a conflict occurs and determines
a new clause that formulates the reason for the conflict. The new clause is learned
using an implication graph that is defined by the assigned variables and the clauses
that implied assignments due to unit propagation and added to the overall formula.
For a more detailed explanation on clause learning, see [10]. In the following, the
integration of CDCL into an MCTS-based solver that was first presented in [14] is
introduced.
This approach for an MCTS-based CDCL solver learns a new clause whenever a
simulation leads to a conflict or a conflicting node is detected in the search tree and
to add it to the formula when the algorithm starts a new iteration. The main aspect
to consider is that at each node that is created during the expansion phase of the
algorithm, a number of variables are already assigned to a value. While no node is
created that has a variable assignment that directly causes a conflict, the learning
of additional clauses can lead to the existence of nodes that have assignments
which lead to a conflict in one of the learned clauses. As those nodes do not lead
to a solution, they can be pruned from the search tree. Therefore we modify the
algorithm to check the nodes that are traversed through during the selection phase
for such conflicts.
The left part of Fig. 5.3 shows a situation where the algorithm is determining
the successor of the diamond-shaped node formed during the selection phase and
notices that assigning the current variable x k to 0 would lead to a conflict such that
the dashed node is conflicting.
The figure shows that the algorithm only has the choice to select the assignment
x k = 1 because the alternative would lead into a conflict. At this point, there are two
possible reasons for this conflict. First, the variable assignment could directly lead
x k
x k+1
x k+1
x k+2
x k+2
x k = 1
x k = 0
x k+1 = 1
x k+1 = 0
x k+1
x k+2
x k+2
x k+1 = 1
x k+1 = 0
Fig. 5.3 Encountering (left) and resolving (right) a conflicting node during the selection phase
113
5.3.1 MCTS-Based CDCL Solver
The clause learning usually takes place whenever a conflict occurs and determines
a new clause that formulates the reason for the conflict. The new clause is learned
using an implication graph that is defined by the assigned variables and the clauses
that implied assignments due to unit propagation and added to the overall formula.
For a more detailed explanation on clause learning, see [10]. In the following, the
integration of CDCL into an MCTS-based solver that was first presented in [14] is
introduced.
This approach for an MCTS-based CDCL solver learns a new clause whenever a
simulation leads to a conflict or a conflicting node is detected in the search tree and
to add it to the formula when the algorithm starts a new iteration. The main aspect
to consider is that at each node that is created during the expansion phase of the
algorithm, a number of variables are already assigned to a value. While no node is
created that has a variable assignment that directly causes a conflict, the learning
of additional clauses can lead to the existence of nodes that have assignments
which lead to a conflict in one of the learned clauses. As those nodes do not lead
to a solution, they can be pruned from the search tree. Therefore we modify the
algorithm to check the nodes that are traversed through during the selection phase
for such conflicts.
The left part of Fig. 5.3 shows a situation where the algorithm is determining
the successor of the diamond-shaped node formed during the selection phase and
notices that assigning the current variable x k to 0 would lead to a conflict such that
the dashed node is conflicting.
The figure shows that the algorithm only has the choice to select the assignment
x k = 1 because the alternative would lead into a conflict. At this point, there are two
possible reasons for this conflict. First, the variable assignment could directly lead
x k
x k+1
x k+1
x k+2
x k+2
x k = 1
x k = 0
x k+1 = 1
x k+1 = 0
x k+1
x k+2
x k+2
x k+1 = 1
x k+1 = 0
Fig. 5.3 Encountering (left) and resolving (right) a conflicting node during the selection phase