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.

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.

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.

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.

As a classical NP-hard problem and the topic of the PACE 2022 competition, the directed feedback vertex set problem (DFVSP) aims to find a minimum subset of vertices such that, when vertices in the subset and all their adjacent edges are removed from the directed graph, the remainder graph is acyclic. In this paper, we propose a threshold-based responsive simulated annealing algorithm called TRSA for solving DFVSP. First, we simplify the problem instances with two new reduction rules proposed in this paper and eight reduction rules from the literature. Then, based on a new solution representation, TRSA solves DFVSP with a fast local search procedure featured by a swap-based neighborhood structure and three neighborhood acceleration strategies. Finally, all these strategies are incorporated into a threshold-based responsive simulated annealing framework. Computational experiments on 140 benchmark instances show that TRSA is highly competitive compared to the state-of-the-art methods. Specifically, TRSA can improve the best known results for 53 instances, while matching the best known results for 79 ones. Furthermore, some important features of TRSA are analyzed to identify its success factors.

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.

In many real-world problems and applications, finding only a single element, even though the best, among all possible candidates, cannot fully meet the requirements. We may wish to have a collection where each individual is not only outstanding but also distinctive. Diversified Top-k (DTk) problems are a kind of combinatorial optimization problem for finding such a promising collection of multiple sub-structures, such as subgraphs like cliques and social communities. In this paper, we address two representative DTk problems, DTk Clique search (DTkC) and DTk Weight Clique search (DTkWC), and propose a novel and effective algorithm called Diversified Top-k Evolutionary AlgorithM (DiverTEAM) for the two problems. DiverTEAM consists of a local search algorithm, which focuses on generating high-quality and diverse individuals and sub-structures, and a genetic algorithm that makes individuals work as a team and converge to (near-)optima efficiently. Extensive experiments show the excellent and robust performance of DiverTEAM across various benchmarks of DTkC and DTkWC.

Local search has been widely applied to solve the well-known (weighted) partial MaxSAT problem, significantly influencing many real-world applications. The main difficulty to overcome when designing a local search algorithm is that it can easily fall into local optima. Clause weighting is a beneficial technique that dynamically adjusts the landscape of search space to help the algorithm escape from local optima. Existing works tend to increase the weights of falsified clauses, and such strategies may result in an unpredictable landscape of search space during the optimization process. Therefore, in this paper, we propose a Unified Soft Clause Weighting Scheme called Unified-SW, which increases the weights of all soft clauses in feasible local optima, whether they are satisfied or not, while preserving the hierarchy among them. We implemented Unified-SW in a new local search solver called USW-LS. Experimental results demonstrate that USW-LS, outperforms the state-of-the-art local search solvers across benchmarks from anytime tracks of recent MaxSAT Evaluations. More promisingly, a hybrid solver combining USW-LS and TT-Open-WBO-Inc won all four categories in the anytime track of MaxSAT Evaluation 2023.

Maximum Common Induced Subgraph (MCIS) is an important NP-hard problem with wide real-world applications. An efficient class of MCIS algorithms uses Branch-and-Bound (BnB), consisting in successively selecting vertices to match and pruning when it is discovered that a solution better than the best solution found so far does not exist. The method of selecting the vertices to match is essential for the performance of BnB. In this paper, we propose a new value function and a hybrid selection strategy used in reinforcement learning to define a new vertex selection method, and propose a new BnB algorithm, called McSplitDAL, for MCIS. Extensive experiments show that McSplitDAL significantly improves the current best BnB algorithms, McSplit+LL and McSplit+RL. An empirical analysis is also performed to illustrate why the new value function and the hybrid selection strategy are effective.

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.

Proof systems for SAT are unsound for MaxSAT because they preserve satisfiability but fail to preserve the minimum number of unsatisfied clauses. Consequently, there has been a need to define cost-preserving resolution-style proof systems for MaxSAT. In this paper, we present the first MaxSAT resolution proof system specifically defined for regular propositional clausal forms and prove its soundness and completeness. The defined proof system provides an exact approach to solving Regular MaxSAT and Weighted Regular MaxSAT with variable elimination algorithms.

The diversified top-k weight clique (DTKWC) search problem is an important generalization of the diversified top-k clique (DTKC) search problem with extensive applications, which extends the DTKC search problem by taking into account the weight of vertices. In this paper, we formulate DTKWC search problem using mixed integer linear program constraints and propose an efficient hybrid evolutionary algorithm (HEA-D) that combines a clique-based crossover operator and an effective simulated annealing-based local optimization procedure to find high-quality local optima. The experimental results show that HEA-D performs much better than the existing methods on two representative real-world benchmarks.

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.

We address Partial MaxSAT (PMS) and Weighted PMS (WPMS), two practical generalizations of the MaxSAT problem, and propose a local search algorithm called BandMaxSAT, that applies a multi-armed bandit to guide the search direction, for these problems. The bandit in our method is associated with all the soft clauses in the input (W)PMS instance. Each arm corresponds to a soft clause. The bandit model can help BandMaxSAT to select a good direction to escape from local optima by selecting a soft clause to be satisfied in the current step, that is, selecting an arm to be pulled. We further propose an initialization method for (W)PMS that prioritizes both unit and binary clauses when producing the initial solutions. Extensive experiments demonstrate that BandMaxSAT significantly outperforms the state-of-the-art (W)PMS local search algorithm SATLike3.0. Specifically, the number of instances in which BandMaxSAT obtains better results is about twice that obtained by SATLike3.0. We further combine BandMaxSAT with the complete solver TT-Open-WBO-Inc. The resulting solver BandMaxSAT-c also outperforms some of the best state-of-the-art complete (W)PMS solvers, including SATLike-c, Loandra and TT-Open-WBO-Inc.

We propose a new and strengthened Branch-and-Bound (BnB) algorithm for the maximum common (connected) induced subgraph problem based on two new operators, Long-Short Memory (LSM) and Leaf vertex Union Match (LUM). Given two graphs for which we search for the maximum common (connected) induced subgraph, the first operator of LSM maintains a score for the branching node using the short-term reward of each vertex of the first graph and the long-term reward of each vertex pair of the two graphs. In this way, the BnB process learns to reduce the search tree size significantly and boost the algorithm performance. The second operator of LUM further improves the performance by simultaneously matching the leaf vertices connected to the current matched vertices, and allows the algorithm to match multiple vertex pairs without affecting the optimality of solution. We incorporate the two operators into the state-of-the-art BnB algorithm McSplit, and denote the resulting algorithm as McSplit+LL. Experiments show that McSplit+LL outperforms McSplit+RL, a more recent variant of McSplit using reinforcement learning that is superior than McSplit.

The Vertex Bisection Minimization Problem (VBMP) is a relevant graph partitioning model with a variety of practical applications. This work introduces a clustering driven iterated hybrid search algorithm (CLUHS), which is the first approach that applies clustering to reinforce iterated local search for solving VBMP. The proposed CLUHS uses hierarchical clustering to build an initial solution, guide local search process and perform search diversification. Experimental studies on 137 benchmark instances show the high competitiveness of the proposed approach compared to the state-of-the-art methods. In particular, CLUHS finds new record-breaking solutions for 18 instances.

The optimal camera placement problem (OCP) aims to accomplish surveillance tasks with the minimum number of cameras, which is one of the topics in the GECCO 2020 Competition and can be modeled as the unicost set covering problem (USCP). This paper presents a weighting-based variable neighborhood search (WVNS) algorithm for solving OCP. First, it simplifies the problem instances with four reduction rules based on dominance and independence. Then, WVNS converts the simplified OCP into a series of decision unicost set covering subproblems and tackles them with a fast local search procedure featured by a swap-based neighborhood structure. WVNS employs an efficient incremental evaluation technique and further boosts the neighborhood evaluation by exploiting the dominance and independence features among neighborhood moves. Computational experiments on the 69 benchmark instances introduced in the GECCO 2020 Competition on OCP and USCP show that WVNS is extremely competitive comparing to the state-of-the-art methods. It outperforms or matches several best performing competitors on all instances in both the OCP and USCP tracks of the competition, and its advantage on 15 large-scale instances are over 10%. In addition, WVNS improves the previous best known results for 12 classical benchmark instances in the literature.

We address the Traveling Salesman Problem (TSP), a famous NP-hard combinatorial optimization problem. And we propose a variable strategy reinforced approach, denoted as VSR-LKH, which combines three reinforcement learning methods (Q-learning, Sarsa and Monte Carlo) with the well-known TSP algorithm, called Lin-Kernighan-Helsgaun (LKH). VSR-LKH replaces the inflexible traversal operation in LKH, and lets the program learn to make choice at each search step by reinforcement learning. Experimental results on 111 TSP benchmarks from the TSPLIB with up to 85,900 cities demonstrate the excellent performance of the proposed method.

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.

The performance of a branch-and-bound (BnB) algorithm for maximum common subgraph (MCS) problem and its related problems, like maximum common connected subgraph (MCCS) and induced Subgraph Isomorphism (SI), crucially depends on the branching heuristic. We propose a branching heuristic inspired from reinforcement learning with a goal of reaching a tree leaf as early as possible to greatly reduce the search tree size. Experimental results show that the proposed heuristic consistently and significantly improves the current best BnB algorithm for the MCS, MCCS and SI problems. An analysis is carried out to give insight on why and how reinforcement learning is useful in the new branching heuristic.

The p-center problem consists of choosing p centers from a set of candidates to minimize the maximum cost between any client and its assigned facility. In this paper, we transform the p-center problem into a series of set covering subproblems, and propose a vertex weighting-based tabu search (VWTS) algorithm to solve them. The proposed VWTS algorithm integrates distinguishing features such as a vertex weighting technique and a tabu search strategy to help the search to jump out of the local optima. Computational experiments on 138 most commonly used benchmark instances show that VWTS is highly competitive comparing to the state-of-the-art methods in spite of its simplicity. As a well-known NP-hard problem which has already been studied for over half a century, it is a challenging task to break the records on these classic datasets. Yet VWTS improves the best known results for 14 out of 54 large instances, and matches the optimal results for all remaining 84 ones. In addition, the computational time taken by VWTS is much shorter than other algorithms in the literature.

Population-based evolutionary algorithms usually manage a large number of individuals to maintain the diversity of the search, which is complex and time-consuming. In this paper, we propose an evolutionary algorithm using only two individuals, called master-apprentice evolutionary algorithm (MAE), for solving the flexible job shop scheduling problem (FJSP). To ensure the diversity and the quality of the evolution, MAE integrates a tabu search procedure, a recombination operator based on path relinking using a novel distance definition, and an effective individual updating strategy, taking into account the multiple complex constraints of FJSP. Experiments on 313 widely-used public instances show that MAE improves the previous best known results for 47 instances and matches the best known results on all except 3 of the remaining instances while consuming the same computational time as current state-of-the-art metaheuristics. MAE additionally establishes solution quality records for 10 hard instances whose previous best values were established by a well-known industrial solver and a state-of-the-art exact method.

MaxSAT reasoning is an effective technology used in modern branch-and-bound (BnB) algorithms for the Maximum Weight Clique problem (MWC) to reduce the search space. However, the current MaxSAT reasoning approach for MWC is carried out in a blind manner and is not guided by any relevant strategy. In this paper, we describe a new BnB algorithm for MWC that incorporates a novel two-stage MaxSAT reasoning approach. In each stage, the MaxSAT reasoning is specialised and guided for different tasks. Experiments on an extensive set of graphs show that the new algorithm implementing this approach significantly outperforms relevant exact and heuristic MWC algorithms in both small/medium and massive real-world graphs.

The maximum clique problem (MaxClique for short) consists of searching for a maximum complete subgraph in a graph. A branch-and-bound (BnB) MaxClique algorithm computes an upper bound of the number of vertices of a maximum clique at every search tree node, to prune the subtree rooted at the node. Existing upper bounds are usually computed from scratch at every search tree node. In this paper, we define an incremental upper bound, called IncUB, which is derived efficiently from previous searches instead of from scratch. Then, we describe a new BnB MaxClique algorithm, called IncMC2, which uses graph coloring and MaxSAT reasoning to filter out the vertices that do not need to be branched on, and uses IncUB to prune the remaining branches. Our experimental results show that IncMC2 is significantly faster than algorithms such as BBMC and IncMaxCLQ. Finally, we carry out experiments to provide evidence that the performance of IncMC2 is due to IncUB. The online supplement is available at https://doi.org/10.1287/ijoc.2017.0770 .

We describe an exact branch-and-bound algorithm for the maximum weight clique problem (MWC), called WLMC, that is especially suited for large vertex-weighted graphs. WLMC incorporates two original contributions: a preprocessing to derive an initial vertex ordering and to reduce the size of the graph, and incremental vertex-weight splitting to reduce the number of branches in the search space. Experiments on representative large graphs from real-world applications show that WLMC greatly outperforms relevant exact and heuristic MWC algorithms, and refute the prevailing hypothesis that exact MWC algorithms are less adequate for large graphs than heuristic algorithms.

The Minimum Sum Coloring Problem (MSCP) is an NP-Hard problem derived from the graph coloring problem (GCP) and has practical applications in different domains such as VLSI design, distributed resource allocation, and scheduling. There exist few exact solutions for MSCP, probably due to its search space much more elusive than that of GCP. On the contrary, much effort is spent in the literature to develop upper and lower bounds for MSCP. In this paper, we borrow a notion called motif, that was used in a recent work for upper bounding the minimum number of colors in an optimal solution of MSCP, to develop a new algebraic lower bound called for MSCP. Experiments on standard benchmarks for MSCP and GCP show that this new lower bound is substantially better than the existing lower bounds for several families of graphs.

Learnt clauses in CDCL SAT solvers often contain redundant literals. This may have a negative impact on performance because redundant literals may deteriorate both the effectiveness of Boolean constraint propagation and the quality of subsequent learnt clauses. To overcome this drawback, we define a new inprocessing SAT approach which eliminates redundant literals from learnt clauses by applying Boolean constraint propagation. Learnt clause minimization is activated before the SAT solver triggers some selected restarts, and affects only some learnt clauses during the search process. Moreover, we conducted an empirical evaluation on instances coming from the hard combinatorial and application categories of recent SAT competitions. The results show that a remarkable number of additional instances are solved when the approach is incorporated into five of the best performing CDCL SAT solvers (Glucose, TC_Glucose, COMiniSatPS, MapleCOMSPS and MapleCOMSPS_LRB).

We describe a new exact algorithm for MaxClique, called LMC (short for Large MaxClique), that is especially suited for large sparse graphs. LMC is competitive because it combines an efficient preprocessing procedure and incremental MaxSAT reasoning in a branch-and-bound scheme. The empirical results show that LMC outperforms existing exact MaxClique algorithms on large sparse graphs from real-world applications.

Recently, MaxSAT reasoning is shown very effective in computing a tight upper bound for a Maximum Clique (MC) of a (unweighted) graph. In this paper, we apply MaxSAT reasoning to compute a tight upper bound for a Maximum Weight Clique (MWC) of a wighted graph. We first study three usual encodings of MWC into weighted partial MaxSAT dealing with hard clauses, which must be satisfied in all solutions, and soft clauses, which are weighted and can be falsified. The drawbacks of these encodings motivate us to propose an encoding of MWC into a special weighted partial MaxSAT formalism, called LW (Literal-Weighted) encoding and dedicated for upper bounding an MWC, in which both soft clauses and literals in soft clauses are weighted. An optimal solution of the LW MaxSAT instance gives an upper bound for an MWC, instead of an optimal solution for MWC. We then introduce two notions called the Top-k literal failed clause and the Top-k empty clause to extend classical MaxSAT reasoning techniques, as well as two sound transformation rules to transform an LW MaxSAT instance. Successive transformations of an LW MaxSAT instance driven by MaxSAT reasoning give a tight upper bound for the encoded MWC. The approach is implemented in a branch-and-bound algorithm called MWCLQ. Experimental evaluations on the broadly used DIMACS benchmark, BHOSLIB benchmark, random graphs and the benchmark from the winner determination problem show that our approach allows MWCLQ to reduce the search space significantly and to solve MWC instances effectively. Consequently, MWCLQ outperforms state-of-the-art exact algorithms on the vast majority of instances. Moreover, it is surprisingly effective in solving hard and dense instances.

Satisfiability (SAT) and maximum satisfiability (MaxSAT) techniques are proved to be powerful in solving combinatorial optimization problems. In this paper, we encode the maximum weight clique (MWC) problem into weighted partial MaxSAT and use MaxSAT techniques to solve it. Concretely, we propose a new algorithm based on MaxSAT reasoning called Top-k failed literal detection to improve the upper bound for MWC, and implement an exact branch-and-bound solver for the MWC problem called MaxWClq based on the Top-k failed literal detection algorithm. To our best knowledge, this is the first time that MaxSat techniques are integrated to solve the MWC problem. Experimental evaluations on the broadly used DIMACS benchmark, BHOSLIB benchmark and random graphs show that MaxWClq outperforms state-of-the-art exact algorithms on the vast majority of instances. In particular, our algorithm is surprisingly powerful for dense and hard graphs.

Recently, MaxSAT reasoning has been shown to be powerful in computing upper bounds for the cardinality of a maximum clique of a graph. However, existing upper bounds based on MaxSAT reasoning have two drawbacks: (1)at every node of the search tree, MaxSAT reasoning has to be performed from scratch to compute an upper bound and is time-consuming, (2) due to the NP-hardness of the MaxSAT problem, MaxSAT reasoning generally cannot be complete at anode of a search tree, and may not give an upper bound tight enough for pruning search space. In this paper, we propose an incremental upper bound and combine it with MaxSAT reasoning to remedy the two drawbacks. The new approach is used to develop an efficient branch-and-bound algorithm for MaxClique, called IncMaxCLQ. We conduct experiments to show the complementarity of the incremental upper bound and MaxSAT reasoning and to compare IncMaxCLQ with several state-of-the-art algorithms for MaxClique.

State-of-the-art branch-and-bound algorithms for the maximum clique problem (Maxclique) frequently use an upper bound based on a partition P of a graph into independent sets for a maximum clique of the graph, which cannot be very tight for imperfect graphs. In this paper we propose a new encoding from Maxclique into MaxSAT and use MaxSAT technology to improve the upper bound based on the partition P. In this way, the strength of specific algorithms for Maxclique in partitioning a graph and the strength of MaxSAT technology in propositional reasoning are naturally combined to solve Maxclique. Experimental results show that the approach is very effective on hard random graphs and on DIMACS Maxclique benchmarks, and allows to close an open DIMACS problem.

State-of-the-art branch-and-bound algorithms for the maximum clique problem (Maxclique) generally exploit the structural information of a graph G to partition G into independent sets, in order to derive an upper bound for the cardinality of a maximum clique of G, which cannot be very tight for imperfect graphs. On the other hand, while Maxclique can be easily encoded into MaxSAT to be solved using a MaxSAT solver, general-purpose MaxSAT solvers are not competitive for solving Maxclique, because they do not exploit the structural information of the graph. Recently, we have shown that propositional reasoning developed for the MaxSAT solvers can be used to improve the upper bound based on the partition. In this paper, we propose and study several improvements to this approach by better combining graph structure exploitation and propositional reasoning to solve Maxclique. Experimental results show that the improvements are very effective on hard random graphs and on DIMACS Maxclique benchmarks which are widely used to evaluate branch-and-bound algorithms for Maxclique.

Exact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability but, unfortunately, solving the Max-SAT problem for the simplified formula is not equivalent to solving it for the original formula. In this paper, we define a number of original inference rules that, besides being applied efficiently, transform Max-SAT instances into equivalent Max-SAT instances which are easier to solve. The soundness of the rules, that can be seen as refinements of unit resolution adapted to Max-SAT, are proved in a novel and simple way via an integer programming transformation. With the aim of finding out how powerful the inference rules are in practice, we have developed a new Max-SAT solver, called MaxSatz, which incorporates those rules, and performed an experimental investigation. The results provide empirical evidence that MaxSatz is very competitive, at least, on random Max-2SAT, random Max-3SAT, Max-Cut, and Graph 3-coloring instances, as well as on the benchmarks from the Max-SAT Evaluation 2006.

A mobile ad-hoc network is considered as a dynamic autonomous system composed of mobile devices interconnected by links without wire, without the use of a fixed infrastructure and without centralized administration. The absence of a centralized infrastructure forces each device to work in a peer to peer distributed environment, and to act as a router to relay communications, or to generate its own data. The management of the network thus is strongly distributed on all elements of the network. In this paper, we present a modelling of the Mobile Ad-hoc NETwork (MANET) problem in form of a Constraint Satisfaction/ Optimization Problem called CSPADhoc. Then, to minimize the consumption of batteries for devices, we describe an approach based on an adaptation of the A star algorithm to the MANET problem called (MANET-Astar). Finally, we present some experimental results using our approach.