Author name cluster

Jordi Coll

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.

9 papers

1 author row

AAAI Conference 2026 Conference Paper

Certified Branch-and-Bound MaxSAT Solving

Dieter Vandesande
Jordi Coll
Bart Bogaerts

Over the past few decades, combinatorial solvers have seen remarkable performance improvements, enabling their practical use in real-world applications. In some of these applications, ensuring the correctness of the solver's output is critical. However, the complexity of modern solvers makes them susceptible to bugs in their source code. In the domain of satisfiability checking (SAT), this issue has been addressed through proof logging, where the solver generates a formal proof of the correctness of its answer. For more expressive problems like MaxSAT, the optimization variant of SAT, proof logging had not seen a comparable breakthrough until recently. In this paper, we show how to achieve proof logging for state-of-the-art techniques in Branch-and-Bound MaxSAT solving. This includes certifying look-ahead methods used in such algorithms as well as advanced clausal encodings of pseudo-Boolean constraints based on so-called Multi-Valued Decision Diagrams (MDDs). We implement these ideas in MaxCDCL, the dominant branch-and-bound solver, and experimentally demonstrate that proof logging is feasible with limited overhead, while proof checking remains a challenge.

PDF Details DOI

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

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 2023 Conference Paper

Constraint Solving Approaches to the Business-to-Business Meeting Scheduling Problem (Extended Abstract)

Miquel Bofill
Jordi Coll
Marc Garcia
Jesús Giráldez-Cru
Gilles Pesant
Josep Suy
Mateu Villaret

The B2B Meeting Scheduling Optimization Problem (B2BSP) consists of scheduling a set of meetings between given pairs of participants to an event, minimizing idle time periods in participants' schedules, while taking into account participants’ availability and accommodation capacity. Therefore, it constitutes a challenging combinatorial problem in many real-world B2B events. This work presents a comparative study of several approaches to solve this problem. They are based on Constraint Programming (CP), Mixed Integer Programming (MIP) and Maximum Satisfiability (MaxSAT). The CP approach relies on using global constraints and has been implemented in MiniZinc to be able to compare CP, Lazy Clause Generation and MIP as solving technologies in this setting. A pure MIP encoding is also presented. Finally, an alternative viewpoint is considered under MaxSAT, showing the best performance when considering some implied constraints. Experimental results on real world B2B instances, as well as on crafted ones, show that the MaxSAT approach is the one with the best performance for this problem, exhibiting better solving times, sometimes even orders of magnitude smaller than CP and MIP.

PDF Details DOI

IJCAI Conference 2023 Conference Paper

SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints (Extended Abstract)

Miquel Bofill
Jordi Coll
Peter Nightingale
Josep Suy
Felix Ulrich-Oltean
Mateu Villaret

When solving a combinatorial problem using propositional satisfiability (SAT), the encoding of the constraints is of vital importance. Pseudo-Boolean (PB) constraints appear frequently in a wide variety of problems. When PB constraints occur together with at-most-one (AMO) constraints over the same variables, they can be combined into PB(AMO) constraints. In this paper we present new encodings for PB(AMO) constraints. Our experiments show that these encodings can be substantially smaller than those of PB constraints and allow many more instances to be solved within a time limit. We also observed that there is no single overall winner among the considered encodings, but efficiency of each encoding may depend on PB(AMO) characteristics such as the magnitude of coefficient values.

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

JAIR Journal 2022 Journal Article

Constraint Solving Approaches to the Business-to-Business Meeting Scheduling Problem

Miquel Bofill
Jordi Coll
Marc Garcia
Jesús Giráldez-Cru
Gilles Pesant
Josep Suy
Mateu Villaret

The Business-to-Business Meeting Scheduling problem consists of scheduling a set of meetings between given pairs of participants to an event, while taking into account participants’ availability and accommodation capacity. A crucial aspect of this problem is that breaks in participants’ schedules should be avoided as much as possible. It constitutes a challenging combinatorial problem that needs to be solved for many real world brokerage events. In this paper we present a comparative study of Constraint Programming (CP), MixedInteger Programming (MIP) and Maximum Satisfiability (MaxSAT) approaches to this problem. The CP approach relies on using global constraints and has been implemented in MiniZinc to be able to compare CP, Lazy Clause Generation and MIP as solving technologies in this setting. We also present a pure MIP encoding. Finally, an alternative viewpoint is considered under MaxSAT, showing best performance when considering some implied constraints. Experiments conducted on real world instances, as well as on crafted ones, show that the MaxSAT approach is the one with the best performance for this problem, exhibiting better solving times, sometimes even orders of magnitude smaller than CP and MIP.

PDF Details DOI

AIJ Journal 2022 Journal Article

SAT encodings for Pseudo-Boolean constraints together with at-most-one constraints

Miquel Bofill
Jordi Coll
Peter Nightingale
Josep Suy
Felix Ulrich-Oltean
Mateu Villaret

When solving a combinatorial problem using propositional satisfiability (SAT), the encoding of the problem is of vital importance. We study encodings of Pseudo-Boolean (PB) constraints, a common type of arithmetic constraint that appears in a wide variety of combinatorial problems such as timetabling, scheduling, and resource allocation. In some cases PB constraints occur together with at-most-one (AMO) constraints over subsets of their variables (forming PB(AMO) constraints). Recent work has shown that taking account of AMOs when encoding PB constraints using decision diagrams can produce a dramatic improvement in solver efficiency. In this paper we extend the approach to other state-of-the-art encodings of PB constraints, developing several new encodings for PB(AMO) constraints. Also, we present a more compact and efficient version of the popular Generalized Totalizer encoding, named Reduced Generalized Totalizer. This new encoding is also adapted for PB(AMO) constraints for a further gain. Our experiments show that the encodings of PB(AMO) constraints can be substantially smaller than those of PB constraints. PB(AMO) encodings allow many more instances to be solved within a time limit, and solving time is improved by more than one order of magnitude in some cases. We also observed that there is no single overall winner among the considered encodings, but efficiency of each encoding may depend on PB(AMO) characteristics such as the magnitude of coefficient values.

Details DOI

IJCAI Conference 2017 Conference Paper

Compact MDDs for Pseudo-Boolean Constraints with At-Most-One Relations in Resource-Constrained Scheduling Problems

Miquel Bofill
Jordi Coll
Josep Suy
Mateu Villaret

Pseudo-Boolean (PB) constraints are usually encoded into Boolean clauses using compact Binary Decision Diagram (BDD) representations. Although these constraints appear in many problems, they are particularly useful for representing resource constraints in scheduling problems. Sometimes, the Boolean variables in the PB constraints have implicit at-most-one relations. In this work we introduce a way to take advantage of these implicit relations to obtain a compact Multi-Decision Diagram (MDD) representation for those PB constraints. We provide empirical evidence of the usefulness of this technique for some Resource-Constrained Project Scheduling Problem (RCPSP) variants, namely the Multi-Mode RCPSP (MRCPSP) and the RCPSP with Time-Dependent Resource Capacities and Requests (RCPSP/t). The size reduction of the representation of the PB constraints lets us decrease the number of Boolean variables in the encodings by one order of magnitude. We close/certify the optimum of many instances of these problems.

PDF Details