MILP-SAT-GNN: Yet Another Neural SAT Solver

• URL: http://arxiv.org/abs/2507.01825v1
• Date: Wed, 02 Jul 2025 15:39:45 GMT
• Title: MILP-SAT-GNN: Yet Another Neural SAT Solver
• Authors: Franco Alberto Cardillo, Hamza Khyari, Umberto Straccia,
• Abstract summary: We propose a novel method that enables Graph Neural Networks (GNNs) to solve SAT problems by leveraging a technique developed for applying GNNs to Mixed Linear Programming (MILP)<n>Specifically, k-CNF formulae are mapped into MILP problems, which are then encoded as weighted bipartite graphs and fed into a GNN for training and testing.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We proposes a novel method that enables Graph Neural Networks (GNNs) to solve SAT problems by leveraging a technique developed for applying GNNs to Mixed Integer Linear Programming (MILP). Specifically, k-CNF formulae are mapped into MILP problems, which are then encoded as weighted bipartite graphs and subsequently fed into a GNN for training and testing. From a theoretical perspective: (i) we establish permutation and equivalence invariance results, demonstrating that the method produces outputs that are stable under reordering of clauses and variables; (ii) we identify a theoretical limitation, showing that for a class of formulae called foldable formulae, standard GNNs cannot always distinguish satisfiable from unsatisfiable instances; (iii) we prove a universal approximation theorem, establishing that with Random Node Initialization (RNI), the method can approximate SAT solving to arbitrary precision on finite datasets, that is, the GNN becomes approximately sound and complete on such datasets. Furthermore, we show that for unfoldable formulae, the same approximation guarantee can be achieved without the need for RNI. Finally, we conduct an experimental evaluation of our approach, which show that, despite the simplicity of the neural architecture, the method achieves promising results.

Related papers

• Scalable Graph Compressed Convolutions [68.85227170390864]
  We propose a differentiable method that applies permutations to calibrate input graphs for Euclidean convolution. Based on the graph calibration, we propose the Compressed Convolution Network (CoCN) for hierarchical graph representation learning.
  arXiv  Detail & Related papers  (2024-07-26T03:14:13Z)
• Learning with Norm Constrained, Over-parameterized, Two-layer Neural Networks [54.177130905659155]
  Recent studies show that a reproducing kernel Hilbert space (RKHS) is not a suitable space to model functions by neural networks. In this paper, we study a suitable function space for over- parameterized two-layer neural networks with bounded norms.
  arXiv  Detail & Related papers  (2024-04-29T15:04:07Z)
• CoRMF: Criticality-Ordered Recurrent Mean Field Ising Solver [4.364088891019632]
  We propose an RNN-based efficient Ising model solver, the Criticality-ordered Recurrent Mean Field (CoRMF) By leveraging the approximated tree structure of the underlying Ising graph, the newly-obtained criticality order enables the unification between variational mean-field and RNN. CoRFM solves the Ising problems in a self-train fashion without data/evidence, and the inference tasks can be executed by directly sampling from RNN.
  arXiv  Detail & Related papers  (2024-03-05T16:55:06Z)
• On Neural Networks as Infinite Tree-Structured Probabilistic Graphical Models [44.676210493587256]
  We propose an innovative solution by constructing infinite tree-structured PGMs that correspond exactly to neural networks.<n>Our research reveals that DNNs, during forward propagation, indeed perform approximations of PGM inference that are precise in this alternative PGM structure.
  arXiv  Detail & Related papers  (2023-05-27T21:32:28Z)
• AskewSGD : An Annealed interval-constrained Optimisation method to train Quantized Neural Networks [12.229154524476405]
  We develop a new algorithm, Annealed Skewed SGD - AskewSGD - for training deep neural networks (DNNs) with quantized weights. Unlike algorithms with active sets and feasible directions, AskewSGD avoids projections or optimization under the entire feasible set. Experimental results show that the AskewSGD algorithm performs better than or on par with state of the art methods in classical benchmarks.
  arXiv  Detail & Related papers  (2022-11-07T18:13:44Z)
• On Representing Linear Programs by Graph Neural Networks [30.998508318941017]
  Graph neural network (GNN) is considered a suitable machine learning model for optimization problems. This paper establishes the theoretical foundation of applying GNNs to solving linear program (LP) problems. We show that properly built GNNs can reliably predict feasibility, boundedness, and an optimal solution for each LP in a broad class.
  arXiv  Detail & Related papers  (2022-09-25T18:27:33Z)
• VQ-GNN: A Universal Framework to Scale up Graph Neural Networks using Vector Quantization [70.8567058758375]
  VQ-GNN is a universal framework to scale up any convolution-based GNNs using Vector Quantization (VQ) without compromising the performance. Our framework avoids the "neighbor explosion" problem of GNNs using quantized representations combined with a low-rank version of the graph convolution matrix.
  arXiv  Detail & Related papers  (2021-10-27T11:48:50Z)
• Framing RNN as a kernel method: A neural ODE approach [11.374487003189468]
  We show that the solution of a RNN can be viewed as a linear function of a specific feature set of the input sequence, known as the signature. We obtain theoretical guarantees on generalization and stability for a large class of recurrent networks.
  arXiv  Detail & Related papers  (2021-06-02T14:46:40Z)
• Learning Graph Neural Networks with Approximate Gradient Descent [24.49427608361397]
  Two types of graph neural networks (GNNs) are investigated, depending on whether labels are attached to nodes or graphs. A comprehensive framework for designing and analyzing convergence of GNN training algorithms is developed. The proposed algorithm guarantees a linear convergence rate to the underlying true parameters of GNNs.
  arXiv  Detail & Related papers  (2020-12-07T02:54:48Z)
• The Surprising Power of Graph Neural Networks with Random Node Initialization [54.4101931234922]
  Graph neural networks (GNNs) are effective models for representation learning on relational data. Standard GNNs are limited in their expressive power, as they cannot distinguish beyond the capability of the Weisfeiler-Leman graph isomorphism. In this work, we analyze the expressive power of GNNs with random node (RNI) We prove that these models are universal, a first such result for GNNs not relying on computationally demanding higher-order properties.
  arXiv  Detail & Related papers  (2020-10-02T19:53:05Z)
• Fast Learning of Graph Neural Networks with Guaranteed Generalizability: One-hidden-layer Case [93.37576644429578]
  Graph neural networks (GNNs) have made great progress recently on learning from graph-structured data in practice. We provide a theoretically-grounded generalizability analysis of GNNs with one hidden layer for both regression and binary classification problems.
  arXiv  Detail & Related papers  (2020-06-25T00:45:52Z)
• Multipole Graph Neural Operator for Parametric Partial Differential Equations [57.90284928158383]
  One of the main challenges in using deep learning-based methods for simulating physical systems is formulating physics-based data. We propose a novel multi-level graph neural network framework that captures interaction at all ranges with only linear complexity. Experiments confirm our multi-graph network learns discretization-invariant solution operators to PDEs and can be evaluated in linear time.
  arXiv  Detail & Related papers  (2020-06-16T21:56:22Z)

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.