Despite decades of intensive research and optimization, modern Boolean Satisfiability (SAT) solvers have reached a plateau where significant performance gains are increasingly difficult to achieve. While Large Language Models (LLMs) have demonstrated remarkable capabilities in pattern recognition and code generation for combinatorial optimization, their direct application to highly optimized SAT solvers remains a formidable challenge due to the extreme complexity and sensitivity of solver heuristics. In this paper, we introduce AESAT (Auto-Evolving SAT solving), a novel neuro-symbolic framework designed to automatically evolve and optimize the heuristic functions of SAT solvers. AESAT employs a memetic-inspired approach, synergizing LLM-guided individual optimization with evolutionary exploration. By leveraging self-optimized prompting techniques, our framework enables LLMs to iteratively discover and refine sophisticated heuristics that bypass the limitations of human-engineered designs. The efficacy of AESAT is demonstrated by its flagship derivative, AE-Kissat-MAB, which won the main track of the 2025 International SAT Competition by a wide margin. This result represents the first time an LLM-enhanced solver has dominated the world's premier SAT competition, marking a paradigm shift in the automated design of reasoning algorithms.

The Maximum Weight Clique Problem (MWCP) is NP-hard and is typically solved exactly within a Branch-and-Bound (BnB) framework, where the quality of upper bounds critically determines the pruning efficiency. Recent solvers enhance independent-set-based bounds using MaxSAT reasoning. However, their effectiveness is limited by two inherent limitations: (i) independent sets in conflicts are discarded after a single use, preventing their reuse in subsequent reasoning; and (ii) conflicts are detected in a fixed order regardless of their potential contribution to bound tightening. To address these issues, we propose two complementary techniques. The UnLocking Mechanism (ULM) preserves conflict cores and enables the reuse of independent sets in subsequent reasoning, while the Benefit-Enhanced Strategy (BES) steers the MaxSAT reasoning process toward conflicts and independent sets with higher pruning potential. By integrating ULM and BES, we develop a new solver, ULE-MWC (UnLocking Enhanced MWC). Experimental results on standard benchmarks show that ULE-MWC consistently yields tighter upper bounds and outperforms state-of-the-art exact solvers in both runtime and search efficiency.

The Simple Assembly Line Balancing Problem (SALBP) is a fundamental optimization challenge in the production and manufacturing domain. In this paper, we address a recently introduced variant, the Simple Assembly Line Balancing Problem with Power Peak Minimization (SALB3PM), which aims to minimize electricity consumption peaks. Despite the growing attention to this problem, existing approaches have yet to fully exploit the potential of logic-based methods. This work introduces exact solution approaches based on Satisfiability (SAT) and Maximum Satisfiability (MaxSAT) formulations to tackle SALB3PM efficiently. A experimental study was carried out on a benchmark set of 300 instances derived from the literature, considering state-of-the-art solvers across multiple paradigms, including SAT, MaxSAT, Integer Linear Programming (ILP), Constraint Programming (CP) and Pseudo-Boolean Optimization (PBO). The results clearly show that the proposed satisfiability-based methods outperform integer linear formulations. In this sense, the strategies introduced in this paper offer promising perspectives for extension to other SALBP variants.

The Weighted Partial MaxSAT (WPMS) problem requires finding an assignment that satisfies all hard clauses while maximizing the total weight of satisfied soft clauses. From a computational perspective, WPMS is not merely an extension of the uniform-weight Partial MaxSAT (PMS); rather, it requires search strategies that actively exploit weight information to navigate the solution space. While state-of-the-art heuristic and SAT-based solvers have successfully integrated weight-aware mechanisms, Branch-and-Bound (BnB) solvers, notably WMaxCDCL, largely treat weight information passively during search and pruning. In this paper, we bridge this gap by introducing two novel weight-aware strategies into the BnB framework. Our methods integrate weight information directly into the preprocessing and lower-bound estimation. Experimental results demonstrate that these strategies significantly enhance the performance of WMaxCDCL, establishing a new state-of-the-art for exact WPMS solving.

The MaxSAT problem is an optimization version of the satisfiability problem (SAT). A tight lower bound (LB) on the number of falsified soft clauses in a MaxSAT solution is crucial for the efficiency of Branch-and-Bound (BnB) MaxSAT solvers. To compute an LB, modern BnB solvers detect disjoint inconsistent subsets of soft clauses, called cores, using unit propagation. A notable feature of these solvers is that soft clauses belonging to already detected cores cannot be reused to detect additional cores, limiting the number of cores that can be detected. In this paper, we propose an unlocking mechanism that allows the reuse of soft clauses in already detected cores while ensuring the soundness of LB. Experimental results show that this unlocking mechanism consistently improves the performance of a state-of-the-art BnB solver. In addition, it allowed us to win the first two places in the exact unweighted category of the MaxSAT Evaluation 2024.

Algorithms designed for routing problems typically rely on high-quality candidate edges to guide their search, aiming to reduce the search space and enhance the search efficiency. However, many existing algorithms, like the classical Lin-Kernighan-Helsgaun (LKH) algorithm for the Traveling Salesman Problem (TSP), often use predetermined candidate edges that remain static throughout local searches. This rigidity could cause the algorithm to get trapped in local optima, limiting its potential to find better solutions. To address this issue, we propose expanding the candidate sets to include other promising edges, providing them an opportunity for selection. Specifically, we incorporate multi-armed bandit models to dynamically select the most suitable candidate edges in each iteration, enabling LKH to make smarter choices and lead to improved solutions. Extensive experiments on multiple TSP benchmarks show the excellent performance of our method. Moreover, we employ this bandit-based method to LKH-3, an extension of LKH tailored for solving various TSP variant problems, and our method also significantly enhances LKH-3's performance across typical TSP variants.

Given a Conjunctive Normal Form (CNF) formula ϕ and a positive integer k, the problem of Diversity Satisfiability (Diverse SAT) consists in finding k assignments satisfying ϕ while maximizing the sum of pairwise distances among them. Previous related works mainly focus on the design of heuristic algorithms, while this paper focuses on introducing exact methods. A quadratic integer programming (QIP) model is first proposed. Then, based on two novel weight functions, namely the direct weight (DW) and the incremental weight (IW), we reformulate the QIP models into two integer linear programming (ILP) models, which can also be adapted to Maximum Satisfiability (MaxSAT) instances. Extensive experiments were conducted to evaluate the efficiency of the proposed methods, showing that the proposed approaches are able to compute optimal solutions for the studied instances with linear models achieving superior performance.

We introduce a tableau calculus for solving the Maximum Satisfiability problem of propositional signed formulas (Signed MaxSAT) and prove its soundness and completeness. Furthermore, we outline how the calculus can be extended to incorporate both hard and soft formulas.

Partial MaxSAT (PMS) and Weighted PMS (WPMS) are two practical generalizations of the MaxSAT problem. In this paper, we propose a local search algorithm for these problems, called BandHS, which applies two multi-armed bandits to guide the search directions when escaping local optima. One bandit is combined with all the soft clauses to help the algorithm select to satisfy appropriate soft clauses, and the other bandit with all the literals in hard clauses to help the algorithm select appropriate literals to satisfy the hard clauses. These two bandits can improve the algorithm's search ability in both feasible and infeasible solution spaces. We further propose an initialization method for (W)PMS that prioritizes both unit and binary clauses when producing the initial solutions. Extensive experiments demonstrate the excellent performance and generalization capability of our proposed methods, that greatly boost the state-of-the-art local search algorithm, SATLike3.0, and the state-of-the-art SAT-based incomplete solver, NuWLS-c.

MaxSAT is a widely studied NP-hard optimization problem due to its broad applicability in modeling and solving diverse real-world optimization problems. Branch-and-Bound (BnB) MaxSAT solvers have proven efficient for solving random and crafted instances but have traditionally struggled to compete with SAT-based MaxSAT solvers on industrial instances. However, this changed with the introduction of the MaxCDCL algorithm, which successfully integrates clause learning into BnB to solve unweighted MaxSAT. Despite this progress, solving Weighted MaxSAT instances remained an open challenge. In this paper, we present WMaxCDCL, the first branch-and-bound (BnB) Weighted Partial MaxSAT solver with clause learning. We describe its algorithm and implementation in detail, experimentally evaluating key aspects that are critical to achieving strong performance. Our results demonstrate that WMaxCDCL can compete with the best state-of-theart MaxSAT solvers and, more importantly, that this new solving approach complements the existing SAT-based MaxSAT methods, which have dominated the field until now. Notably, the combination of WMaxCDCL with other techniques won the weighted track of the 2023 MaxSAT Evaluation, which is the leading annual competition for MaxSAT solvers, affiliated with the International Conference on Theory and Applications of Satisfiability Testing.

The use of constraint models in symbolic AI has significantly increased during the last decades for their capability of certifying the existence of solutions as well as their optimality. In the latter case, approaches based on the Maximum and Minimum Satisfiability problems, or MaxSAT and MinSAT, have shown to provide state-of-the-art performances in solving many computationally challenging problems of social interest, including scheduling, timetabling and resource allocation. Indeed, the research on new approaches to MaxSAT and MinSAT is a trend still providing cutting-edge advances. In this work, we push in this direction by contributing new tableaux-based calculi for solving the MaxSAT and MinSAT problems of regular propositional logic, referred to as Regular MaxSAT and Regular MinSAT problems, respectively. For these problems, we consider as well the two extensions of the highest practical interest, namely the inclusion of weights to clauses, and the distinction between hard (mandatory) and soft (desirable) constraints. Hence, our methods handle any subclass of the most general variants: Weighted Partial Regular MaxSAT and Weighted Partial Regular MinSAT. We provide a detailed description of the methods and prove that the proposed calculi are sound and complete.

The Maximum Satisfiability problem (MaxSAT) is a major optimization challenge with numerous practical applications. In recent MaxSAT evaluations, most MaxSAT solvers have incorporated an Integer Linear Programming (ILP) solver into their portfolios. However, a good portfolio strategy requires a lot of tuning work and is limited to the profiling benchmark. This paper proposes a methodology to fully integrate ILP preprocessing techniques into the MaxSAT solving pipeline and investigates the impact on the top-performing MaxSAT solvers. Experimental results show that our approach helps to improve 5 out of 6 state-of-the-art MaxSAT solvers, especially for WMaxCDCL-OpenWbo1200, the winner of the MaxSAT evaluation 2024 on the unweighted track, which is able to solve 15 additional instances using our methodology.

This paper introduces novel Maximum Satisfiability (MaxSAT) formulations for the Nonlinear Integer Programming (NLIP) problems with discrete polynomial functions. We develop a generic framework based on three established integer encoding techniques from the literature. Our approach treats each polynomial term as an atomic unit and demonstrates how it can be efficiently encoded through compact representations of integer assignments. Additionally, we present two distinct decomposition methods based on the degrees of polynomial terms. This work lays a foundation for future research and has the potential to extend the applicability of modern MaxSAT solvers to a wider range of optimization problems.

The problem of packing equal circles in a circular container is a classic and famous packing problem, which is well-studied in academia and has a variety of applications in industry. The problem is computationally challenging, and researchers mainly focus on small to moderate-scale instances with the number of circular items n less than 320 in the literature. In this work, we aim to solve this problem on large scale, and it is the bottleneck for most global optimization problems. Specifically, we propose a novel geometric batch optimization method that makes batch gradient descent based on the geometric locations of packing items. This method not only can speed up the convergence process of continuous optimization significantly but also reduce the memory requirement during the program's runtime. Then, we propose a heuristic search method, called solution-space exploring and descent, that can discover a feasible solution efficiently on large scale. Besides, we propose an adaptive neighbor object maintenance method to maintain the neighbor structure applied in the continuous optimization process. In this way, we can find high-quality solutions on large-scale instances within reasonable computational times. Extensive experiments on the benchmark instances sampled from n = 300 to 1000 show that our proposed algorithm outperforms the state -of -the -art algorithms and performs excellently on large-scale instances. In particular, our algorithm found 10 improved solutions among the 21 well-studied moderate-scale instances and 95 improved solutions among the 101 sampled large-scale instances. Furthermore, our geometric batch optimization, heuristic search, and adaptive maintenance methods are general and can be adapted to other packing and continuous optimization problems.

The Latin square completion (LSC) problem aims to assign n symbols to the empty cells of a partially filled Latin square such that in each row and each column, each symbol appears exactly once. In this paper, we propose a swap relaxation-based fast local search algorithm called SRLS for solving the LSC problem. First, it introduces a novel search space definition, which forbids row conflicts based on which a swap-based neighborhood is defined. Second, a color domain relaxation technique is employed in the swap-based neighborhood by temporarily accepting the violation of some constraints to connect high-quality solutions. Third, two effective scoring functions are adopted to select neighborhood moves minimizing the number of conflicting edges as well as the number of color domain violations. Finally, SRLS employs an adaptive restart mechanism to balance the exploitation and exploration of the search. Extensive experiments on 1819 public benchmark instances demonstrate that SRLS outperforms the state-of-the-art algorithms in the literature in terms of both success rate and computational efficiency.

The problem of packing equal spheres in a spherical container is a classic global optimization problem, which has attracted enormous studies in academia and found various applications in industry. This problem is computationally very challenging, and many efforts focus on small-scale instances with the number of spherical items less than 200 in the literature. In this work, we propose an efficient local search heuristic algorithm named solution space exploring and descent for solving this problem, which can quantify the solution’s quality to determine the number of exploring actions and quickly discover a high-quality configuration. Besides, we propose an adaptive neighbor item maintenance method to speed up the convergence of the continuous optimization process and reduce the time consumption. Computational experiments on a large number of benchmark instances with 5≤n≤400 spherical items show that our algorithm significantly outperforms the state-of-the-art algorithm. Specifically, our algorithm improves 274 best-known results and matches 84 best-known results out of the 396 well-known benchmark instances.