5 Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning
109
We will make heavy use of unit propagation in the proposed SAT solver. We
adopt the process to work on the graph structures used by the solver, see Sects. 5.2.2
and 5.3.
5.2.2 Monte Carlo Tree Search-Based SAT Solving
This section presents the fundamentals of the MCTS-based CDCL solver based on
[13]. Like most implementations of Monte Carlo Tree Search, it is based on the
UCB1 algorithm for multi-armed bandit problems and uses the Upper Confidence
Bounds for Trees (UCT) formula to decide in which direction to expand the search
tree [12].
The main goal of using the UCT formula is to build an asymmetric search tree
that is expanded at the most promising nodes, i.e., at the nodes with the highest
estimated values. As the estimated value can be biased, the use of the UCT formula
also encourages exploring new paths of the search tree.
In this case, every node of the search tree represents a (partial) variable
assignment and is marked with a variable that is unassigned in the node but
becomes assigned in its children. The root node represents the empty assignment,
i.e., an assignment where every variable is unassigned. Each non-root node n has a
reference to its parent node (n.parent) and stores its parent’s variable assignment
(n.assignment). We additionally define that each of this variable assignment must
be an explicit assignment, i.e., an assignment that is not implied via unit propagation. Then, each assignment represents the explicit assignment and all further
assignments that follow via unit propagation. Using this definition, the assignments
on the path from the root node to node n including all additional assignments
that follow by unit propagation define the (partial) variable assignment of n. To
implement this definition, the algorithm will execute all implied assignments after a
variable is explicitly assigned. Thereby, unit propagation is integrated in the search
tree used by the MCTS algorithm. In Sect. 5.3 we will see that by integrating CDCL,
the usage of unit propagation in the search tree must be adapted.
In Fig. 5.1, an exemplary search tree and the partial variable assignments that are
represented by the search tree nodes for f = (¬x 1 ∨ x 2 ) ∧ (x 1 ∨ x 3 ) ∧ (x 4 ∨ x 5 ) are
shown. For example, the variable assignment of node n 3 contains the assignments
x 1 = 0 and x 2 = 0, because they are the explicit assignments on the path from the
root node to n 3 . Additionally it contains x 3 = 1 as the assignment x 1 = 0 and the
clause (x 1 ∨ x 3 ) imply the assignment of x 3 via unit propagation. Note that n 1 and
n 2 have different variables in the example despite being children of the same node.
This can happen as the assignment of x 1 either implies the assignment of x 2 or x 3
and thus, dependent on the value of x 1 , either x 2 or x 3 does not need to be explicitly
implied and cannot be the variable of a search tree node.
To be able to use the UCT formula, each node has an estimated value as well
as a counter for the number of times the algorithm has traversed through it in the
selection phase as explained below. Both of these properties, n.estimatedV alue
109
We will make heavy use of unit propagation in the proposed SAT solver. We
adopt the process to work on the graph structures used by the solver, see Sects. 5.2.2
and 5.3.
5.2.2 Monte Carlo Tree Search-Based SAT Solving
This section presents the fundamentals of the MCTS-based CDCL solver based on
[13]. Like most implementations of Monte Carlo Tree Search, it is based on the
UCB1 algorithm for multi-armed bandit problems and uses the Upper Confidence
Bounds for Trees (UCT) formula to decide in which direction to expand the search
tree [12].
The main goal of using the UCT formula is to build an asymmetric search tree
that is expanded at the most promising nodes, i.e., at the nodes with the highest
estimated values. As the estimated value can be biased, the use of the UCT formula
also encourages exploring new paths of the search tree.
In this case, every node of the search tree represents a (partial) variable
assignment and is marked with a variable that is unassigned in the node but
becomes assigned in its children. The root node represents the empty assignment,
i.e., an assignment where every variable is unassigned. Each non-root node n has a
reference to its parent node (n.parent) and stores its parent’s variable assignment
(n.assignment). We additionally define that each of this variable assignment must
be an explicit assignment, i.e., an assignment that is not implied via unit propagation. Then, each assignment represents the explicit assignment and all further
assignments that follow via unit propagation. Using this definition, the assignments
on the path from the root node to node n including all additional assignments
that follow by unit propagation define the (partial) variable assignment of n. To
implement this definition, the algorithm will execute all implied assignments after a
variable is explicitly assigned. Thereby, unit propagation is integrated in the search
tree used by the MCTS algorithm. In Sect. 5.3 we will see that by integrating CDCL,
the usage of unit propagation in the search tree must be adapted.
In Fig. 5.1, an exemplary search tree and the partial variable assignments that are
represented by the search tree nodes for f = (¬x 1 ∨ x 2 ) ∧ (x 1 ∨ x 3 ) ∧ (x 4 ∨ x 5 ) are
shown. For example, the variable assignment of node n 3 contains the assignments
x 1 = 0 and x 2 = 0, because they are the explicit assignments on the path from the
root node to n 3 . Additionally it contains x 3 = 1 as the assignment x 1 = 0 and the
clause (x 1 ∨ x 3 ) imply the assignment of x 3 via unit propagation. Note that n 1 and
n 2 have different variables in the example despite being children of the same node.
This can happen as the assignment of x 1 either implies the assignment of x 2 or x 3
and thus, dependent on the value of x 1 , either x 2 or x 3 does not need to be explicitly
implied and cannot be the variable of a search tree node.
To be able to use the UCT formula, each node has an estimated value as well
as a counter for the number of times the algorithm has traversed through it in the
selection phase as explained below. Both of these properties, n.estimatedV alue