The Impact of Boolean Satisfiability Problem Structure on Graph Neural Network Performance

Boolean Satisfiability (SAT) is a fundamental problem in the study of computational complexity, particularly in understanding the complexity class of NP problems. Over the years, Graph Neural Networks (GNNs) have achieved significant advancements in domains such as graphics and image processing. Given that representing SAT problems as graph structures is a fundamental approach in the SAT community, substantial progress has been made in leveraging GNNs for SAT solving, particularly in the development of GNN-based SAT solvers. Building on these developments, this thesis focuses on analyzing the solving capabilities of GNN-SAT solvers from a graph-theoretic perspective. Specifically, we explore how effectively GNN techniques are used to address SAT problems. We identify potential factors that make certain problems challenging for these GNN-SAT solvers and analyze the challenges through the lens of graph theoretic metrics that are studied in traditionalSAT solving. Although GNN-SAT solving is a relatively nascent field compared to the longstanding history of SAT solving, investigating the performance of GNNs and their interaction with SAT structures provides valuable insights that bring benefits to both the GNN-SAT and traditional SAT communities. The first part of this thesis investigates GNN-SAT solvers on random 3-SAT problems, with a particular focus on the clause-to-variable ratio. Traditional conflict driven clause learning (CDCL) solvers often face greater difficulty on random 3-SAT problems compared to industrial problems, particularly those near a critical clause-to-variable ratio. However, the role of this ratio in the performance of GNN-SAT solvers remains unclear. To investigate how well GNNs perform on problems that are challenging for traditional SAT solvers, we conducted comprehensive experimental studies using state-of-the-art GNN-SAT solvers on random 3-SAT problems with different ratios. We propose several metrics to better characterize the performance of GNN-SAT solvers and provide a detailed analysis of the challenges and efficiencies observed. In the second part of the thesis, we extend our analysis to encompass multiple problem domains and structural properties. While most GNN-SAT studies focus on improving model architectures to enhance overall accuracy, they often overlook the significant role of specific structural properties that exist in different SAT problems. Additionally, many GNN-SAT solvers exhibit poor generalization to novel problem domains, with the underlying causes largely unexplored. To tackle these challenges, we introduce a novel GNN-SAT dataset containing diverse problem domains and graph-theoretic properties, along with innovative data-splitting methods. Through extensive experimentation, we analyze how these factors influence the generalization of GNN-SAT solvers and identify which problems pose greater challenges for GNNs to solve, thereby offering new perspectives and directions for future research.