5 Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning
123
thereby take advantage of the clauses learned by an MCTS-based algorithm that
uses the previously introduced heuristics. As stated in the previous section, it is
possible to configure the algorithm to optimize different SAT related aspects like the
usage of unit propagation, the learning of short clauses, and the cutting of the search
space near its root. All of these aspects are strongly related to the learned clauses.
This leads to the assumption that different solvers can benefit from importing those
clauses.
Our approach is to generate such clauses by running a portfolio of instances
of the algorithm as a preprocessor for another solver. The MCTS-based solver
instances of the portfolio are configured to encourage the pruning of the search
tree, the learning of short clauses, and the usage of unit propagation by using
the corresponding scoring heuristics that were introduced in Sect. 5.4. For a given
SAT instance, the portfolio is run for a fixed time to learn clauses that benefit
the mentioned aspects. After that, a backtracking-based solver is started on the
given problem—including the previously learned clauses. The hypothesis is that
these clauses improve the performance of the second solver, as they were learned
to encourage the mentioned SAT related aspects. If the preprocessor was able to
actually solve the given problem, the second solver is not started.
For the experiments described in Sect. 5.6, four instances of the MCTS-based
CDCL solver are used to preprocess a backtracking-based CDCL solver. The
instances were configured to use f depth , f unit , f length , respectively, f num as scoring
heuristics. The selection of this four heuristics will be explained in Sect. 5.6. As the
experiments will show, the preprocessing was able to improve the performance of
the backtracking-based algorithm on several benchmark problems.
5.6 Experiments
To verify the existence of the mentioned benefits, we implemented an MCTS-based
SAT solver as specified in Sect. 5.2 as well as all extensions of the algorithm that
were introduced in this chapter and used them to solve the following benchmark
problems.
5.6.1 Benchmark Problems
As already seen in Sects. 5.3.2 and 5.4.3, we considered different instances of the
easily scalable pigeon hole problem. Additionally, we considered different sets of
randomly generated instances. First, we used random satisfiable and unsatisfiable
3-SAT instances from http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html with 250
variables and 1065 clauses. In the following, this problem sets will be called
random SAT and random UNSAT, respectively. Both problem sets consist of
100 different instances.
123
thereby take advantage of the clauses learned by an MCTS-based algorithm that
uses the previously introduced heuristics. As stated in the previous section, it is
possible to configure the algorithm to optimize different SAT related aspects like the
usage of unit propagation, the learning of short clauses, and the cutting of the search
space near its root. All of these aspects are strongly related to the learned clauses.
This leads to the assumption that different solvers can benefit from importing those
clauses.
Our approach is to generate such clauses by running a portfolio of instances
of the algorithm as a preprocessor for another solver. The MCTS-based solver
instances of the portfolio are configured to encourage the pruning of the search
tree, the learning of short clauses, and the usage of unit propagation by using
the corresponding scoring heuristics that were introduced in Sect. 5.4. For a given
SAT instance, the portfolio is run for a fixed time to learn clauses that benefit
the mentioned aspects. After that, a backtracking-based solver is started on the
given problem—including the previously learned clauses. The hypothesis is that
these clauses improve the performance of the second solver, as they were learned
to encourage the mentioned SAT related aspects. If the preprocessor was able to
actually solve the given problem, the second solver is not started.
For the experiments described in Sect. 5.6, four instances of the MCTS-based
CDCL solver are used to preprocess a backtracking-based CDCL solver. The
instances were configured to use f depth , f unit , f length , respectively, f num as scoring
heuristics. The selection of this four heuristics will be explained in Sect. 5.6. As the
experiments will show, the preprocessing was able to improve the performance of
the backtracking-based algorithm on several benchmark problems.
5.6 Experiments
To verify the existence of the mentioned benefits, we implemented an MCTS-based
SAT solver as specified in Sect. 5.2 as well as all extensions of the algorithm that
were introduced in this chapter and used them to solve the following benchmark
problems.
5.6.1 Benchmark Problems
As already seen in Sects. 5.3.2 and 5.4.3, we considered different instances of the
easily scalable pigeon hole problem. Additionally, we considered different sets of
randomly generated instances. First, we used random satisfiable and unsatisfiable
3-SAT instances from http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html with 250
variables and 1065 clauses. In the following, this problem sets will be called
random SAT and random UNSAT, respectively. Both problem sets consist of
100 different instances.