Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs

• URL: http://arxiv.org/abs/2505.16053v1
• Date: Wed, 21 May 2025 22:07:08 GMT
• Title: Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs
• Authors: Jan Tönshoff, Martin Grohe,
• Abstract summary: This work introduces Reinforcement Learning from Algorithm Feedback (RLAF) as a paradigm for learning to guide SAT solver branchings with Graph Neural Networks (GNNs)<n> RLAF-trained policies significantly reduce the mean solve times of different base solvers across diverse SAT problem distributions, achieving more than a 2x speedup in some cases.
• Score: 2.722939308105689
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Boolean Satisfiability (SAT) solvers are foundational to computer science, yet their performance typically hinges on hand-crafted heuristics. This work introduces Reinforcement Learning from Algorithm Feedback (RLAF) as a paradigm for learning to guide SAT solver branching heuristics with Graph Neural Networks (GNNs). Central to our approach is a novel and generic mechanism for injecting inferred variable weights and polarities into the branching heuristics of existing SAT solvers. In a single forward pass, a GNN assigns these parameters to all variables. Casting this one-shot guidance as a reinforcement learning problem lets us train the GNN with off-the-shelf policy-gradient methods, such as GRPO, directly using the solver's computational cost as the sole reward signal. Extensive evaluations demonstrate that RLAF-trained policies significantly reduce the mean solve times of different base solvers across diverse SAT problem distributions, achieving more than a 2x speedup in some cases, while generalizing effectively to larger and harder problems after training. Notably, these policies consistently outperform expert-supervised approaches based on learning handcrafted weighting heuristics, offering a promising path towards data-driven heuristic design in combinatorial optimization.

Related papers

• Assessing and Enhancing Graph Neural Networks for Combinatorial Optimization: Novel Approaches and Application in Maximum Independent Set Problems [0.0]
  Graph Neural Networks (GNNs) show promise for researchers in solving Combinatorial optimization (CO) problems. This study investigates the effectiveness of GNNs in solving the maximum independent set (MIS) problem.
  arXiv  Detail & Related papers  (2024-11-06T09:12:31Z)
• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem [1.5850859526672516]
  We derive a single differentiable function capable of approximating solutions for the Maximum Satisfiability Problem (MaxSAT) We present a novel neural network architecture to model our differentiable function, and progressively solve MaxSAT using backpropagation.
  arXiv  Detail & Related papers  (2024-02-06T02:33:00Z)
• 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)
• Stochastic Unrolled Federated Learning [85.6993263983062]
  We introduce UnRolled Federated learning (SURF), a method that expands algorithm unrolling to federated learning. Our proposed method tackles two challenges of this expansion, namely the need to feed whole datasets to the unrolleds and the decentralized nature of federated learning.
  arXiv  Detail & Related papers  (2023-05-24T17:26:22Z)
• Learning To Dive In Branch And Bound [95.13209326119153]
  We propose L2Dive to learn specific diving structurals with graph neural networks. We train generative models to predict variable assignments and leverage the duality of linear programs to make diving decisions.
  arXiv  Detail & Related papers  (2023-01-24T12:01:45Z)
• Learning Branching Heuristics from Graph Neural Networks [1.4660170768702356]
  We first propose a new graph neural network (GNN) model designed using a probabilistic method. Our approach introduces a new way of applying GNNs towards enhancing the classical backtracking algorithm used in AI.
  arXiv  Detail & Related papers  (2022-11-26T00:01:01Z)
• Towards Better Out-of-Distribution Generalization of Neural Algorithmic Reasoning Tasks [51.8723187709964]
  We study the OOD generalization of neural algorithmic reasoning tasks. The goal is to learn an algorithm from input-output pairs using deep neural networks.
  arXiv  Detail & Related papers  (2022-11-01T18:33:20Z)
• NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks [13.185943308470286]
  Propositional satisfiability (SAT) is an NP-complete problem that impacts many research fields, such as planning, verification, and security. Recent work aimed to enhance CDCL SAT solvers using Graph Neural Networks (GNNs) This paper proposes an approach called NeuroBack, which builds on two insights: (1) predicting phases (i.e., values) of variables appearing in the majority (or even all) of the satisfying assignments are essential for CDCL SAT solving, and (2) it is sufficient to query the neural model only once for the predictions before the SAT solving starts.
  arXiv  Detail & Related papers  (2021-10-26T22:08:22Z)
• 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)
• SUNRISE: A Simple Unified Framework for Ensemble Learning in Deep Reinforcement Learning [102.78958681141577]
  We present SUNRISE, a simple unified ensemble method, which is compatible with various off-policy deep reinforcement learning algorithms. SUNRISE integrates two key ingredients: (a) ensemble-based weighted Bellman backups, which re-weight target Q-values based on uncertainty estimates from a Q-ensemble, and (b) an inference method that selects actions using the highest upper-confidence bounds for efficient exploration.
  arXiv  Detail & Related papers  (2020-07-09T17:08:44Z)
• Communication-Efficient Distributed Stochastic AUC Maximization with Deep Neural Networks [50.42141893913188]
  We study a distributed variable for large-scale AUC for a neural network as with a deep neural network. Our model requires a much less number of communication rounds and still a number of communication rounds in theory. Our experiments on several datasets show the effectiveness of our theory and also confirm our theory.
  arXiv  Detail & Related papers  (2020-05-05T18:08:23Z)

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.