The Large Weight Syndrome Decoding problem LWSD is a fundamental problem in coding theory. It consists in determining whether a given linear code admits a high Hamming weight vector associated with a specific syndrome. LWSD is a variant of the classical syndrome decoding problem, which conversely seeks a low Hamming weight solution for a linear system defined over the binary field 𝔽₂. In this paper, we investigate a generalization of this problem to the case of a prime finite field 𝔽_Z, referred to as LWZSD. We propose several models using Boolean Satisfiability (SAT) formulas and compare the efficiency of our approaches using state-of-the-art solvers.

Dijkstra’s token ring algorithm is a fundamental example of a self-stabilizing algorithm for solving mutual exclusion in an asynchronous distributed system arranged as a rooted directed ring. This paper studies the self-stabilization of this algorithm using an approach based on propositional satisfiability. We propose a logical modeling framework for the asynchronous executions of the algorithm that rigorously captures the state update rules, as well as the mechanisms for detecting convergence toward a legitimate configuration or, conversely, divergence through the existence of cycles between illegitimate configurations. Furthermore, we also optimize the efficiency and scalability of the analysis by introducing an offset-based symmetry-breaking technique applied to the initial configurations, thereby significantly reducing redundant explorations of equivalent execution scenarios. In addition, we extend the study to restricted daemon assumptions to assess open challenges.

Multi-Armed Bandit (MAB) mechanisms have proven effective for adaptive heuristic switching in modern CDCL SAT solvers, with Kissat_MAB and its variants demonstrating strong performance in recent SAT Competitions. However, while strategies like the Luby series generate restarts with high duration variability, standard bandit models treat each restart as a homogeneous unit. This mismatch can bias credit assignment and lead to suboptimal exploration–exploitation trade-offs between short and long restarts. In this paper, we study MAB-based heuristic selection under variable-duration restart policies and propose a duration-aware modification to both bandit feedback and selection mechanisms. Our approach normalizes and conditions rewards on the restarts and adapts exploration and exploitation accordingly, thereby better aligning bandit updates with the solver’s restart dynamics.

Maximum Satisfiability (MaxSAT) is an optimization extension of the Satisfiability (SAT) problem. In Branch-and-Bound (BnB) MaxSAT solving, the quality of the lower bound estimation is critical for effective search space pruning. State-of-the-art BnB solvers typically estimate this bound by identifying disjoint inconsistent subformulas (cores) via Unit Propagation (UP). However, a limitation of this standard approach is that UP fails to detect cores that exhibit complex dependencies with already identified cores. In this paper, we propose a further lookahead algorithm that leverages pre-detected cores to uncover additional disjoint inconsistencies, thereby tightening the lower bound. Experimental results demonstrate that the proposed algorithm significantly tightens the lower bound, enabling the state of the art BnB solver MaxCDCL to solve more instances.

Abstract The Syndrome Decoding Problem (SDP) for a binary linear code consists in finding a particular solution to an underdetermined linear system defined over the finite field of two elements, such that the Hamming weight of this solution is smaller than a given bound. In this paper, we explore several satisfiability-based models for solving this problem relying on XNF and classical CNF representations. We compare these approaches to assess their efficiency in solving SDP. Furthermore, we also introduce a Maximum Satisfiability (MaxSAT) model of the Low-Weight Codeword Problem (LWCP), which consists in finding a word with minimal Hamming weight in a given code. In particular, we introduce three MAX-SAT models for LWCP: an XNF model, which reuses the XOR constraints from the SDP formulations, and two CNF models, which are also based on the CNF formulations from SDP. For all three models, we add soft clauses to minimize the Hamming weight. Finally, we assess the models using state-of-the-art MaxSAT solvers, which apply different solving paradigms to compute optimal codeword weights.

While Maximum Satisfiability (MaxSAT) has been successfully applied to a wide range of combinatorial optimization problems, the encoding of Nonlinear Integer Programming (NLIP) with polynomial functions into MaxSAT has so far only been studied at a theoretical level. In this paper, we introduce NLIPSat, the first tool capable of encoding bounded polynomial NLIP instances directly into Maximum Satisfiability. Building upon recent MaxSAT formulations for polynomial NLIP proposed in [Zhifei Zheng et al., 2025], NLIPSat enables the encoding of polynomial nonlinear objective functions as weighted soft clauses and also supports the encoding of hard non-linear polynomial constraints within a polynomial setting. Extensive experiments on different benchmarks show that NLIPSat outperforms the state-of-the-art SMT solver Z3 by a wide margin.

In recent years, SAT solvers have been increasingly used in cryptanalysis, for performing attacks both on symmetric and asymmetric schemes. More specifically, they are employed whenever one needs to compute a valid assignment for a logical formula when running the attack. Most often, these formulae are initially represented in Algebraic Normal Form (ANF). Solvers dedicated to solving such instances translate the input formulae into a conjunction of CNF and XOR clauses and use different techniques such as XOR recovery and manipulation and Gaussian elimination. In this paper, we aim to build a solver able to reason directly on ANF formulae derived from attacks using Weil descent on Semaev polynomials of elliptic curves, while integrating dedicated lazy structures inspired from SAT solvers.

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 WMaxCDCLOpenWbo1200, the winner of the MaxSAT evaluation 2024 on the unweighted track, which is able to solve 15 additional instances using our methodology.

This paper explores the application of Maximum Satisfiability (Max-SAT) to the complex problem of conference session scheduling, with a particular focus on minimizing working-group conflicts within the context of the ROADEF conference, the largest French-speaking event aimed at bringing together researchers from various fields such as combinatorial optimization and operational research. A Max-SAT model is introduced then enhanced with new variables, and solved through state-of-the-art solvers. The results of applying our formulation to data from ROADEF demonstrate its ability to effectively compute session schedules, while enabling to reduce the number of conflicts and the maximum number of parallel sessions compared to the handmade solutions proposed by the organizing committees. These findings underscore the potential of Max-SAT as a valuable tool for optimizing conference scheduling processes, offering a systematic and efficient solution that ensures a smoother and more productive experience for attendees and organizers alike.

The Simple Assembly Line Balancing Problem with Power Peak Minimization (SALB3PM) is a relatively new problem that aims to assign tasks to workstations with a focus on minimizing power peaks. By integrating load balancing and task scheduling, this problem offers a comprehensive approach to enhancing energy efficiency in production systems, which can lead to significant cost savings alongside a positive environmental impact. This paper introduces novel models for SALB3PM based on Maximum Satisfiability (MaxSAT), the natural optimization extension of the Satisfiability problem, providing a new perspective to solve this optimization problem effectively. Experimental results demonstrate the efficiency and robustness of our approach with respect to the MaxSAT solvers applied. To the best of our knowledge, this is the first attempt to address the SALB3PM problem through the lens of Maximum Satisfiability.

In this paper, we present a tool, called MS-Builder, which generates certificates for the Max-SAT problem in the particular form of a sequence of equivalence-preserving transformations. To generate a certificate, MS-Builder iteratively calls a SAT oracle to get a SAT resolution refutation which is handled and adapted into a sound refutation for Max-SAT. In particular, the size of the computed Max-SAT refutation is linear with respect to the size of the initial refutation if it is semi-read-once, tree-like regular, tree-like or semi-tree-like. Additionally, we propose an extendable tool, called MS-Checker, able to verify the validity of any Max-SAT certificate using Max-SAT inference rules.

Adapting a SAT resolution proof into a Max-SAT resolution proof without considerably increasing its size is an open problem. Read-once resolution, where each clause is used at most once in the proof, represents the only fragment of resolution for which an adaptation using exclusively Max-SAT resolution is known and trivial. Proofs containing non read-once clauses are difficult to adapt because the Max-SAT resolution rule replaces the premises by the conclusions. This paper contributes to this open problem by defining, for the first time since the introduction of Max-SAT resolution, a new fragment of resolution whose proofs can be adapted to Max-SAT resolution proofs without substantially increasing their size. In this fragment, called crossing-free resolution, non read-once clauses are used independently to infer new information thus enabling to bring along each non read-once clause while unfolding the proof until a substitute is required.

Current Max-SAT solvers are able to efficiently compute the optimal value of an input instance but they do not provide any certificate of its validity. In this paper, we present a tool, called MS-Builder, which generates certificates for the Max-SAT problem in the particular form of a sequence of equivalence-preserving transformations. To generate a certificate, MS-Builder iteratively calls a SAT oracle to get a SAT resolution refutation which is handled and adapted into a sound refutation for Max-SAT. In particular, we prove that the size of the computed Max-SAT refutation is linear with respect to the size of the initial refutation if it is semi-read-once, tree-like regular, tree-like or semi-tree-like. Additionally, we propose an extendable tool, called MS-Checker, able to verify the validity of any Max-SAT certificate using Max-SAT inference rules. Both tools are evaluated on the unweighted and weighted benchmark instances of the 2020 Max-SAT Evaluation.

Conflict Driven Clause Learning (CDCL) solvers are known to be efficient on structured instances and manage to solve ones with a large number of variables and clauses. An important component in such solvers is the branching heuristic which picks the next variable to branch on. In this paper, we evaluate different strategies which combine two state-of-the-art heuristics, namely the Variable State Independent Decaying Sum (VSIDS) and the Conflict History-Based (CHB) branching heuristic. These strategies take advantage of the restart mechanism, which helps to deal with the heavy-tailed phenomena in SAT, to switch between these heuristics thus ensuring a better and more diverse exploration of the search space. Our experimental evaluation shows that combining VSIDS and CHB using restarts achieves competitive results and even significantly outperforms both heuristics for some chosen strategies.

Adapting a resolution refutation for SAT into a Max-SAT resolution refutation without increasing considerably the size of the refutation is an open question. This paper contributes to this topic by introducing an algorithm, called substitute generation, able to adapt any resolution refutation to get a Max-SAT refutation using SAT oracles. This algorithm is able to efficiently adapt k-stacked diamond patterns, whose transformation is exponential in the literature.

In this paper, we are interested in proof systems for Max-SAT and particularly in the construction of Max-SAT equivalence-preserving transformations to infer information from a given formula. To this end, we introduce the notion of explainability and we provide a characterization for explainable clauses and formulas. Furthermore, we introduce a new proof system, called Explanation Calculus (ExC) and composed of two rules: symmetric cut and expansion. We study the relation between ExC and several existing proof systems. Then, we introduce a new algorithm, called explanation algorithm, able to construct an explanation in ExC for any clause or refute its explainability and we extend it for formula explanations. Finally, we use our results on explainability to provide proofs for the Max-SAT problem with a new bound on the number of inference steps in the proof, improving the bound obtained with the Max-SAT resolution calculus.

Reinforcement learning has shown its relevance in designing search heuristics for backtracking algorithms dedicated to solving decision problems under constraints. Recently, an efficient heuristic, called Conflict History Search (CHS), based on the history of search failures was introduced for the Constraint Satisfaction Problem (CSP). The Exponential Recency Weighted Average (ERWA) is used to estimate the hardness of constraints and CHS favors the variables that often appear in recent failures. The step parameter is important in CHS since it controls the estimation of the hardness of constraints and its refinement may lead to notable improvements. The current research aims to achieve this objective. Indeed, a Multi-Armed Bandits (MAB) framework can select an appropriate value of this parameter during the restarts performed by the search algorithm. Each arm represents a CHS with a given value for the step parameter and it is rewarded by its ability to improve the search. A training phase is introduced earlier in the search to help MAB choose a relevant arm. The experimental evaluation shows that this approach leads to significant improvements regarding CHS and other state-of-the-art heuristics.

Adapting a resolution proof for SAT to a Max-SAT resolution proof without increasing considerably the size of the proof is an open question. This paper contributes to this topic by exhibiting linear adaptations, in terms of the input SAT proof size, in restricted cases which are regular tree resolution refutations, tree resolution refutations and a new introduced class of refutations that we refer to as semi-tree resolution refutations. We also extend these results by proposing a complete adaptation for any unrestricted SAT refutation to a Max-SAT refutation, which is exponential in the worst case.