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

TL;DR

This work tackles NP-hard MaxSAT by introducing torchmSAT, a differentiable, oracle-free solver that encodes a CNF instance into a fixed matrix $W$ and optimizes a relaxable variable vector $\mathbf{x}$ through a single differentiable function $f(\mathbf{x})$, solving via backpropagation. The method computes an unsatisfaction vector $\mathcal{U}=f(\mathbf{x})$ and uses a masked mean-squared error loss to iteratively refine $\mathbf{x}$, with a projection $\mathbf{x}'$ mapping back to Boolean assignments and a condition $\mathbf{x}' \cdot W = \mathbf{s}$ to identify unsatisfied clauses. Unlike traditional solvers that rely on a SAT oracle, torchmSAT is progressive and GPU-accelerated, and experiments show it outperforms two baselines while matching a third on several challenging instances, highlighting the potential of neural, LP-relaxation–inspired approaches for combinatorial optimization. The work thus proposes a new class of neural solvers for NP-hard problems that leverage differentiable optimization and hardware acceleration to explore solution spaces without labeled data or external SAT calls.

Abstract

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.

Figures (7)

• Figure 1: Existing MaxSAT solvers depend on a SAT oracle to iteratively evaluate a Boolean formula, $\mathcal{F}$, and update the clauses in $\mathcal{F}$ to reduce the number of unsatisfied clauses, $\mathcal{U}$. Our torchmSAT solver eliminates the need for a SAT oracle and encodes $\mathcal{F}$ in the architecture of a neural network. Maximizing satisfiability is performed using backpropagation on the neurons contributing to $\mathcal{U}$.
• Figure 2: Overview of torchmSAT neural network architecture. The learnable vector $\mathbf{x}$ represents the assignments of the Boolean variables in a conjunctive normal form, $\mathcal{F}$. The $W$ matrix is fixed and encodes a given MaxSAT instance represented in conjunctive normal form (CNF), i.e. Equation \ref{['eq:cnf']}, where the rows represent boolean variables, and columns represent clauses. A value of 1 or-1 is assigned if a variable $x_i$ or $\neg x_i$ appears in clause $c_j$ respectively; and 0 otherwise. The output layer calculates the unsatisfied cores, $\mathcal{U}$. The loss function, $\mathcal{L}$, calculates gradients with respect to elements of $\mathbf{x}$ that are contributing to $\mathcal{U}$. The neural network requires no data for training. Rather, the training process functions as the solving process of maximizing the number of satisfied clauses in $\mathcal{F}$.
• Figure 3: Performance of torchmSAT as compared to the state-of-the-art MaxSAT solvers in PySAT imms-sat18, namely FM, RC2 and LSU (refer to Section \ref{['sec:preliminaries']} for detailed descriptions of algorithms). Each row represents one of the datasets and each column is the time limit given to the solver. Each dataset contains 50 problem instances of increasing size (number of Boolean variables and number of clauses). In the plots, the problem size is parameterized by its total number of clauses on the x-axis. On the y-axis, the cost represents the number of unsatisfiable clauses ($\mathcal{U}$) by the end of the time limit. The FM and RC2 solvers tend to not perform well as problem instances get larger. The reason is that their solving process starts by calling the SAT oracle to establish the unsatisfiability of the given formula, which is NP-hard. LSU is the best-performing algorithm since it solves a given problem incrementally, delaying expensive calls to the SAT solver to the end. Our proposed approach, torchmSAT, is designed to be progressive like LSU, but without calling a SAT oracle. As evident from the plots, given more time, it becomes increasingly effective at finding solutions with lower costs. Synthesis scripts for the datasets are available in Appendix \ref{['appendix:dataset']}. PySAT solvers are called using their default configurations.
• Figure 4: Running torchmSAT on CPU vs. GPU, where it is capable of taking advantage of GPU acceleration, and finds better MaxSAT solutions within the same time limit (5mins). For complete results on scalability under different time limits, and on GT and PAR datasets, see Appendix \ref{['appendix:gpu']}.
• Figure 5: Running torchmSAT on CPU vs. GPU, where it is capable of taking advantage of GPU acceleration, and finds better MaxSAT solutions within the same time limit (10mins).