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

In recent years, machine learning has emerged as a powerful method for solving complex combinatorial optimization problems, a class of problems that are notably difficult to solve due to their inherent combinatorial nature. These problems often fall within the realm of Karp’s NP-hard complexity class [18], requiring a substantial amount of computational resources to find exact solutions as the problem size increases. The application of machine learning, particularly deep neural networks, has demonstrated remarkable potential in tackling such problems [8]. Machine learning techniques encompass a diverse range of approaches, including those that substitute traditional heuristics within existing algorithms [13, 26, 44, 20], enhance solvers by incorporating learned configurations [14, 43, 37], or reformulate a problem as a Markov Decision Process and employ reinforcement learning strategies [30, 21, 19, 7]. These techniques have been successfully employed across various domains, from operations research and graph theory to constraint satisfaction and scheduling problems, offering a new perspective on addressing the challenges posed by NP-hard problems [8].

Satisfiability (SAT) and Maximum Satisfiability (MaxSAT) problems represent two prominent classes of combinatorial optimization problems. In the case of SAT, the objective is to determine whether there exists an assignment of truth values to a given set of Boolean variables that satisfies a given set of logical clauses, typically expressed in conjunctive normal form (CNF). When the problem is non-satisfiable, MaxSAT extends the SAT problem by seeking an assignment that maximizes the number of satisfied clauses, rather than trying to satisfy all clauses. MaxSAT problems are of particular interest due to their ability to model optimization scenarios where some degree of constraint violation is tolerable, capturing a broader range of real-world applications [39, 40, 17]. Both SAT and MaxSAT problems have been extensively studied, giving rise to a variety of algorithmic techniques and heuristics aimed at efficiently solving or approximating solutions to these problems [5].

Existing MaxSAT solvers employ a diverse range of techniques to efficiently tackle the Maximum Satisfiability problem. These techniques can generally be classified into two main categories: complete and incomplete methods. Complete methods, such as Branch and Bound algorithms [24], search exhaustively for an optimal solution, guaranteeing the best possible assignment of truth values to satisfy the maximum number of clauses. Some complete solvers utilize SAT solvers as a core engine, iteratively refining their search space by tightening the upper bound of unsatisfied clauses, as seen in iterative SAT-based MaxSAT algorithms [32, 33]. In contrast, incomplete methods, like local search algorithms, do not guarantee optimality but aim to find high-quality solutions in less time. These methods involve exploring the solution space by iteratively making small changes to the current assignment of truth values, guided by various heuristics and neighborhood search strategies [29, 31]. Both complete and incomplete MaxSAT solvers have been successfully applied to real-world problems, with the choice of solver being dependent on the problem size, required optimality guarantees, and available computational resources.

In this paper, we present a novel MaxSAT solver, called torchmSAT, that leverages neural networks and falls within the incomplete category. Departing from the conventional practice of incrementally enhancing existing SAT solvers for MaxSAT resolution, we propose a completely new algorithm developed from scratch. As depicted in Figure 1, our method forgoes the necessity for a traditional SAT solver as a fundamental component of the search algorithm in incomplete techniques for MaxSAT. Rather than training a neural network to predict assignments that maximize satisfied clauses, an inherently complex task, we develop a novel neural network architecture with a differentiable loss function for solving MaxSAT. The key intuition is that by relaxing the binary constraint of the problem and allowing the Boolean variables to be represented in a continuous domain, advances in deep learning libraries would allow this optimization to be executed efficiently. Accordingly, the training process can be seen as a process that iteratively explores the solution space, generating progressively improved variable assignments. Consequently, our approach eliminates the need for labeled training data, or the need to call an underlying SAT solver to testify (un)satisfiability. Moreover, since our proposed solver is natively built using a reliable deep learning library [35], we are able to run the solver on GPUs without any change to the data structure, the solving algorithm or the optimization process. Therefore, we investigate the advantages of hardware acceleration for solving MaxSAT, demonstrating that the acceleration of such computations enables the solver to traverse the feasible solution space more rapidly. In essence, torchmSAT presents a fresh approach for solving MaxSAT that could potentially open doors for a new generation of combinatorial optimization solvers.

MaxSAT Formulation. In propositional logic, a Boolean formula is composed of Boolean variables, $\mathbf{x}=\{x_{1},x_{2},\dots x_{n}\}$, and logical operators, including negations ($\neg$), conjunctions ($\wedge$), and disjunctions ($\vee$). A common representation for Boolean formulas is the conjunctive normal form (CNF), which is structured as a conjunction of multiple clauses, $\boldsymbol{C}=\{c_{1},c_{2},\dots,c_{m}\}$. Each clause is a disjunction of literals, where a literal can be either a variable or its negation.

This format facilitates the systematic analysis and manipulation of Boolean expressions for various computational tasks. A formula is deemed satisfiable if there is at least one assignment of Boolean variables, $\mathbf{}{x}$, that satisfies all clauses. In numerous applications, a formula may not be entirely satisfiable, and the objective of MaxSAT solvers is to identify an assignment that satisfies the greatest number of clauses. In this scenario, the number of unsatisfied clauses is referred to as the cost of the CNF – a lower cost corresponds to a better assignment. In some applications, (weighted) partial CNF formulas are considered. Clauses in a partial CNF formula are characterized as hard, $\mathcal{H}$, meaning that these must be satisfied, or soft, $\mathcal{S}$, meaning that these are to be satisfied, if at all possible.

SAT Oracle. Existing MaxSAT solvers employ SAT oracles to handle CNF formulas. A SAT oracle is any algorithm that can determine the satisfiability of any given Boolean formula in the conjunctive normal form (CNF). If the formula is satisfiable, the SAT oracle provides a satisfying assignment; if not, it returns additional information such as an unsatisfiable core, $\mathcal{U}\subseteq\mathcal{F}$. The unsatisfiable core, $\mathcal{U}$, represents a subset of $\mathcal{F}$’s clauses that are inherently unsatisfiable. The task of determining the satisfiability of a given CNF is indeed NP-complete [18].

Conflict-Driven Clause Learning (CDCL) is a method used by modern SAT solvers to efficiently search the solution space and resolve conflicts during the search process. State-of-the-art SAT solvers build upon the basic DPLL (Davis-Putnam-Logemann-Loveland) algorithm [34], which employs backtracking and unit propagation, by adding clause learning and non-chronological backtracking [10]. When a CDCL-based solver encounters a conflict, which occurs when the current partial assignment of $\boldsymbol{X}$ leads to an unsatisfiable core $\mathcal{U}$, it analyzes the conflict to generate a new learned clause. This learned clause represents the assignments of variables contributing to the conflict and helps in preventing the solver from introducing similar conflicts in the future. The solver then performs jumping back several levels in the search tree instead of just one, using the learned clause to guide the process. The main advantage of CDCL-based solvers is their ability to learn from conflicts and use that knowledge to prune the search space more effectively. This results in faster and more efficient SAT solving for many real-world problem instances.

MaxSAT Solvers. In an unweighted MaxSAT problem, a typical MaxSAT algorithm proceeds by making several calls to an underlying SAT oracle such as CaDiCaL [12], Glucose [6] or Minisat [41]. The difference amongst algorithms is how they orchestrate the calls to the SAT solver. For example, the RC2 algorithm sends $\mathcal{F}$ to the SAT solver, which reports that $\mathcal{F}$ is unsatisfiable and returns an unsatisfiable core, $\mathcal{U}$. At least one of the clauses of the core will have to be disregarded in order to fix the core. So, the algorithm proceeds by relaxing each clause in $\mathcal{U}$ (i.e. augmenting the clause with a fresh variable called relaxation variable) and constrains the sum of the relaxation variables to be at most one [16]. In other words, the algorithm starts by assuming all clauses can be satisfied and iteratively relaxes this assumption until it finds a satisfying assignment. Similarity, the FM algorithm [27] involves a sequence of calls to an unsatisfiability oracle, each of which generates an unsatisfiable core. The clauses that are part of this unsatisfiable core are then relaxed, followed by the introduction of a new constraint that pertains to the relaxation variables in the formula. On the other hand, the LSU algorithm runs a series of satisfiability oracle calls refining an upper bound on the MaxSAT cost, followed by one unsatisfiability call, which stops the algorithm [31]. In other words, it finds an initial assignment with a suboptimal cost, and iteratively search for better assignments to reduce the cost.

In our work, we present a novel MaxSAT algorithm that does not rely on a SAT oracle during the search process. Instead, it adopts a progressive strategy akin to the one described in [31] and relies entirely on the neural network for identifying unsatisfiable cores, $\mathcal{U}$, and discovering improved solutions through backpropagation.

ML for MaxSAT. Several recent efforts have investigated the integration of machine learning in solving SAT and MaxSAT problems. Selsam et al. [38] train a graph neural network classifier to predict satisfiability of random SAT problems. The model learns to search for satisfying assignments during inference for problem instances that are larger than the ones seen during training. Similarily, Li and Si [25] present a framework for SAT solving utilizing Belief Propagation (BP). They introduce a Graph Neural Network (GNN) architecture that embeds BP in the latent space and use the trained model for marginal inference to obtain satisfying assignments for SAT. Other learning-based methods have been proposed for MaxSAT. For example, Kumar et al. [23] propose a method for learning combinatorial optimization problems from contextual examples, which indicate whether solutions are adequate in specific contexts. The framework uses the MaxSAT formulation and considers a specific setting where example solutions and negative solutions are context-specific. In the same way, Berden et al. [9] train MaxSAT models from examples and use a genetic algorithm that decreases the number of evaluations needed to find good models. Marino [28] uses a supervised learning approach to develop an algorithm that can fix Boolean variables based on local information from the Survey Propagation algorithm. In general, this line of research collects training data on MaxSAT instances, and trains a model that generalizes for bigger problems. Our method is different as it does not necessitate the gathering of any training data.

NN-based Combinatorial Optimization. An emerging approach to incorporating machine learning for tackling combinatorial optimization problems involves regarding the neural network’s training process as the problem-solving procedure for a given instance. In this paradigm, a neural network is dynamically generated based on the problem instance, and through multiple iterations of forward and backpropagation, a series of learnable parameters embody the ultimate solution to the problem instance. The absence of data requirements for training makes this method particularly attractive for deployment in diverse settings. For instance, Alkhouri et al. [4] introduce a technique that operates on graphs and addresses the Maximum Independent Set (MIS) problem [42]. The core concept involves representing the MIS problem as a single differentiable function, which facilitates the utilization of differentiable solutions. Schuetz et al. [36] present a Graph Neural Network (GNN)-based solver for approximately solving combinatorial optimization problems by encoding the optimization problem using a Hamiltonian (cost function) and associating binary decision variables with vertices in an undirected graph. A relaxation strategy is applied to generate a differentiable loss function for learning the GNN’s node representations. After several iterations, a softmax activation is applied to obtain one-dimensional probabilistic node assignments, which are then mapped back to integer variables using a projection heuristic. Both work can be viewed as a Linear Programming (LP) relaxation of the Mixed-Integer Linear Programming (MILP) formulation of the investigated problems, i.e. Maximum Independent Set (MIS), and Maximim Cut (MaxCUT). While our approach is inspired by the same ideas, we address a different problem (i.e. MaxSAT), and eliminate the use of GNNs.

Key Idea. Our proposed method, torchmSAT, is conceptually inspired by the technique of Linear Programming (LP) relaxations often utilized in the field of Mixed Integer Linear Programming (MILP) [1]. In MILP, certain variables are constrained to take only integer values which makes the optimization problem NP-hard. A common strategy to tackle this issue is to apply LP relaxation, where the integer constraints on the variables are relaxed, allowing them to take on continuous values. Similarly, in our method, we treat the binary variables of the MaxSAT problem as continuous, allowing us to leverage the power of differentiable optimization methods. The challenge we try to address becomes constructing a single differentiable function capable of approximating solutions for MaxSAT problems. Once derived, implementing the optimization process using a neural network allows us to capitalize on existing deep learning libraries, and their acceleration capabilities.

In what comes next, we begin by deriving a single differentiable function for MaxSAT using a novel neural network architecture. We describe the key components, their interactions, and their roles in the solving process. Following this, we show how our solver is different in finding unsatisfiable cores and how the solving process proceeds.

The Neural Network Architecture. Our proposed single differentiable function for MaxSAT is modeled as a neural network. Figure 2 presents a high-level overview of its architecture. At the heart of our solving algorithm lies a vector, $\mathbf{x}$, which represents the relaxations of the Boolean variables in a given MaxSAT instance (refer to Equation 4). The vector $\mathbf{x}$ is the only trainable set of parameters within the neural network. Although $\mathbf{x}$ consists of real numbers, at any given point in time during the solving process, we can project it back into the binary domain to derive the variable assignments. To reverse the relaxation, we interpret $x_{i}=1$ when $x_{i}>0$, and $0$ otherwise. At the onset of the solving process, $\mathbf{x}$ is initialized with random real values. Interpreting the values at this point merely corresponds to assigning random Boolean values to the variables. Throughout the solving process, the values of $\mathbf{x}$ are incrementally updated in a direction that minimizes the loss. This specific design prompts the network to progressively learn to satisfy an increasing number of clauses.

In the context of backpropagation and the chain rule, the derivative of a multiplication operation with respect to its inputs distributes the gradients. Therefore, the first hidden layer performs a point-wise multiplication between $\mathbf{x}$ and a vector of identical length containing all values set to 1, denoted as $\mathbf{e}$. This vector serves to propagate the gradient to the corresponding $x_{i}$s during the backpropagation process. After that, and to stabilize backpropagation, a $\tanh$ activation function is applied to constrain the values of the first layer within the range of -1 to 1. The $\tanh$ activation prevents the output of the first layer from reaching excessively high or low values, which could potentially terminate the learning (i.e. solving) prematurely. The rest of the neural network is fixed (i.e. non-learnable) and architected to encode our novel single differentiable function.

The second layer uniquely encodes a given MaxSAT instance. A matrix $W_{n,m}$ is initialized at the start of the solving process, with rows representing variables $x_{i}$’s and columns representing clauses $c_{j}$’s. A value of $1$ is set if a variable $x_{i}$ appears in clause $c_{j}$, while a value of $-1$ is set if its negation $\neg x_{i}$ appears in $c_{j}$. All other entries in the matrix are set to 0. This formulation results in our unique differentiable function, $f(\mathbf{x})$, which generates a vector $\mathcal{U}$ of length $m$:

where $\odot$ is element-wise multiplication, and $\cdot$ is a matrix multiplication. The entries of this vector, $\mathcal{U}$, indicate the (un)satisfiability status of each clause, serving as a dual-purpose: an evaluator for SAT and a guide for variable gradients.

Example. Consider the following MaxSAT problem in CNF:

This formula is not satisfiable. It is evident that any combination of binary assignments for $x_{1}$ and $x_{2}$ can satisfy, at most, two clauses. Assume that $\mathbf{x}$ is initialized randomly as $[0.43,1.27]$, which is interpreted as $x_{1}=1$ and $x_{2}=1$ since both values are positive. The output of the forward pass is:

Similar to the reverse relaxation operation of $\mathbf{x}$, the output of $f(\mathbf{x})$ is interpreted similarly, i.e. $c_{j}$ is satisfied if its activation in $f$ is positive, and vice versa. In this case, the output indicates that the first two clauses are unsatisfied, while only the last clause is satisfied. This represents the first role of $f(\mathbf{x})$ as a SAT evaluator. To satisfy the first two clauses, the values of $\mathbf{x}$ need to become negative so that the activations of the first two clauses in $f$ are positive. This is where the role of the loss function comes in. The loss function, $\mathcal{L}$, computes the MSE between $f(x)$ and a zero vector for the unsatisfied clauses. A single iteration of backpropagation updates the values of $x_{1}$ and $x_{2}$ in the negative direction of the gradient, moving their values closer to zero. For instance, with a learning rate of $0.1$, the new values of $\mathbf{x}$ will be $[0.34,1.23]$. The process continues as the forward-loss-backward loop attempts to satisfy the first two clauses. However, once the first two clauses are satisfied (i.e., $\mathbf{x}$’s are negative, representing a Boolean zero when reversing the relaxation), the third clause becomes unsatisfied. This is when the training process explores other ways of satisfying more clauses.

Unsatisfiable Cores Contrary to conventional MaxSAT solvers discussed in Section 3 that rely on a SAT oracle to identify the set of unsatisfied clauses, $\mathcal{U}$, if the formula is determined to be unsatisfiable, our proposed neural network model directly infers the unsatisfied clauses from $f(\mathbf{x})$. Nevertheless, for larger problems, the activations of $f(\mathbf{x})$ alone might not be enough to ascertain satisfiability. The reason is that the matrix multiplication occurring in the first two layers is a non-injective operation. This implies that distinct assignments for $\mathbf{x}$ might yield identical activations for $f(x)$. For instance, the inputs $\mathbf{x}=[0.43,-1.27]$ and $\mathbf{x}=[-1.27,0.43]$ would result in the same negative activation for the aforementioned third clause, despite the fact that the de-relaxed variable assignments are totally different; one corresponds to $[1,0]$ while the other corresponds to $[0,1]$. To overcome this, we use an alternative method to establish (un)satisfiability of clauses. We construct a vector, $\mathbf{s}$, of length $m$, where each entry corresponds to the negative of the number of variables present in its respective clause, i.e., $s_{j}=-len(c_{j})$. We also project $\mathbf{x}$ onto its Boolean domain, such that $x_{i}^{\prime}=1$ if $x_{i}>1$, and $0$ otherwise. This makes a clause in $\mathcal{U}$ unsatisfiable if and only if $\mathbf{x}^{\prime}\cdot W=\mathbf{s}$. We use this projection to mask out satisfied clauses in the loss function, and only calculate it for unsatisfied clauses. Consequently, gradients are computed exclusively for those variables that contribute to the unsatisfied clauses, resulting in a more efficient optimization.

The Solving Process. In contrast to conventional MaxSAT solvers, which necessitate invoking a SAT oracle, pausing to await a result, and then coordinating the subsequent call, our algorithm operates differently. torchmSAT operates in a progressive manner, which implies that it incrementally improves the solutions as the search process unfolds. Algorithm 1 shows the main steps of our solving process. The solving process is an iterative procedure that alternates between a forward pass, loss calculation, and backward propagation. In Line 1, we construct the neural network layers based on the given problem instance. While the time limit has not been exhausted, the forward pass, in Line 3, takes the current assignments of the Boolean variables, $\mathbf{x}$, and computes the output of the network, $f(\mathbf{x})$. In addition, it calculates the reversed relaxation of $\mathbf{x}$, denoted as $\mathbf{x}^{\prime}$, which is used to determine clauses are currently satisfied by the assignment in Line 4. In Lines 5-7, if the current assignment satisfies more clauses than previously found solutions, it outputs this result and updates the value of the best cost (the lower, the better). In Line 8, the loss function calculates the MSE between $f(\mathbf{x})$ and a zero vector of the same length, reflecting the number of unsatisfied clauses. The backpropagation step, in Line 9, adjusts the values of $\mathbf{x}$ according to the gradient calculated by backpropagation, moving the assignments in a direction that reduces the number of unsatisfied clauses. This process continues until all clauses are satisfied, as indicated by a zero loss, or a given time limit is reached.

In this section, we present a series of experiments designed to evaluate the performance of our proposed algorithm and compare it with existing state-of-the-art MaxSAT solvers. Our experiments aim to demonstrate the effectiveness of the method in various scenarios and showcase its strengths and limitations. We describe the experimental setup, including the problem instances used, the choice of benchmarks, and the evaluation metrics employed. Additionally, we provide a detailed analysis of the experimental results, highlighting key observations and insights. Through these experiments, we aim to validate the applicability of our approach and its potential impact on combinatorial optimization.

Setup. We use PyTorch (v1.10.2) [35]. No other dependencies are required to run torchmSAT (e.g. no calls to a SAT oracle is made). We use Adam optimizer for backprogation with a learning rate of 1e-4. For reproducibility and extensibility of our work, we use the PySAT toolkit (v0.1.8.dev1) [15] to synthesize hard problem instances and compare against existing methods. The toolkit provides a unified interface to various state-of-the-art SAT and MaxSAT solvers. The experimental results are obtained using a machine with Intel Xeon E5-2680 [email protected] GHz, 128GB RAM. For experiments on hardware acceleration, a Tesla P40 GPU is utilized to run torchmSAT.

Evaluation Criteria. We will use a multi-faceted approach to thoroughly assess the performance of our proposed method. First, we will investigate the cost obtained by our solver on problem instances of varying complexity and sizes, and under different time constraints. The imposition of a time limit in this scenario is crucial given the NP-hard nature of MaxSAT, which implies that exploring and assessing the entire feasible region would necessitate exponential time. Secondly, we will calculate the MaxSAT regret which quantifies the difference between the best solution found by any baseline solver and the solution obtained by our solver. Lastly, we will assess the impact of leveraging GPU acceleration on the performance of our solver.

Dataset. While the datasets of the popular MaxSAT evaluations ¹¹1https://maxsat-evaluations.github.io/ represent a set of non-trivial SAT instances, we opt to test our methods on smaller, yet hard, dataset to validate the applicability of the method. Although our method does not outperform one of the state-of-the-art SAT solvers, torchmSAT offers a completely revamped method to solve MaxSAT problems without the need for a SAT oracle. We employ PySAT to synthesize four representative datasets, encompassing combinatorial principles extensively examined in the context of propositional proof complexity. Specifically, they implement encodings for the pigeonhole principle (PHP) [11], the greater-than (ordering) principle (GT) [22], the mutilated chessboard principle (CB) [3], and the parity principle (PAR) [2]. For each principle, we synthesize 50 MaxSAT instances of increasing sizes where all problem instances are not satisfiable. In other words, there is at least one clause that cannot be satisfied, and the goal of MaxSAT solvers to find a feasible variable assignment that maximizes satisfiability. Synthesis scripts are available in Appendix A.

Comparing with Existing MaxSAT Solvers. As discussed in Section 2, existing MaxSAT algorithms proceed by making several calls to an underlying SAT oracle (i.e. solver). In PySAT, both the RC2 and the FM algorithms start their solving process by making a call to the underlying SAT solver, which reports that $\mathcal{F}$ is unsatisfiable and returns an unsatisfiable core, $\mathcal{U}$. The algorithm proceeds by alternating between relaxing clauses and calling the underlying SAT solver. As depicted in Figure 3, both methods struggle to find any assignment for moderately large problem instances. This is primarily due to their initial step, which involves invoking the SAT solver to establish unsatisfiability. Conversely, the LSU algorithm identifies an initial assignment carrying a suboptimal cost, then incrementally searches for superior assignments to lower the cost. This explains its position as the top-performing algorithm on the dataset. Our proposed method, torchmSAT, excels at progressively generating viable solutions that surpass those of FM and RC2. Indeed, when considering the GT dataset, torchmSAT’s performance approaches that of LSU.

In Table 1, we compute the average regret of RC2, FM, and torchmSAT relative to LSU, the top-performing MaxSAT solver. For every problem instance, we calculate a solver’s regret as the difference between the cost it achieves and the cost LSU achieves. As the results clearly show, torchmSAT generally demonstrates a markedly lower average regret. Raw results for individual problem instances can be found in Appendix B.

GPU Acceleration. The main premise of our method is the novel application of contemporary GPUs and the evolving ecosystem of deep learning libraries and accelerators in solving MaxSAT instances. In this section, we aim to demonstrate that by merely altering where the neural network is initialized, without any modifications to its structure or the solving process described earlier. As shown in Figure 4, executing torchmSAT on a GPU yields solutions to larger MaxSAT instances with lower costs within the same time limit. This can be attributed to the enhanced speed of GPU computations, which accelerates the forward-loss-backward loop (Algorithm 1), thereby enabling more extensive exploration of the feasible region of variable assignments.

The use of GPUs in torchmSAT advances MaxSAT solving, offering an accelerated and efficient exploration of the solution space. This acceleration is particularly transformative given that the algorithm’s progressive nature means it benefits directly from more rapid computations, enabling it to find better solutions within the same time frame. In contrast, traditional MaxSAT solvers are inherently sequential and cannot take advantage of GPU acceleration.

Limitations. While our proposed method presents several notable advantages, it also has some limitations. First, it currently only works for unweighted MaxSAT instances, meaning it cannot handle instances where different clauses have different weights or importance. Secondly, the algorithm lacks a definitive stopping criterion for backpropagation unless the optimal solution is zero. This means it can be difficult to determine when the algorithm has reached an optimal solution or when to halt the process except using timeouts. Lastly, the memory requirement for the method is $\mathcal{O}(nm)$, which can be prohibitive for large instances. Although the matrix W is sparse, which could potentially be leveraged to save memory, our current implementation does not take advantage of this sparsity.

Conclusions and Future Work. In conclusion, we have presented a new method for MaxSAT solving that capitalizes on the use of neural networks. Our method, named torchmSAT, is a progressive approach that continually refines and improves its solutions over time. One of the core advantages of torchmSAT is its independence from a SAT oracle, a feature that differentiates it from traditional MaxSAT solvers. This makes our method more self-sufficient and less reliant on external components. Experimental results show that our method outperforms two existing MaxSAT solvers, and is on par with another state-of-the-art solver for small to medium problem sizes. Additionally, torchmSAT is able to benefit from GPU acceleration, allowing for more rapid exploration of feasible solution regions. Despite some limitations, torchmSAT represents a promising step forward in MaxSAT problem solving. For future work, we aim to extend the capabilities of our method to handle weighted MaxSAT instances, develop a clear stopping criteria for backpropagation, and optimize memory usage by leveraging the sparsity of the matrix $W$. This could lead to a more efficient, versatile and powerful solver that can tackle even more complex problems.

Reproducibility. The implementation of torchmSAT is provided as a Python package in the supplementary material. The dataset can be synthesized using scripts in Appendix A.