1. Preliminaries & Subject Area Research 5
1.1. Introduction 5
1.2. Boolean Satisfiability Problem & SAT Solvers 5
1.3. Machine Learning for SAT 7
1.3.1. Portfolio Algorithms 7
1.3.2. Graph Neural Networks: Architectures and Implementations 7
1.4. Graph-Q-SAT: The Original Approach 11
1.4.1. Idea and Implementation Details 11
1.4.2. Experimental Results 13
1.5. Research Objectives 14
2. Graph-Q-SATd—+: Re-envisioning a Popular Approach 15
2.1. Reproducing the Original Results 15
2.2. Direct Implementation Into a SAT Solver 16
2.3. Experimental Results & Improvements 18
2.4. Discussion 21
3. Conclusion 22
References
The Boolean satisfiability problem (SAT) is a paramount problem of computer science that impacts various areas of knowledge, including but not limited to software
and hardware verification, circuit design, automatic proof checking and cryptography. This is
an NP-complete problem [9], which means that any problem from the NP class can be reduced
to it in polynomial time, and the problem itself is assumed to be computationally hard and
not having a straightforward algorithm that would solve it in a reasonable amount of time in
general case. In spite of this, conflict-driven clause learning solving algorithms achieve very
prominent results in reducing the time required to solve an instance of the SAT problem by
employing various heuristics.The branching heuristic that decides which variable to assign a
value during each iteration of the exhaustive search is one of the crucial ones.
In the Graph-Q-SAT [17] paper, a team of NVIDIA and the Oxford university researchers
proposed to improve the widely used Variable State Independent Decaying Sum (VSIDS) heuristic [18] by using a deep neural network, particularly a graph neural network, to “communicate”
with the MiniSat solver via a GYM [7] environment (implemented in Python) and predict the
next variable to branch on during each step based on the current state of the problem. In many
cases this approach decreases the number of branching decisions required to solve an instance
of the SAT problem as compared to the original backbone solver MiniSat 2.2 [10]. However,
as stated by the researchers themselves, it did not show any substantial results in improving
wall-clock time, which is a key factor in industrial-scale settings.
In the proposed approach named Graph-Q-SAT++ the implementation of Graph-Q-SAT is
studied and several changes are suggested in order to improve the results achieved in the original
research. First of all, the deep neural network is embedded in the MiniSat 2.2 solver itself using
the C++ PyTorch API and, secondly, experiments with the architecture of the network are
conducted in order to shave off some computational time while preserving the quality of its
predictions.
In the present thesis, the domain of SAT solving was explored, and various machine learning
approaches to improving the performance of SAT solvers were studied and reviewed, focusing on
those which utilize graph neural networks, since they were showing very promising results at the
moment of writing. Out of all of the studied heuristics a popular and straightforward approach
called Graph-Q-SAT was picked. The approach and its implementation were thoroughly studied
and the reproduction of results of the original work of interest was carried out. Graph-Q-SAT
was then re-envisioned as an algorithm embedded into one of the standard solvers, MiniSat,
instead of being a separate algorithm which communicates with the solver re-implemented as
a reinforcement learning environment. The code of Graph-Q-SAT was modified to make it
possible for the algorithm to save the trained graph neural network, which predicts the next
beneficial decision for the solver, in TorchScript format, a format embeddable into C++ code,
and the MiniSat solver was modified to query this network.
The experiments, in which MiniSat, Graph-Q-SAT and Graph-Q-SAT++ are compared in
terms of wall-clock time, were conducted. They show that the latter approach is more efficient in
this setting. In particular, we observe that Graph-Q-SAT++ outperforms Kissat and shows an
average increase in speed of almost 4 times over Graph-Q-SAT on datasets containing problems
from the Uniform Random-3-SAT family.
Moreover, additional experiments were conducted which show the extent to which our modification improves the performance of the SAT solver.
In the future, the proposed approach can be released as an open source tool with readily
available models pre-trained on larger formulae sets, which could be embedded into various
SAT solvers (since a huge portion of them is written in C++), including the state-of-the-art
ones, in order to further improve their performance on certain pools of SAT problems.
