Structure based SAT dataset for analysing GNN generalisation

• URL: http://arxiv.org/abs/2502.11410v1
• Date: Mon, 17 Feb 2025 03:49:25 GMT
• Title: Structure based SAT dataset for analysing GNN generalisation
• Authors: Yi Fu, Anthony Tompkins, Yang Song, Maurice Pagnucco,
• Abstract summary: We present StructureSAT: a curated dataset, along with code to further generate novel examples. We aim to help explain problematic generalisation in existing GNN SAT solvers by exploiting knowledge of structural graph properties. We conclude with multiple future directions that can help researchers in GNN based SAT solving develop more effective and generalisable SAT solvers.
• Score: 13.394698965947622
• License:
• Abstract: Satisfiability (SAT) solvers based on techniques such as conflict driven clause learning (CDCL) have produced excellent performance on both synthetic and real world industrial problems. While these CDCL solvers only operate on a per-problem basis, graph neural network (GNN) based solvers bring new benefits to the field by allowing practitioners to exploit knowledge gained from solved problems to expedite solving of new SAT problems. However, one specific area that is often studied in the context of CDCL solvers, but largely overlooked in GNN solvers, is the relationship between graph theoretic measure of structure in SAT problems and the generalisation ability of GNN solvers. To bridge the gap between structural graph properties (e.g., modularity, self-similarity) and the generalisability (or lack thereof) of GNN based SAT solvers, we present StructureSAT: a curated dataset, along with code to further generate novel examples, containing a diverse set of SAT problems from well known problem domains. Furthermore, we utilise a novel splitting method that focuses on deconstructing the families into more detailed hierarchies based on their structural properties. With the new dataset, we aim to help explain problematic generalisation in existing GNN SAT solvers by exploiting knowledge of structural graph properties. We conclude with multiple future directions that can help researchers in GNN based SAT solving develop more effective and generalisable SAT solvers.

Related papers

• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  We introduce hardware accelerated algorithms for fast SAT problem generation and a geometric SAT encoding. These advances allow us to scale our approach to SAT problems with thousands of variables and tens of thousands of clauses. A fundamental aspect of our work concerns the very nature of SAT data and its suitability for training machine learning models.
  arXiv  Detail & Related papers  (2024-10-18T22:25:54Z)
• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  We present GraSS, a novel approach for automatic SAT solver selection based on tripartite graph representations of instances. We enrich the graph representation with domain-specific decisions, such as novel node feature design. We demonstrate that this combination of raw representations and domain-specific choices leads to improvements in runtime.
  arXiv  Detail & Related papers  (2024-05-17T18:00:50Z)
• G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks [7.951021955925275]
  Graph neural networks (GNNs) have emerged as a promising approach for solving the Boolean Satisfiability Problem (SAT) G4SATBench is the first benchmark study that establishes a comprehensive evaluation framework for GNN-based SAT solvers. Our results provide valuable insights into the performance of GNN-based SAT solvers.
  arXiv  Detail & Related papers  (2023-09-29T02:50:57Z)
• Using deep learning to construct stochastic local search SAT solvers with performance bounds [0.0]
  We train oracles using Graph Neural Networks and evaluate them on two SLS solvers on random SAT instances of varying difficulty. We find that access to GNN-based oracles significantly boosts the performance of both solvers.
  arXiv  Detail & Related papers  (2023-09-20T16:27:52Z)
• Addressing Variable Dependency in GNN-based SAT Solving [19.38746341365531]
  We propose AsymSAT, a GNN-based architecture which integrates recurrent neural networks to generate dependent predictions for variable assignments. Experiment results show that dependent variable prediction extends the solving capability of the GNN-based method as it improves the number of solved SAT instances on large test sets.
  arXiv  Detail & Related papers  (2023-04-18T05:33:33Z)
• Rethinking Complex Queries on Knowledge Graphs with Neural Link Predictors [58.340159346749964]
  We propose a new neural-symbolic method to support end-to-end learning using complex queries with provable reasoning capability. We develop a new dataset containing ten new types of queries with features that have never been considered. Our method outperforms previous methods significantly in the new dataset and also surpasses previous methods in the existing dataset at the same time.
  arXiv  Detail & Related papers  (2023-04-14T11:35:35Z)
• A Comprehensive Study on Large-Scale Graph Training: Benchmarking and Rethinking [124.21408098724551]
  Large-scale graph training is a notoriously challenging problem for graph neural networks (GNNs) We present a new ensembling training manner, named EnGCN, to address the existing issues. Our proposed method has achieved new state-of-the-art (SOTA) performance on large-scale datasets.
  arXiv  Detail & Related papers  (2022-10-14T03:43:05Z)
• Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
  The paper reviews the recent literature on solving the Boolean satisfiability problem (SAT) with machine learning techniques. We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT.
  arXiv  Detail & Related papers  (2022-03-02T05:14:12Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Evaluating Logical Generalization in Graph Neural Networks [59.70452462833374]
  We study the task of logical generalization using graph neural networks (GNNs) Our benchmark suite, GraphLog, requires that learning algorithms perform rule induction in different synthetic logics. We find that the ability for models to generalize and adapt is strongly determined by the diversity of the logical rules they encounter during training.
  arXiv  Detail & Related papers  (2020-03-14T05:45:55Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.