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.

Given a maritime liner network, the cargo routing problem consists of determining which maritime routes containers will take to be transported from their loading port to their destination port. This constrained optimization problem is an essential task in the context of maritime commodity transportation, both in terms of network design and operational implementation. Several variants of this problem have been considered depending on their usage (e.g. for designing the network or for carrying containers in practice), the constraints taken into account or the criterion to be optimized. In this article, we address several variants of this problem, relying on the flexibility of Constraint Programming. First, we propose two general COP models. Then, we describe a local search method that can be easily adapted to the desired context. Finally, we experimentally compare our two models and the proposed method.

The liner shipping network design problem consists, for a shipowner, in determining, on the one hand, which maritime lines (in the form of rotations serving a set of ports) to open, and, on the other hand, the assignment of ships (container ships) with the adapted sizes for the different lines to carry all the container flows. In this paper, we propose a modeling of this problem using constraint programming. Then, we present a preliminary study of its solving using a state-of-the-art solver, namely the OR-Tools CP-SAT solver.

Bounded Variable Elimination (BVE) is an important Boolean formula simplification technique in which the variable ordering is crucial. We define a new variable ordering based on variable activity, called ESA (variable Elimination Scheduled by Activity), for in-processing BVE in Conflict-Driven Clause Learning (CDCL) SAT solvers, and incorporate it into several state-of-the-art CDCL SAT solvers. Experimental results show that the new ESA ordering consistently makes these solvers solve more instances on the benchmark set including all the 5675 instances used in the Crafted, Application and Main tracks of all SAT Competitions up to 2022. In particular, one of these solvers with ESA, Kissat_MAB_ESA, won the Anniversary track of the SAT Competition 2022. The behaviour of ESA and the reason of its effectiveness are also analyzed.

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.

Branch and Bound (BnB) has been successfully used to solve many combinatorial optimization problems. However, BnB MaxSAT solvers perform poorly when solving real-world and academic optimization problems. They are only competitive for random and some crafted instances. Thus, it is a prevailing opinion in the community that BnB is not really useful for practical MaxSAT solving. We refute this opinion by presenting a new BnB MaxSAT solver, called MaxCDCL, which combines clause learning and an efficient bounding procedure. MaxCDCL is among the top 5 out of a total of 15 exact solvers that participated in the 2020 MaxSAT Evaluation, solving several instances that other solvers cannot solve. Furthermore, MaxCDCL solves the highest number of instances from different MaxSAT Evaluations when combined with the best existing solvers.

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.

Branch and Bound (BnB) is a powerful technique that has been successfully used to solve many combinatorial optimization problems. However, MaxSAT is a notorious exception because BnB MaxSAT solvers perform poorly on many instances encoding interesting real-world and academic optimization problems. This has formed a prevailing opinion in the community stating that BnB is not so useful for MaxSAT, except for random and some special crafted instances. In fact, there has been no advance allowing to significantly speed up BnB MaxSAT solvers in the past few years, as illustrated by the absence of BnB solvers in the annual MaxSAT Evaluation since 2017. Our work aims to change this situation and proposes a new BnB MaxSAT solver, called MaxCDCL, by combining clause learning and an efficient bounding procedure. The experimental results show that, contrary to the prevailing opinion, BnB can be competitive for MaxSAT. MaxCDCL is ranked among the top 5 solvers of the 15 solvers that participated in the 2020 MaxSAT Evaluation, solving a number of instances that other solvers cannot solve. Furthermore, MaxCDCL, when combined with the best existing solvers, solves the highest number of instances of the MaxSAT Evaluations.

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.

Branch and Bound solvers for Max-SAT are very efficient on random and some crafted instances, as shown in the recent Max-SAT Evaluation results. However, on structured instances (particularly on the ones issued from industrial applications), they are significantly outperformed by other types of Max-SAT solvers. In the SAT context, CDLC solvers perform very well on industrial instances. One of the main reasons of this efficiency is the learning mechanism of nogood clauses, which has been introduced more than fifteen years ago. It allows solvers to learn from their failure with a twofold objective: limit redundancies and lead the exploration to the most promising areas of the search space. We propose in this paper a similar mechanism, which we call nobetter clause learning, adapted to BnB Max-SAT solvers. The results we have obtained show gains on industrial instances. These results call for more work in this direction, to further improve the quality of the information learned and make a better exploitation of them.

The Minimum Satisfiability Problem (MinSAT) consists in finding the minimum number of satisfied clauses of a CNF formula. This NP-hard problem is an extension of the famous SAT problem and has received less attention than its dual problem MaxSAT (Maximum Satisfiability). One of the MinSAT variants is the Partial MinSAT Problem where some clauses are hard and the others are soft. This variant is used to encode many optimization problems. Recent works on Partial MinSAT are only focused on its exact solving. In this paper, we propose a local search algorithm called GMinSAT to solve the Partial MinSAT Problem. It handles two opposite objectives: satisfying the hard clauses while minimizing the number of satisfied soft clauses. We compare empirically our proposed solver to the Branch & Bound solver MinSatz and show its interest on random and crafted instances. To the best of our knowledge, GMinSAT is the first genuine local search algorithm for this problem.

One of the most critical components of Branch & Bound (BnB) solvers for Max-SAT is the estimation of the lower bound. At each node of the search tree, they detect inconsistent subsets (IS) of the formula by unit propagation based methods and apply a treatment on them. Depending on the structure of the IS, current best performing BnB solvers transform them by several max-resolution steps and keep the changes in the sub-part of the sub tree or simply remove the clauses of these subsets from the formula and restore them before the next decision. The formula obtained after this last treatment is not equivalent to the original one and the number of detectable remaining inconsistencies may be reduced. In this paper, instead of applying such a removal, we propose to fully exploit all the inconsistent subsets by applying the well-known max-resolution inference rule to transform them locally in the current node of the search tree. The expected benefits of this transformation are an accurate lower bound estimation and the reduction of the number of decisions needed to solve an instance. We show experimentally the interest of our approach on weighted and unweighted Max-SAT instances and discuss the obtained results.

Unit propagation (UP) based method are widely used in Branch and Bound (BnB) Max-SAT solvers for detecting disjoint inconsistent subsets (IS) during the lower bound (LB) estimation. UP consists in assigning to true (propagating) all the literals which appear in unit clauses. The existing implementations of UP only consider the first unit clause causing the assignment of each variable, thus the propagations must be done and undone chronologically to ensure that all the unit clauses are properly exploited. Max-SAT BnB solvers transforms the formulas to ensure IS disjointness. These transformations remove clauses from the formula thus propagations are frequently undone. Since the propagations are undone in chronological order, many useless unassignments and reassignments are performed. We propose in this paper a new unit propagation scheme which considers all the unit clauses causing the assignment of the variables by UP. This new scheme allows to undo propagations in a non-chronological way and thus it reduces the number of redundant propagation steps made by BnB solvers. We also show how the information available with this new scheme can be used to influence the characteristics of the IS built by BnB solvers. We propose a heuristic which aims at reducing their size, and thus improving the quality of the LB estimation. We have implemented the new propagation scheme as well as the IS building heuristic in our solver MSsolver. We present and discuss the results of the experimental study we have performed.

In the last years, many advances were accomplished in the exact solving of the Max-SAT problem, especially by the definition of new inference rules and a better estimation of lower bounds in branch and bound based methods. However, and oppositely to the SAT problem, fewer works exist on approximate methods for Max-SAT, mainly local search ones which have shown their potency for SAT. In this paper, we illustrate that including inference rules in a classical local search solver for SAT improves its performances when solving the Max-SAT problem. The obtained results confirm the efficiency of our approach.

In this paper, we propose a local search method that integrates conflict analysis, usually used as part of complete search, to solve the satisfiability problem (SAT). This integration provides to the local search the following improvements: use of unit propagation, consideration of the dependencies between variables, clause learning and finally the ability to prove the unsatisfiability.

The main purpose of the paper is to solve structured instances of the satisfiability problem. The structure of a SAT instance is represented by an hypergraph, whose vertices correspond to the variables and the hyper-edges to the clauses. The proposed method is based on a tree decomposition of this hyper-graph which guides the enumeration process of a DPLL-like method. During the search, the method makes explicit some information which is recorded as structural goods and nogoods. By exploiting this information, the method avoids some redundancies in the search, and so it guarantees a bounded theoretical time complexity which is related to the tree-decomposition. Finally, the method is assessed on structured SAT benchmarks.

Walksat-like algorithms are considered among the most powerful local search methods to solve the satisfiability problem. Such algorithms introduce a diversification mechanism based on a random walk strategy. This one is controlled by a noise parameter for which the optimal value setting is strongly dependent on the treated instance. In this paper, we propose to extend a previous work in order to reduce the sensitivity of such algorithms to this setting. This task is accomplished by taking into account relations between variables and a cooperation with a DPLL-like procedure.

Most of the local search methods for the satisfiability problem deal with a complete and inconsistent truth assignment of the problem variables, and try to repair it by switching the truth value of some variables until reaching a model. We propose a new local search algorithm which works on partial truth assignments, but always consistent, instead of complete and inconsistent ones. This method attempts to extend a current partial assignment as a complete method would do. However, instead of backtracking when a conflict arises, it frees at least one variable involved in each falsified clause to restore consistency. Thus, the explored neighborhood is always consistent whereas it is not the case for classical local search algorithms. Experimental results show the competitiveness of our method towards other local search methods.

The problem of managing an Agile Earth Observing Satellite consists of selecting and scheduling a subset of photographs, among a set of candidate ones, satisfying imperative constraints and maximizing a gain function. In this paper, we propose a tabu search algorithm to solve the management problem of an Agile Earth Observing Satellite. This algorithm is an adaptation of CN-Tabu methodology working on a consistent neighborhood. Indeed, to obtain a wide-ranging and efficient exploration, the search space is sampled by consistent and saturated configurations. The consistency is maintained by constraint propagation and the saturation is a feature of the optimal solution. Furthermore, our tabu algorithm is hybridized with a systematic search, using partial enumerations, to solve several decisional problems. Moreover, for better resolution, a second objective problem, the minimization of the sum of transition durations between two image acquisitions, is introduced and tackled with a second tabu search algorithm.