ABSTRACT. Branch-and-bound methods rely heavily on the quality and speed of bound computation to prune the search space effectively. Relaxed Multi-valued Decision Diagrams (MDDs) offer a powerful and flexible tool for computing relaxed bounds. Varying the width of decision diagrams make it possible to strike different tradeoff between bound tightness and computational cost. Existing implementation of Domain Independent Dynamic Programming showed how to take advantage of that capability for solving combinatorial optimization problems with a sequential or a multi-threaded approach. This paper introduces and describes a GPU-accelerated approach for constructing relaxed MDDs, and integrates it within a branch-and-bound solver. Experimental results show speedups reaching 4x compared to a state-of-the-art sequential baselines.

ABSTRACT. The Multiple Constant Multiplication (MCM) problem arises in many applications such as, for example, digital signal processing or deep neural network inference. Given a set T of target constants, the goal of MCM is to find the most efficient way for multiplying an input number with every constant in T, where multiplications are realized through bit-shifts and additions, and where intermediate results may be shared to produce different target constants. In this paper, we introduce a Constraint Programming (CP) model to solve MCM. We experimentally evaluate this model on a widely used benchmark extracted from a collection of digital filter designs, and we show that it is competitive with state-of-the-art Integer Linear Programming and SAT models. Then, we show that for any MCM instance there always exists an optimal solution that satisfies a "target-flattening" property. We introduce a new global constraint that ensures this property, together with an algorithm for propagating it in polynomial time. The addition of this global constraint to our CP model allows us to strongly reduce the search space and clearly outperform all other existing approaches.

ABSTRACT. Constraint programming technology allows optimisation experts to solve a broad category of personnel rostering problems, such as nurse rostering, airline crew rostering or retail worker scheduling. However, for problem domain experts to use this technology, the optimisation system must bridge the gap for users to easily explore solutions and influence constraints. Working with our energy industry partner for several years, we identified rostering problems involving multi-skilled shift workers present on site for extended periods. Their existing workflow for handling rostering (crew allocation), and rerostering (dealing with inevitable employee absences) and for time-limited formation of dedicated maintenance crews is labour intensive and complex, requiring in-depth knowledge of personnel files and skill competencies. To address this, we propose an interactive decision support system for crew rostering and rerostering, currently being deployed by our industry partner, that provides interactive tools for domain experts to perform exploration, validation, and conflict recovery.

ABSTRACT. Modern constraint solvers solve combinatorial problems through search with branching, propagation, and nogood learning. Although effective, the resulting search trees are hard to interpret: many branches and low-level inferences obscure why a conclusion is reached. Step-wise explanations provide an inference-based alternative, but prior successes were mainly in puzzle-style settings that required little or no search when solved by a CP-solver. We investigate whether step-wise explanations can be extended to search-heavy combinatorial problems. We study explanation sequences with only user-level constraints, ideally just one per step, and construct them from solver proof logs through nested explanations of complex steps. Our current results indicate that concise user-level explanations are often achievable, even when solving requires many search nodes, while also highlighting open challenges such as deep nesting in some instances and dependence on proof generation. This motivates future work on explanation-aware solving and richer explanation languages.

ABSTRACT. Algorithm selection is important in satisfiability and constraint solving, since no single solver performs best across all instances. Traditional learning-based approaches represent problem instances using expert-designed features to predict solver performance, while recent work explores graph representations derived from ASTs. However, most existing approaches overlook high-level contextual information, such as the application domain or the benchmark origin. In practice, such cues often help practitioners choose an appropriate solver. We present SMT-Select, a multimodal framework for SMT algorithm selection. It learns graph representations from formula ASTs and textual representations from natural-language context descriptions. These representations are then combined to guide solver selection. Evaluated across nine SMT logics, SMT-Select consistently outperforms existing selectors and SMT-COMP winning solvers. It has successfully closed at least 30% of the performance gap between the competition winner and the virtual best solver (VBS) across all evaluated logics; notably, it nearly matches the VBS in two logics.

ABSTRACT. A variety of heuristic search algorithms have been used in Domain-Independent Dynamic Programming (DIDP) for combinatorial optimization problems. While Complete Anytime Beam Search (CABS) has shown the best performance, it has an exponential memory usage in the worst case. We implement three linear-memory complete beam search algorithms in DIDP: two from the literature, Beam Stack Search (BSS) and Beam search Using Limited discrepancy Backtracking (BULB), and a third that is a novel adaptation of Depth-bounded Discrepancy Search to beam search. Our experimental results show that the linear-memory algorithms exhaust memory on fewer problem instances than CABS. Under restricted memory and extended run-time, BSS and BULB solve more problem instances in more problem classes than CABS. However, in all tested environments, CABS achieves the highest average proportion of instances solved in each of the problem classes, solves the most instances to optimality, and generates solutions with the lowest mean optimality gap.

ABSTRACT. Column generation and branch-and-price (B&P) are leading mathematical optimization methods for large-scale exact optimization, iterating between solving a master problem and a pricing problem. Due to the difficulty of discrete optimization, high-performance column generation often relies on a custom pricing algorithm built specifically to exploit the problem's structure. This bespoke nature of the pricing solver makes column generation a problem-specific method and hinders the use of generic implementations across a wide range of problems. We show that domain-independent dynamic programming (DIDP), a model-based paradigm for dynamic programming, can be used as a generic pricing solver. We develop new modeling features and a solving algorithm for DIDP to achieve better performance in typical pricing problems. We demonstrate that in four problem classes, our implementations of B&P price with pricing by DIDP empirically outperform an existing automated B&P price solver and B&P with pricing by mixed-integer programming or constraint programming.

ABSTRACT. Domain-Independent Dynamic Programming (DIDP) is a general framework for solving combinatorial optimization problems using Dynamic Programming (DP), where the search algorithm is separated from the problem specification. However, modelling directly in DIDP requires defining state variables, transitions, and dominance relations, which can be complex and error-prone. We present GRID, a modelling interface that enables high-level DP-oriented specifications. Users describe entities, relations, and resource attributes over a graph-based structure, from which GRID automatically compiles a DIDP model by deriving the components required by a DIDP solver. Common modelling elements are supported with built-in semantics, while additional constraints can be specified through user-defined variables and expressions. We instantiate GRID for vehicle routing problems and evaluate it on three variants: CVRP, PDPTW, and ECVRP. Results show that compilation overhead from GRID to DIDP is small and that generated models remain competitive with manually designed DIDP models while outperforming state-of-the-art CP and MIP approaches.

ABSTRACT. The aerospace line-balancing problem involves assigning and scheduling tasks to workstations to minimize cycle time, subject to strict precedence and shared resource constraints. A unique complexity in this environment is the presence of cyclic resource constraints caused by workers moving between stations within the same cycle. The existing constraint programming (CP) model schedules the tasks on an absolute time horizon. However, this approach suffers from two major weaknesses: it requires the factory layout (number of stages and parallel workstations per stage) to be fixed in advance, and it relies on modulo operators to project task intervals into a cycle window, which hinders constraint propagation. In this paper, we propose a novel spatial CP formulation that addresses both shortcomings. Our model dynamically determines the optimal placement of parallel workstations rather than relying on a predetermined layout. Additionally, it defines task decision variables directly within the cycle window, eliminating the need for modulo operators. Experimental evaluations using OptalCP demonstrate the spatial model's superiority, consistently finding equal or better solutions faster than the temporal approach. Furthermore, a direct engine comparison shows that OptalCP outperforms CP Optimizer on these models across the vast majority of instances.

ABSTRACT. High Mix Low Volume (HMLV) assembly problems involve producing a variety of items in small quantities, each of which requires scheduling a sequence of actions performed by machines or human operators. For the production process, companies are increasingly adopting reconfigurable manufacturing systems (RMS) where they choose which machines to deploy. Importantly, the selection of machines can substantially influence overall production time. For this reason, we present a CP model for solving HMLV for RMS. However, solely minimizing makespan does not necessarily yield the most desirable solution from a managerial perspective. For example, it may heavily rely on human operators. Since determining preferred solutions is challenging, incorporating Decision Maker (DM) feedback becomes essential. Therefore, to support DMs in selecting solutions that better reflect their preferences, we adapt pairwise preference elicitation methods for this industrial multi-objective combinatorial problem, while also comparing with trade-off-based methods.

ABSTRACT. Equal-Sized Partition (ESP) problem originates from real-world yarn production planning, where cotton bales that are characterized by type, color, and micronaire must be selected and divided into equal-sized groups (one per production day) such that the counts of each type and color grade differ by at most 1 across groups, while minimizing the maximum difference in average Mic between any two groups. A spinning company in Hue province, Vietnam, previously relied on a manual three-step process to solve this challenge. This study proves the NP-hardness of ESP, introduces intelligent computational approaches for its complex steps, proposes a dynamic programming algorithm for exact micronaire discretization in the first step, and develops a constraint-based local search metaheuristic for assigning bales to days in the third step. Experiments on five months of historical company data show substantial improvements over the manual method, resulting in the adoption of the proposed solution for daily operations.

ABSTRACT. The large-scale requirements of modern tooth manufacturing call for automated scheduling methods that can optimize multiple cost objectives while accounting for complex constraints. Previously, the artificial teeth scheduling problem (ATSP) was formally introduced, along with exact and heuristic methods to approach challenging real-life scenarios. Although existing approaches provide feasible solutions for all practical benchmarks evaluated, optimal results remain unknown. We propose a novel solver-independent constraint modeling approach that solves the ATSP through an innovative two-stage process. The first stage uses a subproblem formulation that batches product demands into compact jobs via constraint programming or column generation. In the second phase, the job sequence is optimized using a single-machine model with interval variables and global scheduling constraints. Experimental results with state-of-the-art constraint solvers and a heuristic demonstrate the approach's effectiveness, yielding improved solutions across the majority of realistically sized benchmark instances.

ABSTRACT. Validating Automated Driving Systems (ADS) requires generating various kinematically executable traffic scenarios. The grounding of qualitative descriptions into concrete trajectories is a combinatorial task poorly addressed by learning-based methods. We propose ScenaGen, a CP model operating on qualitative knowledge graphs (QKGs) to encode spatio-temporal relations between traffic entities. Formulated over integer position variables, ScenaGen enforces qualitative spatial constraints, distance thresholds, and inter-frame kinematic consistency. A single QKG acts as a formal template for systematically enumerating distinct, quantitatively varied concrete scenarios. Evaluation of synthetic and real-world benchmarks demonstrates that ScenaGen provides a robust and efficient alternative for scenario instantiation, outperforming standard search baselines in both scalability and solution diversity.

ABSTRACT. In Machine Learning, an accepted definition of fairness of a decision taken by a classifier is that it should not depend on protected features, such as gender. Unfortunately, when constraints exist between features, such dependencies can be obscured by the constraints. To avoid this problem, we propose that a decision be considered fair if it has a fair explanation. We define a fair explanation as a prime-implicant reason for the decision that does not contain any protected feature (where the constraints are taken into account in the definition of prime- implicant). Surprisingly, ignoring constraints can completely change the fairness of a decision (according to this definition) even in the absence of constraints between protected and unprotected features. Three possible definitions of fairness of a classifier are that for all its decisions (1) there are only fair explanations, (2) there is at least one fair explanation, or (3) changing protected features does not change the outcome. We identify the relationships between these different definitions of fairness and study the computational complexity of testing fairness of classifiers.

ABSTRACT. High-Utility Itemset Mining (HUIM) aims to discover itemsets whose utility exceeds a given threshold. While specialized algorithms achieve strong performance, they lack flexibility when additional domain constraints must be incorporated. Constraint Programming (CP) offers a declarative alternative but requires strong propagation to remain competitive. In this paper, we propose a CP framework for utility-driven pattern mining based on a parameterized global constraint that unifies the enumeration of High-Utility Itemsets (HUIs) and a new condensed representation called Utility-Peak Itemsets (UPIs). A UPI is an itemset whose utility is strictly higher than that of all its immediate subsets and supersets, capturing locally utility-maximal patterns. We study the computational complexity of UPI mining and show that deciding the existence of a UPI is NP-complete. Our global constraint, peakUtility, integrates utility computation and upper-bound pruning through propagation rules. Experiments on benchmark datasets show that the approach is competitive with state-of-the-art HUIM algorithms while preserving the modeling flexibility of CP.

ABSTRACT. Using a single broadcast camera, modern deep learning methods can detect and label players’ and ball positions on a frame-by-frame basis. This work focuses on post-game analysis, where frame-level labels are available for the entire video sequence. Deep learning alone performs poorly when retrieving intervals of frames in which specific spatio-temporal conditions or tactical patterns occur involving players and ball positions. A loosely coupled neuro-symbolic approach is proposed, in which these precomputed frame-level detections are processed through a SQL-like domain-specific query language. Each query is compiled into a Constraint Programming (CP) model that retrieves intervals of frames satisfying the specified constraints. The method leverages well-established CP constructs, such as time intervals and regular constraints. Experiments on real football games demonstrate that this approach is simple and efficient, enabling expressive querying for post-game tactical analysis while remaining accurate and scalable.

ABSTRACT. Many reasoning tasks require short partial satisfying assignments (implicants), sometimes focusing on a set of important variables. SAT-to-Ising/QUBO formulations are implicitly designed so that ground states correspond to total assignments, since the Ising/QUBO model assigns a value to every spin and has no native representation of unassigned variables. We introduce an Ising/QUBO framework that incorporates "don’t-care" semantics into the quadratic model via a dual-polarity representation, enabling the retrieval of short implicants. The encoding supports implicant shrinking and projection through minor objective modifications. We provide parameter regimes under which ground states correspond to short partial satisfying assignments, achieving minimality and, when the quadratic penalty function permits, minimum-cardinality. We empirically evaluate the encoding with simulated annealing on random 3-SAT enumeration benchmarks and non-CNF formulas, showing that it leaves about one-third of variables unassigned on random 3-SAT formulas while preserving satisfiability, and that consecutive polarity-freezing rounds achieve minimality (and minimum-cardinality) with high probability.

ABSTRACT. Parallel solving via cube-and-conquer is a key method for solving hard instances with SAT. While cube-and-conquer has proven successful for pure SAT problems, notably the Pythagorean triples conjecture, its application to SAT solvers augmented with propagators presents unique challenges as propagators learn constraints dynamically during the search. We study this problem using SAT Modulo Symmetries (SMS) as our primary test case, where a symmetry-breaking propagator reduces the search space by learning constraints that eliminate isomorphic graphs. Through extensive experimentation comprising over 20,000 CPU hours, we systematically evaluate different cube-and-conquer variants on three well-studied combinatorial problems. Our methodology combines prerun phases to collect learned constraints, various cubing strategies, and parameter tuning via algorithm configuration. The comprehensive empirical evaluation provides new insights into effective cubing strategies for propagator-based SAT solving, with our best method achieving speedups of 2-10x from improved cubing and algorithm configuration, providing an additional 2-50x improvement on the hardest cubes.

ABSTRACT. When solving constraint problems, symmetry handling is a crucial optimization. However, it is well-known that several preprocessing methods and encodings change the syntactic symmetries of the problem, and hence make it more difficult to exploit the symmetries that were present in the original problem. As a consequence, when currently using such methods, one should either handle the symmetries on the original specification or live with the fact that efficiency is lost since this structure is no longer visible. In this paper, we take a different approach: we develop a framework in which symmetry information is explicitly part of the specification and can be passed along through different transformations. One subtle, but important point in this respect is that transformations can change the set of variables. We study theoretical properties of transformations that preserve symmetry information, and we analyze existing transformations from the literature in this framework. We experimentally evaluate our framework, among others, on translations of pseudo-Boolean constraints into CNF, and show that in practice, simply passing on the symmetry information can lead to significant speed-ups in solving time.

ABSTRACT. Given a constraint satisfaction problem (CSP) predicate $P \subseteq D^r$, the non-redundancy (NRD) of $P$ is maximum-sized instance on $n$ variables such that for every clause of the instance, there is an assignment which satisfies all but that clause. The study of NRD for various CSPs is an active area of research which combines ideas from extremal combinatorics, logic, lattice theory, and other techniques. Complete classifications are known in the cases $r=2$ and $(|D|=2, r=3)$. In this paper, we give a near-complete classification of the case $(|D|=2, r=4)$. Of the 400 distinct non-trivial Boolean predicates of arity 4, we implement an algorithmic procedure which perfectly classifies 397 of them. Of the remaining three, we solve two by reducing to extremal combinatorics problems---leaving the last one as an open question. Along the way, we identify the first Boolean predicate whose non-redundancy asymptotics are non-polynomial.