5 Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning
119
Another criterion to measure the quality of learned clauses is to benefit the
learning of clauses that enable the algorithm to cut the search space near to its
root. To do so, we define f depth in Eq. (5.7)—where depth(s) is the number of
decisions, i.e., variable assignments that were not caused by unit propagation, that
were executed in a simulation s—that rewards simulations which lead to a conflict
after a low number of decisions and therefore learn clauses that prune the search
tree near to its root.
f depth (Simulation) = −depth(Simulation)
(5.7)
A last scoring heuristic aims to reward simulations that enforce many variable
assignments due to unit propagation. As formulated in Eq. (5.8), where assigned(s)
is the number of variables that were assigned in simulation s, the heuristic gives
those simulations a high value that executed a high proportion of their assignments
due to unit propagation.
f unit (Simulation) =
assigned(Simulation)
depth(Simulation)
(5.8)
Of course, the different heuristics can be combined to follow both approaches
or benefit different criteria. For example, one could reward the occurrence of early
conflicts while satisfying as many clauses as possible (see Eq. (5.9)).
f combined (Simulation) =
f num (Simulation)
f depth (Simulation)
(5.9)
In Sect. 5.6 we will see that the different heuristics succeed in optimizing their
respective criteria.
5.4.2 Probability Heuristics
In Sect. 5.2 the simulations of the MCTS-based CDCL solver were defined to assign
the variables of the formula uniformly at random. While this is an approach that can
be used to solve SAT and is quite standard when using MCTS, it is also common
to use domain specific knowledge—if it is available—to weight the probabilities
in the simulation phase [1]. This section focuses on using knowledge that can be
extracted from the given SAT formula as well as from the learned clauses to weight
the probabilities.
In backtracking-based SAT solvers, the decision to which value to assign the
variables is made using the Phase Selection Heuristic, where one approach is to
assign a variable x i to 1 if the literal x i occurs more often in the formula than ¬x i and
vice versa. We adapted this approach and used probabilities according to Eq. (5.10)
during the simulation phase, where num(x i ) is the number of occurrences of literal
119
Another criterion to measure the quality of learned clauses is to benefit the
learning of clauses that enable the algorithm to cut the search space near to its
root. To do so, we define f depth in Eq. (5.7)—where depth(s) is the number of
decisions, i.e., variable assignments that were not caused by unit propagation, that
were executed in a simulation s—that rewards simulations which lead to a conflict
after a low number of decisions and therefore learn clauses that prune the search
tree near to its root.
f depth (Simulation) = −depth(Simulation)
(5.7)
A last scoring heuristic aims to reward simulations that enforce many variable
assignments due to unit propagation. As formulated in Eq. (5.8), where assigned(s)
is the number of variables that were assigned in simulation s, the heuristic gives
those simulations a high value that executed a high proportion of their assignments
due to unit propagation.
f unit (Simulation) =
assigned(Simulation)
depth(Simulation)
(5.8)
Of course, the different heuristics can be combined to follow both approaches
or benefit different criteria. For example, one could reward the occurrence of early
conflicts while satisfying as many clauses as possible (see Eq. (5.9)).
f combined (Simulation) =
f num (Simulation)
f depth (Simulation)
(5.9)
In Sect. 5.6 we will see that the different heuristics succeed in optimizing their
respective criteria.
5.4.2 Probability Heuristics
In Sect. 5.2 the simulations of the MCTS-based CDCL solver were defined to assign
the variables of the formula uniformly at random. While this is an approach that can
be used to solve SAT and is quite standard when using MCTS, it is also common
to use domain specific knowledge—if it is available—to weight the probabilities
in the simulation phase [1]. This section focuses on using knowledge that can be
extracted from the given SAT formula as well as from the learned clauses to weight
the probabilities.
In backtracking-based SAT solvers, the decision to which value to assign the
variables is made using the Phase Selection Heuristic, where one approach is to
assign a variable x i to 1 if the literal x i occurs more often in the formula than ¬x i and
vice versa. We adapted this approach and used probabilities according to Eq. (5.10)
during the simulation phase, where num(x i ) is the number of occurrences of literal