118
O. Keszocze et al.
and thus the maximization of the number of satisfied clauses—like in the MaxSAT
problem—is the consequent approach. While this measurement was successfully
used in the MCTS-based SAT solver with and without clause learning, this section
presents alternative measurements to adapt to the addition of CDCL to the plain
algorithm. This gives access to more information during the course of the algorithm
that can be exploited in the scoring heuristic.
One common approach when designing SAT solving heuristics is to accredit
more importance to clauses and variables that have a high impact on the clause
learning procedure. For example, the learning rate based heuristic [8] uses such a
measurement to order the variables.
There are different ways to define scoring heuristics that follow this approach,
where the easiest one is the initially introduced heuristic that just uses the number of
satisfied clauses as a measurement (see Eq. (5.4), where sat clauses(f, a) is the set
of satisfied clauses in formula f for the variable assignment a). When this heuristic
is used in the context of the MCTS-based CDCL algorithm, the number of clauses
raises through the course of its execution and thus the fulfillment of learned clauses
gains extra importance by enabling higher scores.
f num (f, a) =
c∈sat clauses(f,a)
1
(5.4)
To explain a second scoring heuristic that follows the described approach we
define the activity act (c) of a clause c as the number of times c occurred during
the resolution process of the clause learning procedure. Equation (5.5) uses this
measurement to benefit the satisfying of clauses with high activity values. We also
tried a similar scoring heuristic that is inspired by the VSIDS variable order heuristic
which benefits variables that occur in newly learned clauses and uses the age of
clauses, i.e., the number of MCTS iterations that occurred since the clauses were
added, to benefit the satisfying of new clauses. This heuristic behaved similarly and
thus is not further considered.
f activity (f, a) =
c∈sat clauses(f,a)
act (c)
(5.5)
Another approach is to not directly optimize the satisfying of as many clauses as
possible but to optimize the collection of useful information. As already concluded
in the analysis of the search trees, a great benefit of the MCTS-based CDCL solver
may be the ability to learn valuable clauses. We now introduce different heuristics
that aim on learning clauses that fulfill different criteria and reward the learning of
“good” clauses. One simple and commonly used criteria for the quality of learned
clauses is their length, which leads to the scoring heuristic as defined in Eq. (5.6),
where length(c) is the number of literals in the newly learned clause c.
f length (Clause) = −length(Clause)
(5.6)
O. Keszocze et al.
and thus the maximization of the number of satisfied clauses—like in the MaxSAT
problem—is the consequent approach. While this measurement was successfully
used in the MCTS-based SAT solver with and without clause learning, this section
presents alternative measurements to adapt to the addition of CDCL to the plain
algorithm. This gives access to more information during the course of the algorithm
that can be exploited in the scoring heuristic.
One common approach when designing SAT solving heuristics is to accredit
more importance to clauses and variables that have a high impact on the clause
learning procedure. For example, the learning rate based heuristic [8] uses such a
measurement to order the variables.
There are different ways to define scoring heuristics that follow this approach,
where the easiest one is the initially introduced heuristic that just uses the number of
satisfied clauses as a measurement (see Eq. (5.4), where sat clauses(f, a) is the set
of satisfied clauses in formula f for the variable assignment a). When this heuristic
is used in the context of the MCTS-based CDCL algorithm, the number of clauses
raises through the course of its execution and thus the fulfillment of learned clauses
gains extra importance by enabling higher scores.
f num (f, a) =
c∈sat clauses(f,a)
1
(5.4)
To explain a second scoring heuristic that follows the described approach we
define the activity act (c) of a clause c as the number of times c occurred during
the resolution process of the clause learning procedure. Equation (5.5) uses this
measurement to benefit the satisfying of clauses with high activity values. We also
tried a similar scoring heuristic that is inspired by the VSIDS variable order heuristic
which benefits variables that occur in newly learned clauses and uses the age of
clauses, i.e., the number of MCTS iterations that occurred since the clauses were
added, to benefit the satisfying of new clauses. This heuristic behaved similarly and
thus is not further considered.
f activity (f, a) =
c∈sat clauses(f,a)
act (c)
(5.5)
Another approach is to not directly optimize the satisfying of as many clauses as
possible but to optimize the collection of useful information. As already concluded
in the analysis of the search trees, a great benefit of the MCTS-based CDCL solver
may be the ability to learn valuable clauses. We now introduce different heuristics
that aim on learning clauses that fulfill different criteria and reward the learning of
“good” clauses. One simple and commonly used criteria for the quality of learned
clauses is their length, which leads to the scoring heuristic as defined in Eq. (5.6),
where length(c) is the number of literals in the newly learned clause c.
f length (Clause) = −length(Clause)
(5.6)