# torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem

arXiv: https://arxiv.org/abs/2402.03640 · HTML: https://mlsanity.com/paper/2402.03640/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 18 of its 44 references that are in the map.
- First posted on arXiv 6 Feb 2024.

## Builds on (most cited first, 18 of 18)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Attention, Learn to Solve Routing Problems!](https://mlsanity.com/paper/1803.08475/) (2018)
- [Machine Learning for Combinatorial Optimization: a Methodological Tour d'Horizon](https://mlsanity.com/paper/1811.06128/) (2018)
- [Neural Combinatorial Optimization with Reinforcement Learning](https://mlsanity.com/paper/1611.09940/) (2016)
- [Learning Combinatorial Optimization Algorithms over Graphs](https://mlsanity.com/paper/1704.01665/) (2017)
- [Exact Combinatorial Optimization with Graph Convolutional Neural Networks](https://mlsanity.com/paper/1906.01629/) (2019)
- [Reinforcement Learning for Combinatorial Optimization: A Survey](https://mlsanity.com/paper/2003.03600/) (2020)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Combinatorial Optimization with Graph Convolutional Networks and Guided Tree Search](https://mlsanity.com/paper/1810.10659/) (2018)
- [Combinatorial Optimization with Physics-Inspired Graph Neural Networks](https://mlsanity.com/paper/2107.01188/) (2021)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [A Bi-Level Framework for Learning to Solve Combinatorial Optimization on Graphs](https://mlsanity.com/paper/2106.04927/) (2021)
- [NSNet: A General Neural Probabilistic Framework for Satisfiability Problems](https://mlsanity.com/paper/2211.03880/) (2022)
- [Learning from Survey Propagation: a Neural Network for MAX-E-3-SAT](https://mlsanity.com/paper/2012.06344/) (2020)
- [Learning Branching Heuristics for Propositional Model Counting](https://mlsanity.com/paper/2007.03204/) (2020)
- [Learning MAX-SAT from Contextual Examples for Combinatorial Optimisation](https://mlsanity.com/paper/2202.03888/) (2022)
- [Incremental Cardinality Constraints for MaxSAT](https://mlsanity.com/paper/1408.4628/) (2014)
- [Branch & Learn for Recursively and Iteratively Solvable Problems in Predict+Optimize](https://mlsanity.com/paper/2205.01672/) (2022)

## Built on by (most cited first, 3 of 3)

- [Neural Approaches to SAT Solving: Design Choices and Interpretability](https://mlsanity.com/paper/2504.01173/) (2025)
- [On the Dataless Training of Neural Networks](https://mlsanity.com/paper/2510.25962/) (2025)
- [Learning to Solve Weighted Maximum Satisfiability with a Co-Training Architecture](https://mlsanity.com/paper/2511.19544/) (2025)

## Abstract (arXiv)

The remarkable achievements of machine learning techniques in analyzing discrete structures have drawn significant attention towards their integration into combinatorial optimization algorithms. Typically, these methodologies improve existing solvers by injecting learned models within the solving loop to enhance the efficiency of the search process. In this work, we derive a single differentiable function capable of approximating solutions for the Maximum Satisfiability Problem (MaxSAT). Then, we present a novel neural network architecture to model our differentiable function, and progressively solve MaxSAT using backpropagation. This approach eliminates the need for labeled data or a neural network training phase, as the training process functions as the solving algorithm. Additionally, we leverage the computational power of GPUs to accelerate these computations. Experimental results on challenging MaxSAT instances show that our proposed methodology outperforms two existing MaxSAT solvers, and is on par with another in terms of solution cost, without necessitating any training or access to an underlying SAT solver. Given that numerous NP-hard problems can be reduced to MaxSAT, our novel technique paves the way for a new generation of solvers poised to benefit from neural network GPU acceleration.