5 Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning
131
Table 5.1 Run time in milliseconds for solving different problems using Sat4j and the preprocessed Sat4j
Benchmark
w/o preproc.
w/ preprocessing
Improvement
Pigeon 9
90,172
71,674 (1 s)
1.26
Pigeon 10
335,897
367,237 (1 s)
0.91
Pigeon 11
6,380,764
6,270,727 (1 s)
1.02
Random SAT
7544
5363 (250 ms)
1.40
Random UNSAT
10,248
10,287 (250 ms)
0.99
Random set 1
31,456
16,606 (2 s)
1.89
Random set 2
242,268
190,592 (2 s)
1.27
Random set 3
527,738
478,709 (2 s)
1.10
qquery3l42lambda
21,042
19,274 (10 s)
1.09
gss-13-s100
92,078
65,341 (10 s)
1.40
gss-14-s100
122,405
152,834 (10 s)
0.8
gss-16-s100
768,782
301,306 (10 s)
2.55
mod3block3vars9gates r estr
115,320
130,358 (10 s)
0.88
mod34vars6gates
410,409
300,104 (10 s)
1.36
AProVE07-09
686,304
675,980 (10 s)
1.02
AProVE07-08
1,512,648
1,365,943 (10 s)
1.11
The running time for the preprocessed Sat4j includes the running time of the preprocessor, which
is displayed in parentheses
All in all the results of this experiments indicate that the usage of MCTSbased CDCL solvers as preprocessors can improve the performance of established
backtracking-based solvers.
5.7 Conclusion and Outlook
In this chapter we analyzed the behavior of a Monte Carlo Tree Search-based
Conflict-Driven Clause Learning SAT solver and showed that the usage of CDCL is
beneficial for the SAT solving process. The improvement is achieved by pruning the
search tree and directing the simulations in better directions via unit propagation on
the learned clauses.
The visualization of the search trees indicates the importance of an accurate value
estimation of the tree nodes as it enables the algorithm to ignore large parts of
the search space. Additionally they illustrate the ability of the algorithm to learn
valuable clauses.
To further take advantage of that ability, different scoring heuristics were
introduced that can be used to actively search for valuable clauses. Our experiments
showed that it is indeed possible to use those heuristics to configure the algorithm
to optimize different SAT related aspects—like the learning of short clauses or the
early occurrence of conflicts.
131
Table 5.1 Run time in milliseconds for solving different problems using Sat4j and the preprocessed Sat4j
Benchmark
w/o preproc.
w/ preprocessing
Improvement
Pigeon 9
90,172
71,674 (1 s)
1.26
Pigeon 10
335,897
367,237 (1 s)
0.91
Pigeon 11
6,380,764
6,270,727 (1 s)
1.02
Random SAT
7544
5363 (250 ms)
1.40
Random UNSAT
10,248
10,287 (250 ms)
0.99
Random set 1
31,456
16,606 (2 s)
1.89
Random set 2
242,268
190,592 (2 s)
1.27
Random set 3
527,738
478,709 (2 s)
1.10
qquery3l42lambda
21,042
19,274 (10 s)
1.09
gss-13-s100
92,078
65,341 (10 s)
1.40
gss-14-s100
122,405
152,834 (10 s)
0.8
gss-16-s100
768,782
301,306 (10 s)
2.55
mod3block3vars9gates r estr
115,320
130,358 (10 s)
0.88
mod34vars6gates
410,409
300,104 (10 s)
1.36
AProVE07-09
686,304
675,980 (10 s)
1.02
AProVE07-08
1,512,648
1,365,943 (10 s)
1.11
The running time for the preprocessed Sat4j includes the running time of the preprocessor, which
is displayed in parentheses
All in all the results of this experiments indicate that the usage of MCTSbased CDCL solvers as preprocessors can improve the performance of established
backtracking-based solvers.
5.7 Conclusion and Outlook
In this chapter we analyzed the behavior of a Monte Carlo Tree Search-based
Conflict-Driven Clause Learning SAT solver and showed that the usage of CDCL is
beneficial for the SAT solving process. The improvement is achieved by pruning the
search tree and directing the simulations in better directions via unit propagation on
the learned clauses.
The visualization of the search trees indicates the importance of an accurate value
estimation of the tree nodes as it enables the algorithm to ignore large parts of
the search space. Additionally they illustrate the ability of the algorithm to learn
valuable clauses.
To further take advantage of that ability, different scoring heuristics were
introduced that can be used to actively search for valuable clauses. Our experiments
showed that it is indeed possible to use those heuristics to configure the algorithm
to optimize different SAT related aspects—like the learning of short clauses or the
early occurrence of conflicts.