ABSTRACT. Paratransit services are vital for individuals who cannot use fixed-route public transit, including those with disabilities. Optimizing these services is essential for transit agencies to deliver high-quality service efficiently. This paper introduces a Constraint Programming (CP) model to jointly optimize route planning and shift scheduling for paratransit operations, along with practical guidance for real-world implementation. A case study in Savannah, Georgia, demonstrates that the new approach is competitive with a recently proposed, highly effective AI-accelerated column generation framework, and significantly increases the number of requests served compared to current practices. The method is also easier to implement and provides an inherently practical solution for transportation planners. CP further provides the flexibility to optimize schedules without requiring shifts to start exactly on the hour, yielding an additional 5% improvement in the number of requests served.

ABSTRACT. This paper addresses the early stage design of a search and rescue mission by focusing on the configuration of the agent fleet, i.e., the selection and customization of each autonomous unit. To guide this configuration, two key evaluation criteria are introduced: (i) the performance --effectiveness of the fleet for executing the mission-- and (ii) the operability --the human workload required to supervise the fleet--. We formally define the joint optimization problem that simultaneously selects a fleet layout and assesses these criteria, and we present a unified Constraint Programming model to solve it. The model incorporates three interchangeable cognitive workload sub-models of increasing granularity, allowing designers to test different assumptions about operator workload while balancing the two criteria. Experiments on realistic instances inspired by the RoboCup Rescue Simulation League show that the approach efficiently identifies several fleet configurations, offering a human-centered approach for early mission design.

ABSTRACT. Global constraints are a central concept in Constraint Programming (CP), which allows modellers to compactly express complex relations, and allows solvers to efficiently handle them. Table constraints have especially been well-studied as they can express arbitrary finite relations, and are extensively used in CP benchmarks. In this paper we study how to best deal with table constraints when using Integer Linear Programming (ILP) solvers. We study two paradigms: linear encodings, and a lazy cut generation approach. For the encoding we propose a novel Boolean decomposition, as well as an MDD-based flow encoding. For the cut generation, in which lazy constraints are generated on-demand during branch-and-cut search, we investigate different ways of generating such integer and fractional cuts as well as how to strengthen them through shrinking and cut lifting. We experimentally compare the different approaches on CP competition instances with a wide variety of table constraints, showing clear benefits over the standard integer encoding.

ABSTRACT. Stepwise explanations are essential for interpreting constraint programs, yet current methods—relying on repeated MUS extraction or heavy SAT-based propagation—remain computationally prohibitive for complex problems. We propose a novel framework leveraging Multi-Valued Decision Diagrams (MDDs) to overcome these bottlenecks. By decomposing CSPs into smaller, graph-based subproblems compactly represented as MDDs, we enable highly efficient constraint propagation through network-flow reformulation. To further enhance efficiency, we propose a Divide-and-Conquer approach to improve the search for minimal explanation steps. Furthermore, we utilize the MDD’s network-flow structure to generate nested explanations that breaks down complex derivation steps into granular, arc-level details, revealing specifically how variable-value assignments become infeasible. In this way, our approach equips the explainer agent a voice that provides more intuitive and granular stepwise explanations. Evaluated on Graph Coloring and Nurse Rostering benchmarks, our framework significantly reduces explanation generation time while maintaining interpretability and conciseness compared to state-of-the-art methods.

ABSTRACT. This work proposes a CP-based methodology for estimating the maximum freight capacity of railway junctions serving industrial areas with multiple terminals, where minimum per-destination service frequencies must be guaranteed as hard constraints to preserve commercial competitiveness among terminal operators. The problem is formulated as a scheduling problem with optional interval variables: the solver decides which candidate services to execute and when, maximising completed round-trips within a 24-hour horizon while satisfying track-occupancy exclusivity, turnout conflicts, buffer-capacity limits, a mandatory maintenance window, and a fixed passenger timetable. The approach is implemented in OptalCP and evaluated on five scenarios covering the current and a planned upgraded infrastructure of a maritime port in the northern Adriatic Sea. Satisfiability queries are answered in under 13 seconds; maximisation queries establish that the as-is network sustains at least 35 freight services per day against the 11 currently operated, rising to at least 38 after the planned upgrade, with both authority service targets confirmed feasible on their respective infrastructures.

ABSTRACT. Optimizing schedules in real-world settings often requires considering workload constraints, especially for human resources, to ensure regulatory compliance, impose rest periods, and level the workload over time. This paper focuses on tackling this family of constraints in the context of preemptive jobshop scheduling, as preemption is particularly relevant when human resources are involved (allowing personnel to flexibly switch between tasks). The main contribution of this paper is a Constraint Programming approach designed to handle effectively maximum workload constraints in a preemptive setting, without decomposing activities into unit-duration tasks (computationally prohibitive). Since workload constraints introduce significant additional complexity, we further propose a solution method that iteratively introduces the workload constraints into the problem, and tailored heuristics specifically designed to guide the search efficiently. The experimental results demonstrate the effectiveness of our approach on a large set of instances, highlighting its performance compared to a well-known industrial solver, IBM's CP Optimizer.

ABSTRACT. The aeronautical industry transitioned in the 90s to takt-paced, product-specific assembly lines. The current trend of increased customization and demand variability is pushing for a transition to flexible mixed-model assembly lines. We address a mid-term planning problem for an airframe assembly plant, modeled as a Resource-Constrained Project Scheduling Problem (RCPSP) with complex industrial constraints. This formulation serves a dual purpose: facilitating high-level production planning and validating plant designs, particularly during ramp-up scenarios. We specifically tackle challenges involving calendar-based preemption, variable resource capacity, and resource blocking between task groups. We propose a Constraint Programming (CP) formulation that optimizes conflicting objectives, including Tardiness and Just-in-Time costs. To ensure scalability for large industrial instances, we introduce a sequential solving method based on topological decomposition. The proposed approach proves effective in handling complex scenarios, acting as a foundation for more realistic models.

ABSTRACT. Constraint Programming (CP) has been around for several decades, yet it remains largely unknown in industry. When faced with combinatorial optimization problems, industry practitioners not knowledgeable in constraint techniques often resort to more creative but not necessarily adequate solutions. This paper is the result of an actual case study brought by an industry consultant. The problem at hand is the optimization of the activation schedule for high-power pumps in a water treatment facility under fluctuating energy costs. The schedule was previously generated using a combination of heuristics and Discrete Particle Swarm Optimization (DPSO). These methods struggled with the increasing complexity of volatile market signals and strict operational constraints. Our simpler model, developed in Python using the CPMpy library, formalizes the problem as a CP model. Our experiments demonstrate the benefits of our model's simplicity compared to the DPSO solution. This use case also showcases the importance of the accessibility of constraint modelling solutions for less knowledgeable practitioners.

ABSTRACT. A standard problem in the field of Earth observation is the scheduling of the observations of an agile satellite constellation. Given a set of end-user requests, the problem consists in defining the assignment and sequence of observations planned for each satellite under temporal constraints. This paper presents how Constraint Programming (CP) can be applied to solve this combinatorial observation dispatching and scheduling problem to maximize a sum of collected individual observation rewards. Our main focus is the search for efficient strategies to approximate time-dependent no-overlap constraints given CP solvers that only manage sequence-dependent no-overlap constraints. In particular, we introduce constant-step and variable-step time-discretization methods, together with several approximation parameters. To get actually feasible solutions, the CP model is coupled with a greedy repair strategy that takes time-dependency into account, and a Large Neighborhood Search (LNS) that post-optimizes the solutions, delivering high-quality solutions compared to a baseline LNS.

ABSTRACT. In high school timetabling, several schools construct their schedules according to predefined block patterns designed to ensure a balanced distribution of instructional time. This structure introduces a specific challenge: courses occupying half-blocks must be paired to form full blocks and integrate with other courses. The pairing of half-block courses is a critical step, as it directly impacts the balance of students across sections. Therefore, this paper introduces a constraint programming approach to generate a feasible half-block courses schedule leading to good student balancing. The approach is evaluated on real-world data, provided by Dash Computer Solutions, a company responsible for the design of many high school schedules in Quebec, and is integrated with their existing student sectioning algorithm. Our results show that our approach provides solutions of comparable quality to a human-guided local search, while reducing the designing time from 10 hours to an hour in the best case.

ABSTRACT. Constraint model performance strongly depends on formulation. Redundant constraints can strengthen propagation and speed solving, but designing effective ones requires expertise. Recent work shows that Large Language Models (LLMs) can generate useful constraints for MiniZinc, but without soundness guarantees: generated constraints may exclude optimal solutions or make instances infeasible. We present a pipeline that combines LLM-based constraint generation, empirical evaluation, and formal verification. A key component is a formalization of a supported MiniZinc subset that verifies redundancy of a constraint schema for all instances by translating MiniZinc models into Lean 4 theorems. To handle MiniZinc's partial semantics, we require the base model to be safe and separately prove that the new constraint is well-defined for all instances and solutions. We evaluate the approach on three optimization problems from the literature, starting from published models and observing clear gains on one and mixed or small effects on the others.

ABSTRACT. As constraint programming (CP) solvers are increasingly used in critical applications, there is a growing need for certification of solver claims of infeasibility and optimality. Recent work has demonstrated that certification is feasible for CP solvers using a multi-stage proof-generation framework; however, the underlying proof system was informal, and verification relied on translation into an external proof format, impacting the trustworthiness. We address these issues by designing a rigorous, solver‑agnostic framework for certifying CP solver claims. We introduce DRCP, a formally specified proof system for CP over integer domains that captures core solver operations, including conflict analysis and heterogeneous propagation, by modular inference rules with precise semantics. We also develop FznDrcpCheck, a formally verified proof checker in Rocq that validates DRCP proofs directly against FlatZinc models. Our evaluation shows that our framework enables practical certification across various benchmarks with negligible overhead during solving and modest proof-checking costs.

ABSTRACT. When a certifying solver claims that a solution is optimal or that a problem is unsatisfiable, it demonstrates this convincingly by giving a proof log which can be checked by an independent (and ideally formally-verified) proof checker. Such an approach should also be viable for enumeration problems ("I have listed all solutions explicitly") and counting problems ("there are exactly 42 solutions"), but the currently most popular proof logging systems contain several vital features which are incompatible with this goal. We explain how the VeriPB system can be modified for enumeration and counting proofs whilst retaining as much as possible of its powerful "strengthening" and "deletion" features. We implement this extension both inside VeriPB's user-friendly proof checker and elaborator, and the formally verified CakePB backend, and use this to obtain formally verified enumerations of solutions for a range of constraint solving and graph problem instances.

ABSTRACT. We propose an oracle-guided approach to construct VIPR certificates that certify the optimality of integer linear programming solutions. Our approach treats the solver as a black-box LP oracle and translates its floating-point answers into exact rational derivations. This translation is based on the notion of cascaded rationalization, a sequence of continued-fraction approximations at increasing precision levels. Our approach does not require an exact LP solver and comes with self-contained, independently verifiable certificates. We implement this approach and evaluate it empirically against SCIP's exact mode on generated benchmarks across four problem classes and on MIPLIB 2017 instances. On generated benchmarks, the oracle approach produces substantially more compact certificates on nearly all instances. On MIPLIB, each approach solves instances that the other cannot handle. The two approaches to certified optimality are complementary.

ABSTRACT. Applied combinatorial optimization has witnessed a revolution in performance since the turn of the millennium, but the complexity of modern solvers is making bugs into an ever more serious concern. The most promising remedy is to make solvers certifying, so that they use proof logging to generate machine-verifiable proofs of correctness. We present the first example of certified graph colouring in the state-of-the-art solver ZykovColor using VeriPB proofs. Combined with the formally verified CakePB backend, this provides end-to-end certified graph colouring. An experimental evaluation shows excellent results with only moderate overhead for proof logging and checking.

ABSTRACT. Dijkstra’s token ring algorithm is a fundamental example of a self-stabilizing algorithm for solving mutual exclusion in an asynchronous distributed system arranged as a rooted directed ring. This paper studies the self-stabilization of this algorithm using an approach based on propositional satisfiability. We propose a logical modeling framework for the asynchronous executions of the algorithm that rigorously captures the state update rules, as well as the mechanisms for detecting convergence toward a legitimate configuration or, conversely, divergence through the existence of cycles between illegitimate configurations. Furthermore, we also optimize the efficiency and scalability of the analysis by introducing an offset-based symmetry-breaking technique applied to the initial configurations, thereby significantly reducing redundant explorations of equivalent execution scenarios. In addition, we extended the study to restricted daemon assumptions to assess open challenges.