Author name cluster

Felip Manyà

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

25 papers

2 author rows

AAAI Conference 2025 Conference Paper

Improving the Lower Bound in Branch-and-Bound Algorithms for MaxSAT

Shuolin Li
Chu-Min Li
Jordi Coll
Djamal Habet
Felip Manyà

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.

PDF Details DOI

AIJ Journal 2025 Journal Article

Integrating multi-armed bandit with local search for MaxSAT

Jiongzhi Zheng
Kun He
Jianrong Zhou
Yan Jin
Chu-Min Li
Felip Manyà

Partial MaxSAT (PMS) and Weighted PMS (WPMS) are two practical generalizations of the MaxSAT problem. In this paper, we introduce a new local search algorithm for these problems, named BandHS. It applies two multi-armed bandit (MAB) models to guide the search directions when escaping local optima. One MAB model is combined with all the soft clauses to help the algorithm select to satisfy appropriate soft clauses, while the other MAB model is combined with all the literals in hard clauses to help the algorithm select suitable literals to satisfy the hard clauses. These two models enhance the algorithm's search ability in both feasible and infeasible solution spaces. BandHS also incorporates a novel initialization method that prioritizes both unit and binary clauses when generating the initial solutions. Moreover, we apply our MAB approach to the state-of-the-art local search algorithm NuWLS and to the local search component of the incomplete solver NuWLS-c-2023. The extensive experiments conducted demonstrate the excellent performance and generalization capability of the proposed method. Additionally, we provide analyses on the type of problems where our MAB method works well or not, aiming to offer insights and suggestions for its application. Encouragingly, our MAB method has been successfully applied in core local search components in the winner of the WPMS complete track of MaxSAT Evaluation 2023, as well as the runners-up of the incomplete track of MaxSAT Evaluations 2022 and 2023.

Details DOI

IJCAI Conference 2023 Conference Paper

A New Variable Ordering for In-processing Bounded Variable Elimination in SAT Solvers

Shuolin Li
Chu-Min Li
Mao Luo
Jordi Coll
Djamal Habet
Felip Manyà

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.

PDF Details DOI

IJCAI Conference 2022 Conference Paper

BandMaxSAT: A Local Search MaxSAT Solver with Multi-armed Bandit

Jiongzhi Zheng
Kun He
Jianrong Zhou
Yan Jin
Chu-Min Li
Felip Manyà

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.

PDF Details DOI

IJCAI Conference 2022 Conference Paper

Combining Clause Learning and Branch and Bound for MaxSAT (Extended Abstract)

Chu-Min Li
Zhenxing Xu
Jordi Coll
Felip Manyà
Djamal Habet
Kun He

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.

PDF Details DOI

AIJ Journal 2020 Journal Article

Clause vivification by unit propagation in CDCL SAT solvers

Chu-Min Li
Fan Xiao
Mao Luo
Felip Manyà
Zhipeng Lü
Yu Li

Original and learnt clauses in Conflict-Driven Clause Learning (CDCL) SAT solvers often contain redundant literals. This may have a negative impact on solver 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 propose a clause vivification approach that eliminates redundant literals by applying unit propagation. The proposed clause vivification is activated before the SAT solver triggers some selected restarts, and only affects a subset of original and learnt clauses, which are considered to be more relevant according to metrics like the literal block distance (LBD). Moreover, we conducted an empirical investigation with instances coming from the hard combinatorial and application categories of recent SAT competitions. The results show that a significant number of additional instances are solved when the proposed approach is incorporated into five of the best performing CDCL SAT solvers (Glucose, TC_Glucose, COMiniSatPS, MapleCOMSPS and MapleCOMSPS_LRB). More importantly, the empirical investigation includes an in-depth analysis of the effectiveness of clause vivification. It is worth mentioning that one of the SAT solvers described here was ranked first in the main track of SAT Competition 2017 thanks to the incorporation of the proposed clause vivification. That solver was further improved in this paper and won the bronze medal in the main track of SAT Competition 2018.

Details DOI

AAAI Conference 2018 Conference Paper

A Two-Stage MaxSAT Reasoning Approach for the Maximum Weight Clique Problem

Hua Jiang
Chu-Min Li
Yanli Liu
Felip Manyà

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 signiﬁcantly outperforms relevant exact and heuristic MWC algorithms in both small/medium and massive real-world graphs.

PDF Details

IJCAI Conference 2017 Conference Paper

An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers

Mao Luo
Chu-Min Li
Fan Xiao
Felip Manyà
Zhipeng Lü

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).

PDF Details

ECAI Conference 2016 Conference Paper

Combining Efficient Preprocessing and Incremental MaxSAT Reasoning for MaxClique in Large Graphs

Hua Jiang
Chu-Min Li 0001
Felip Manyà

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.

Details

AIJ Journal 2012 Journal Article

Optimizing with minimum satisfiability

Chu Min Li
Zhu Zhu
Felip Manyà
Laurent Simon

MinSAT is the problem of finding a truth assignment that minimizes the number of satisfied clauses in a CNF formula. When we distinguish between hard and soft clauses, and soft clauses have an associated weight, then the problem, called Weighted Partial MinSAT, consists in finding a truth assignment that satisfies all the hard clauses and minimizes the sum of weights of satisfied soft clauses. In this paper we describe a branch-and-bound solver for Weighted Partial MinSAT equipped with original upper bounds that exploit both clique partitioning algorithms and MaxSAT technology. Then, we report on an empirical investigation that shows that solving combinatorial optimization problems by reducing them to MinSAT is a competitive generic problem solving approach when solving MaxClique and combinatorial auction instances. Finally, we investigate an interesting correlation between the minimum number and the maximum number of satisfied clauses on random CNF formulae.

Details DOI

AAAI Conference 2012 Conference Paper

The Automated Vacuum Waste Collection Optimization Problem

Ramón Béjar
César Fernández
Carles Mateu
Felip Manyà
Francina Sole-Mauri
David Vidal

One of the most challenging problems on modern urban planning and one of the goals to be solved for smart city design is that of urban waste disposal. Given urban population growth, and that the amount of waste generated by each of us citizens is also growing, the total amount of waste to be collected and treated is growing dramatically (EPA 2011), becoming one sensitive issue for local governments. A modern technique for waste collection that is steadily being adopted is automated vacuum waste collection. This technology uses air suction on a closed network of underground pipes to move waste from the collection points to the processing station, reducing greenhouse gas emissions as well as inconveniences to citizens (odors, noise, .. .) and allowing better waste reuse and recycling. This technique is open to optimize energy consumption because moving huge amounts of waste by air impulsion requires a lot of electric power. The described problem challenge here is, precisely, that of organizing and scheduling waste collection to minimize the amount of energy per ton of collected waste in such a system via the use of Artificial Intelligence techniques. This kind of problems are an inviting opportunity to showcase the possibilities that AI for Computational Sustainability offers.

PDF Details

SAT Conference 2011 Conference Paper

Analyzing the Instances of the MaxSAT Evaluation

Josep Argelich
Chu-Min Li 0001
Felip Manyà
Jordi Planes

Abstract The MaxSAT Evaluation [1] is an affiliated event of the SAT Conference that is held every year since 2006, and is devoted to empirically evaluate exact MaxSAT algorithms solving any of the following problems: MaxSAT, Weighted MaxSAT (WMaxSAT), Partial MaxSAT (PMaxSAT), and Weighted Partial MaxSAT (WPMaxSAT).

Details

SAT Conference 2010 Conference Paper

Exact MinSAT Solving

Chu-Min Li 0001
Felip Manyà
Zhe Quan
Zhu Zhu

Abstract We present an original approach to exact MinSAT solving based on solving MinSAT using MaxSAT encodings and MaxSAT solvers, and provide empirical evidence that our generic approach is competitive.

Details

SAT Conference 2009 Conference Paper

Exploiting Cycle Structures in Max-SAT

Chu-Min Li 0001
Felip Manyà
Nouredine Ould Mohamedou
Jordi Planes

Abstract We investigate the role of cycles structures (i. e. , subsets of clauses of the form \(\bar{l}_{1}\vee l_{2}, \bar{l}_{1}\vee l_{3}, \bar{l}_{2}\vee\bar{l}_{3}\) ) in the quality of the lower bound (LB) of modern MaxSAT solvers. Given a cycle structure, we have two options: (i) use the cycle structure just to detect inconsistent subformulas in the underestimation component, and (ii) replace the cycle structure with \(\bar{l}_{1}, l_{1}\vee\bar{l}_{2}\vee\bar{l}_{3}, \bar{l}_{1}\vee l_{2}\vee l_{3}\) by applying MaxSAT resolution and, at the same time, change the behaviour of the underestimation component. We first show that it is better to apply MaxSAT resolution to cycle structures occurring in inconsistent subformulas detected using unit propagation or failed literal detection. We then propose a heuristic that guides the application of MaxSAT resolution to cycle structures during failed literal detection, and evaluate this heuristic by implementing it in MaxSatz, obtaining a new solver called MaxSatz c. Our experiments on weighted MaxSAT and Partial MaxSAT instances indicate that MaxSatz c substantially improves MaxSatz on many hard random, crafted and industrial instances.

Details

SAT Conference 2009 Conference Paper

Sequential Encodings from Max-CSP into Partial Max-SAT

Josep Argelich
Alba Cabiscol
Inês Lynce
Felip Manyà

Abstract We define new encodings from Max-CSP into Partial Max-SAT which are obtained by modelling the at-most-one condition with the sequential SAT encoding of the cardinality constraint ≤ 1 ( x 1, .. ., x n ). They have fewer clauses than the existing encodings, and the experimental results indicate that they have a better performance profile.

Details

SAT Conference 2008 Conference Paper

A Preprocessor for Max-SAT Solvers

Josep Argelich
Chu-Min Li 0001
Felip Manyà

Abstract We describe a preprocessor that incorporates a variable saturation procedure for Max-SAT, and provide empirical evidence that it improves the performance of some of the most successful state-of-the-art solvers on several partial (weighted) Max-SAT instances of the 2007 Max-SAT Evaluation.

Details

SAT Conference 2008 Conference Paper

Modelling Max-CSP as Partial Max-SAT

Josep Argelich
Alba Cabiscol
Inês Lynce
Felip Manyà

Abstract We define a number of original encodings that map Max-CSP instances into partial Max-SAT instances. Our encodings rely on the well-known direct and support encodings from CSP into SAT. Then, we report on an experimental investigation that was conducted to compare the performance profile of our encodings on random binary Max-CSP instances. Moreover, we define a new variant of the support encoding from CSP into SAT which produces fewer clauses than the standard support encoding.

Details

SAT Conference 2007 Conference Paper

Mapping CSP into Many-Valued SAT

Carlos Ansótegui
Maria Luisa Bonet
Jordi Levy
Felip Manyà

Abstract We first define a mapping from CSP to many-valued SAT which allows to solve CSP instances with many-valued SAT solvers. Second, we define a new many-valued resolution rule and prove that it is refutation complete for many-valued CNF formulas and, moreover, enforces CSP ( i, j )-consistency when applied to a many-valued SAT encoding of a CSP. Instances of our rule enforce well-known local consistency properties such as arc consistency and path consistency.

Details

SAT Conference 2007 Conference Paper

Partial Max-SAT Solvers with Clause Learning

Josep Argelich
Felip Manyà

Abstract We describe three original exact solvers for Partial Max-SAT: PMS, PMS-hard, and PMS-learning. PMS is a branch and bound solver which incorporates efficient data structures, a dynamic variable selection heuristic, inference rules which exploit the fact that some clauses are hard, and a good quality lower bound based on unit propagation. PMS-hard is built on top of PMS and incorporates clause learning only for hard clauses; this learning is similar to the learning incorporated into modern SAT solvers. PMS-learning is built on top of PMS-hard and incorporates learning on both hard and soft clauses; the learning on soft clauses is quite different from the learning on SAT since it has to use Max-SAT resolution instead of SAT resolution. Finally, we report on the experimental investigation in which we compare the state-of-the-art solvers Toolbar and ChaffBS with PMS, PMS-hard, and PMS-learning. The results obtained provide empirical evidence that Partial Max-SAT is a suitable formalism for representing and solving over-constrained problems, and that the learning techniques we have defined in this paper can give rise to substantial performance improvements.

Details

AIJ Journal 2007 Journal Article

Resolution for Max-SAT

María Luisa Bonet
Jordi Levy
Felip Manyà

Max-SAT is the problem of finding an assignment minimizing the number of unsatisfied clauses in a CNF formula. We propose a resolution-like calculus for Max-SAT and prove its soundness and completeness. We also prove the completeness of some refinements of this calculus. From the completeness proof we derive an exact algorithm for Max-SAT and a time upper bound. We also define a weighted Max-SAT resolution-like rule, and show how to adapt the soundness and completeness proofs of the Max-SAT rule to the weighted Max-SAT rule. Finally, we give several particular Max-SAT problems that require an exponential number of steps of our Max-SAT rule to obtain the minimal number of unsatisfied clauses of the combinatorial principle. These results are based on the corresponding resolution lower bounds for those particular problems.

Details DOI

SAT Conference 2006 Conference Paper

A Complete Calculus for Max-SAT

Maria Luisa Bonet
Jordi Levy
Felip Manyà

Abstract Max-SAT is the problem of finding an assignment minimizing the number of unsatisfied clauses of a given CNF formula. We propose a resolution-like calculus for Max-SAT and prove its soundness and completeness. We also prove the completeness of some refinements of this calculus. From the completeness proof we derive an exact algorithm for Max-SAT and a time upper bound.

Details

SAT Conference 2005 Conference Paper

Improved Exact Solvers for Weighted Max-SAT

Teresa Alsinet
Felip Manyà
Jordi Planes

Abstract We present two new branch and bound weighted Max-SAT solvers ( Lazy and Lazy *) which incorporate original data structures and inference rules, and a lower bound of better quality.

Details

SAT Conference 2005 Conference Paper

Solving Over-Constrained Problems with SAT Technology

Josep Argelich
Felip Manyà

Abstract We present a new generic problem solving approach for over-constrained problems based on Max-SAT. We first define a clausal form formalism that deals with blocks of clauses instead of individual clauses, and that allows one to declare each block either as hard (i. e. , must be satisfied by any solution) or soft (i. e. , can be violated by some solution). We then present two Max-SAT solvers that find a truth assignment that satisfies all the hard blocks of clauses and the maximum number of soft blocks of clauses. Our solvers are branch and bound algorithms equipped with original lazy data structures; the first one incorporates static variable selection heuristics while the second one incorporates dynamic variable selection heuristics. Finally, we present an experimental investigation to assess the performance of our approach on a representative sample of instances (random 2-SAT, Max-CSP, and graph coloring).

Details

SAT Conference 2004 Conference Paper

Mapping Problems with Finite-Domain Variables into Problems with Boolean Variables

Carlos Ansótegui
Felip Manyà

We define a collection of mappings that transform many-valued clausal forms into satisfiability equivalent Boolean clausal forms, analyze their complexity and evaluate them empirically on a set of benchmarks with state-of-the-art SAT solvers. Our results provide empirical evidence that encoding combinatorial problems with the mappings defined here can lead to substantial performance improvements in complete SAT solvers.

Details

LPAR Conference 1999 Conference Paper

Solving Combinatorial Problems with Regular Local Search Algorithms

Ramón Béjar
Felip Manyà

Abstract In this paper we describe new local search algorithms for regular CNF formulas and investigate their suitability for solving problems from the domains of graph coloring and sports scheduling. First, we define suitable encodings for such problems in the logic of regular CNF formulas. Second, we describe Regular-GSAT and Regular-WSAT, as well as some variants, which are a natural generalization of two prominent local search algorithms -GSAT and WSAT- used to solve the prepositional satisfiability (SAT) problem in classical logic. Third, we report on experimental results that demonstrate that encoding graph coloring and sports scheduling problems as instances of the SAT problem in regular CNF formulas and then solving these instances with local search algorithms can outperform or compete with state-of-the-art approaches to solving hard combinatorial problems.

Details