108
O. Keszocze et al.
One contribution of this chapter is to visualize the search trees that are produced
by MCTS-based algorithms and use them to analyze and illustrate the behavior of
different variants of the algorithm. Based on the analysis this chapter will introduce
different SAT specific MCTS heuristics that focus on learning “good” clauses that
benefit different SAT solver features. The impact of this heuristics is illustrated by
benchmarks.
It turns out that, even with the use of additional features like CDCL, the MCTSbased approach cannot compete with modern state-of-the-art SAT solvers without
further improvements and engineering. Therefore, the main contribution of this
chapter is to exploit the ability of the MCTS-based CDCL algorithm to learn “good”
clauses. The presented method is used as a preprocessor for a backtracking-based
solver. We will show that the performance of the backtracking-based solver can be
improved in many cases.
5.2 Monte Carlo Tree Search-Based SAT Solving
This section presents the fundamentals of the MCTS-based CDCL solver. After a
brief introduction to the SAT problem, the basis for the SAT solver proposed in this
work is presented: an MCTS-based SAT solving algorithm similar to UCTSAT by
Previti et al. [13].
5.2.1 Problem Formulation and Unit Propagation
The SAT problem is to decide whether there exists a variable assignment for a given
Boolean formula such that the formula evaluates to true. Almost all state-of-the-art
SAT solvers accept Boolean formulas in Conjunctive Normal Form (CNF) that is a
conjunction of clauses.
The CNF
(x ∨ ¯
y) ∧ z ∧ ( ¯
x ∨ ¯
z)
consists of three clauses C 1 = x ∨ ¯
y, C 2 = z, and C 3 = ¯
x ∨ ¯
z. It is satisfiable with
the assignment x = 0, y = 0, and z = 1.
One key technique in SAT solving is unit propagation, see, e.g. [2]. A clause C is
called unit if and only if it consists of a single literal only. The merit of unit clauses
is that they enforce the assignment of their unit literal as it must be assigned to truth
value 1 to satisfy the clause. In the above CNF, C 2 is a unit clause enforcing z = 1 or
¯
z = 0, respectively. This reduces C 3 to the unit clause ¯
x. The forced assignment of
x = 0, again, reduces the next clause, C 1 , to become unit. The process of repeatedly
checking for and assigning unit clauses is called unit propagation.
O. Keszocze et al.
One contribution of this chapter is to visualize the search trees that are produced
by MCTS-based algorithms and use them to analyze and illustrate the behavior of
different variants of the algorithm. Based on the analysis this chapter will introduce
different SAT specific MCTS heuristics that focus on learning “good” clauses that
benefit different SAT solver features. The impact of this heuristics is illustrated by
benchmarks.
It turns out that, even with the use of additional features like CDCL, the MCTSbased approach cannot compete with modern state-of-the-art SAT solvers without
further improvements and engineering. Therefore, the main contribution of this
chapter is to exploit the ability of the MCTS-based CDCL algorithm to learn “good”
clauses. The presented method is used as a preprocessor for a backtracking-based
solver. We will show that the performance of the backtracking-based solver can be
improved in many cases.
5.2 Monte Carlo Tree Search-Based SAT Solving
This section presents the fundamentals of the MCTS-based CDCL solver. After a
brief introduction to the SAT problem, the basis for the SAT solver proposed in this
work is presented: an MCTS-based SAT solving algorithm similar to UCTSAT by
Previti et al. [13].
5.2.1 Problem Formulation and Unit Propagation
The SAT problem is to decide whether there exists a variable assignment for a given
Boolean formula such that the formula evaluates to true. Almost all state-of-the-art
SAT solvers accept Boolean formulas in Conjunctive Normal Form (CNF) that is a
conjunction of clauses.
The CNF
(x ∨ ¯
y) ∧ z ∧ ( ¯
x ∨ ¯
z)
consists of three clauses C 1 = x ∨ ¯
y, C 2 = z, and C 3 = ¯
x ∨ ¯
z. It is satisfiable with
the assignment x = 0, y = 0, and z = 1.
One key technique in SAT solving is unit propagation, see, e.g. [2]. A clause C is
called unit if and only if it consists of a single literal only. The merit of unit clauses
is that they enforce the assignment of their unit literal as it must be assigned to truth
value 1 to satisfy the clause. In the above CNF, C 2 is a unit clause enforcing z = 1 or
¯
z = 0, respectively. This reduces C 3 to the unit clause ¯
x. The forced assignment of
x = 0, again, reduces the next clause, C 1 , to become unit. The process of repeatedly
checking for and assigning unit clauses is called unit propagation.