Schedule

Cumulative constraints are central in scheduling with constraint programming, yet propagation is typically performed per constraint, missing multi-resource interactions and causing severe slowdowns on some benchmarks. I present a preprocessing method for inferring additional cumulative constraints that capture such interactions without search-time probing. This approach interprets cumulative constraints as linear inequalities over occupancy vectors and generates valid inequalities by (i) discovering covers, the sets of tasks that cannot run in parallel, (ii) strengthening the cover inequalities for the discovered sets with lifting, and (iii) injecting the resulting constraints back into the scheduling problem instance. Experiments on standard RCPSP and RCPSP/max test suites show that these inferred constraints improve search performance and tighten objective bounds on favorable instances, while exhibiting more stable performance on unfavorable instances than the prior work. Additionally, these experiments discover new lower bounds and new best solutions; seven of the lower bounds are obtained directly from the inferred constraints.

Few amongst the rules that filter the Cumulative\ constraint reason on the integrity of resource consumption. We augment the overload check with an integral reasoning that better evaluates resource availability. This reasoning is based on the knapsack problem, which we solve using dynamic programming. Our new rule subsumes the time table horizontally elastic overload check while its running time complexity is O(capacity n^2), only increasing by a factor capacity (the resource capacity) due to solving knapsack problems. Exploiting word-parallelism actually makes this complexity Oleft(capacity{w} n^2right) for w-bit machines. On usual instances, capacity is small and this complexity collapses back to O(n^2). Our algorithm generates explanations for lazy clause generation solvers. With our new knapsack augmented overload check, we are able to solve all but 5 instances of the Pack benchmark. By performing a small transformation of the instances, we show that our method is more robust than known pre-solving methods that perform well on the original benchmark.

Optional variables have for a long time been identified as a crucial component of state-of-the-art scheduling solvers. They not only offer a natural way to model many scheduling problems but also play an important role in the efficiency of such solvers by enabling a stronger inference in a constraint propagation engine. Despite this recognition, their adoption in modern solvers remains extremely scarce presumably because their native support requires pervasive changes to a solver and handling many subtleties that have not been extensively studied. In this paper, we aim to provide a good foundation in this direction by providing a formal characterization of optional variables and of their interactions with key components of a constraint programming solver including propagators, reification and lazy clause generation. In addition, we present a new lazy clause generation solver with native support for optional variables and demonstrate its efficiency on variants of the flexible jobshop problem.

Benchmarking scheduling instances solely by nominal size is often misleading: instances with the same number of jobs and machines can differ by orders of magnitude in empirical hardness. This paper proposes a supervised, solver-aligned difficulty estimator for Job-shop Scheduling Problem (JSP) instances. Building on standard disjunctive-graph descriptors and ISA-inspired distributional summaries, we construct an auditable hardness target from normalised multi-solver traces and learn to predict it from static instance features. A Random Forest regressor learns a bounded hardness score P(x)in[0,1], from which balanced easy/medium/hard categories are induced. The empirical evaluation shows that the learned score is strongly aligned with solver-effort indicators, provides interpretable feature-level explanations, and provides evidence of partial ordinal transfer on classical JSPLIB benchmarks under distribution shift. The proposed framework provides a practical and interpretable basis for difficulty-aware benchmarking, instance selection, and solver-behaviour analysis beyond nominal size parameters.

Constraint Programming (CP) is a powerful optimization method that provides optimality guarantees, but due to its exact nature, its scalability to large instances is often limited. To address this, we propose a hybrid approach that combines a CP solver with heuristic methods, directly and asynchronously exchanging solutions and objective values during runtime. The hybrid parallel configuration yields faster convergence to good solutions across various problem domains than the solver alone, while retaining the ability to guarantee optimality, leveraging the complementary nature of the CP solver and heuristics. The efficiency of this approach is evaluated on three well-known scheduling problems and three well-known routing problems. Noticeable improvements are observed for the Flow-shop Scheduling Problem (FSSP), the Traveling Salesman Problem (TSP), and the Vehicle Routing Problem with Time Windows (VRP-TW). Even for problems where improvements are marginal, the portfolio of methods increases the robustness of the approach.

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.

Tree ensembles (TEs) are among the most widely used machine learning models, yet explaining their predictions remains a computational challenge. Recent work in formal explainable AI (FXAI) has focused on computing abductive explanations for TEs using Boolean satisfiability (SAT) and maximum satisfiability (MaxSAT). However, these methods often fail to scale with the growth of the number and depth of the trees in the ensemble. This paper addresses these scalability limitations by shifting focus to Rule Ensembles (REs), a structurally simpler alternative to TEs. We make three primary contributions. First, we adapt an existing MaxSAT-based explanation framework designed for TEs to function with general REs. Second, we devise a dedicated logic encoding for REs combining SAT solving with pseudo-Boolean (PB) constraints for determining the winning class. Finally, empirical experiments on standard tabular and image datasets demonstrate a significant advantage of the proposed SAT-based approach for REs over the state-of-the-art MaxSAT-based approach for TEs.

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.

Conflict_Driven Clause Learning (CDCL) is central to the success of SAT solvers, and its adaptation to Constraint Programming (CP) through Lazy Clause Generation (LCG) has been a major breakthrough for CP solving. A core requirement of LCG is to maintain both a CP and SAT view of the problem. Because maintaining a full SAT encoding is impractical, solvers rely on partial and solver_specific encodings -- an approach that has evolved as folklore rather than formal design. We present the first systematic analysis of how leading LCG solvers maintain their SAT encodings, based on source_code inspection and developer correspondence. Our analysis reveals substantial differences in explanation lifting, backwards explanations, linking clauses, and nogood minimisation, all driven by the need to preserve a SAT view. To overcome these compromises, we propose a native CDCL framework for CP. We replace SAT literals with atomic constraints, enabling conflict analysis, nogood learning, and nogood propagation directly at the CP level. This results in cleaner algorithmic design, eliminates SAT_specific complications, and allows us to introduce extended nogood propagation, a generalisation of SAT_based clause propagation, as well as CPIP nogoods, a generalisation of SAT-based learned nogoods. Our implementation of the framework in Pumpkin demonstrates competitive performance in the MiniZinc Challenge 2025. Additionally, we empirically show that extended nogood propagation combined with CPIP nogoods can significantly reduce failures, especially on problems with constraints that reason over domain holes. Overall, our framework provides a principled and semantically rich generalisation of CDCL for CP.

The Large Weight Syndrome Decoding problem LWSD is a fundamental problem in coding theory. It consists in determining whether a given linear code admits a high Hamming weight vector associated with a specific syndrome. LWSD is a variant of the classical syndrome decoding problem, which conversely seeks a low Hamming weight solution for a linear system defined over the binary field F_2. In this paper, we investigate a generalization of this problem to the case of a prime finite field F_Z, referred to as LWZSD. We propose several models using Boolean Satisfiability (SAT) formulas and compare the efficiency of our approaches using state-of-the-art solvers.

Global constraints are a central concept in CP, which allow modellers to compactly express complex relations, and which allow 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 milp solvers. We study two paradigms: linear encodings, and a logic-based Benders decomposition{lazy cut generation approach}. For the encoding we propose a novel mdd-based flow encoding. For the Benders decomposition{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.

Stepwise explanations are an important tool for interpreting constraint programs. Existing methods rely heavily on repeated minimal unsatisfiable subsets (MUS) extraction or intensive SAT-based propagation, which are computationally prohibitive for large-scale problems with complex constraints. 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 break 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 with 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.

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.

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

The performance of constraint models strongly depends on the formulation used. Redundant constraints, which are logically implied by the model, can strengthen propagation and speed up solving, but finding effective ones requires substantial expertise. Recent work has shown that Large Language Models (LLMs) can generate performance-improving constraints for MiniZinc models. However, such approaches offer no soundness guarantees and the generated constraints may exclude optimal solutions or render instances infeasible. We present a pipeline that combines LLM-based constraint generation with empirical evaluation and formal verification. At its core is a novel formalization of a supported MiniZinc subset for verifying redundancy of a constraint schema over all instances by translating MiniZinc models to Lean 4 theorems. We handle MiniZinc's partial semantics by requiring the base model to be safe and separately proving that the proposed constraint is well-defined for all instances and solutions of the base model. We evaluate the approach on three constraint optimization problems from the literature, starting from published expert-crafted models. The augmented models show a clear improvement on one problem, improved MiniZinc Challenge scores with metric trade-offs on another, and small but non-significant changes on the third.

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 formalising a rigorous, solver-agnostic framework for certifying CP solver claims. We present a formal definition of proofsystemname, a 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 proofsystemname 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.

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.

We propose an oracle-guided approach to construct VIPR certificates that certify the optimality of integer linear programming (ILP) solutions. Our approach treats the ILP solver as a black-box 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 VIPR 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.

Applied combinatorial optimization has witnessed a revolution in performance since the turn of the millennium, but the complexity of modern solvers is making bugs 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 state-of-the-art certified graph colouring by equipping the solver zykovcolor with veripb proof logging. Combined with the formally verified cakepb checker, this provides end-to-end formally certified results. An experimental evaluation shows excellent results with only moderate overhead for proof logging and checking.

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 extend the study to restricted daemon assumptions to assess open challenges.

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

Optimizing schedules in real-world settings often requires considering workload constraints, especially for human resources, to ensure regulatory compliance, impose rest periods, or level the workload over the working horizon. 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). Preemption also offers theoretical insights as a relaxation of non-preemptive problems. 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 (which may be computationally prohibitive). Since workload constraints introduce significant additional complexity, we further propose a method that iteratively introduces the workload constraints into the problem, along with 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.

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.

Constraint Programming (CP) has been around for decades, yet it remains largely unknown in industry. When faced with combinatorial optimization problems, industry practitioners not knowledgeable in CP techniques often resort to more creative but not necessarily adequate solutions. This paper is the result of an actual case study brought by Technord, 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 Discrete Particle Swarm Optimization (DPSO). This method 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.

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 over Points of Interest (POIs), the problem consists in selecting observations among the candidate ones, attributing each of them to a satellite, and defining the sequence of observations planned for each satellite under operational constraints. These constraints stem from the visibility windows of the POIs and from the time_dependent maneuvers required to reorient the satellites between successive POI observations (duration of the maneuvers function depending on their start times). This paper presents how Constraint Programming (CP) can be applied to solve this combinatorial observation dispatching and scheduling problem, the objective being 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. This CP-Repair-LNS pipeline delivers high_quality solutions compared to a baseline LNS.

In high school timetabling, some institutions adopt a university-like structure in which students follow different curricula and multiple sections are offered for each course, without pre-assigning students to specific sections. In such settings, student sectioning and timetabling are strongly interdependent. Timetabling is usually carried out with integer linear programming or metaheuristics, before assigning students to sections on the fixed schedule. However, several Canadian high schools construct their schedules according to predefined block patterns designed to ensure a balanced distribution of instructional time. While this structure eliminates many classical timetabling constraints, it introduces a specific challenge: courses occupying half-blocks must be paired to form full blocks. This allows students to have the rest of their courses on well balanced, full blocks, thus easing student mixing between sections for improved student sectioning. The pairing of half-block courses is a critical step, as it directly impacts the balance of students across sections. Based on this context, this paper introduces a constraint programming approach to generate a feasible half-block courses schedule leading to good student balancing. The model is designed to enhance computational efficiency, accommodate additional practical constraints, and reduce the need for manual adjustments by scheduling operators. The approach is evaluated on anonymized real-world data from Canadian high schools for the 2024-2025 academic year, provided by Dash Computer Solutions, a company responsible for the annual 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 with a hand-crafted initial solution, while reducing the designing time from 10 hours to an hour in the best case.

Insertion sequence variables have recently been introduced as a computational domain for modeling routing and sequencing problems in constraint programming. Typically, search heuristics guide the insertion process of new nodes into a partial growing path, while constraints eliminate infeasible insertions. This paper investigates filtering for the (minimum) distance constraint over insertion sequence variables. This global constraint links a sequence to a distance variable based on a given distance matrix. So far, only a simple filtering algorithm has been proposed, which considers the partial path but ignores mandatory nodes. Our contribution is to introduce stronger lower bounds that also take mandatory nodes into account. These bounds further enable the derivation of additional filtering rules for node insertions. An experimental evaluation on the TourMustSee problem shows that the proposed filtering rules significantly reduce the search space compared to the existing filtering approach.

We study the p-dispersion problem with distance constraints (pDD), a variant of the well-known p-dispersion problem. In a pDD, the goal is to locate a set of facilities so as to maximize the minimum distance between any two of them, subject to additional constraints specifying minimum allowed distances. Two CP models for the pDD have recently been proposed. The first is a typical model that includes the global constraints {em Minimum} and {em Element} and explicitly represents the objective function, connecting it to the decision variables. However, as problem size grows, this model becomes increasingly inefficient. The second model adopts a simplistic approach that only uses binary constraints, essentially treating the pDD as a satisfaction problem. In this paper, after demonstrating the deficiencies of these models, we propose a new compact model that captures the problem through ternary constraints, instead of global or binary ones. We prove that, rather surprisingly, the pruning of the decision variables' domains achieved in our new model is equivalent to that achieved in the model with global constraints, resulting in the same search tree under the same variable and value ordering. Experiments demonstrate that our new model is by far superior to the existing ones, both in terms of solution quality and run times.

The Bound-Impact Value Selector (BIVS) employs a look-ahead strategy to enable black-box Constraint Optimization Problem (COP) solvers to find high-quality solutions earlier. However, its computational cost prohibits its use throughout the entire search process. To mitigate this cost, the Restricted Fixpoint (RF) approach considers only the constraints on the shortest paths between the selected variable and the objective, yielding better performance. In this paper, we propose a lightweight strategy from a different perspective, named Assess Before Look-Ahead (ABLA), to enhance the performance of look-ahead-based value heuristics for solving COPs. ABLA first assesses whether the look-ahead process can differentiate between the values of a variable, and only performs the look-ahead when this assessment passes. Experiments on benchmark instances from recent MiniZinc Challenges demonstrate that ABLA's decisions to skip redundant look-ahead processes are highly reliable, with an average accuracy of over 94%. Consequently, ABLA significantly boosts the performance of both BIVS and RF, outperforming two other baselines: the minimum value heuristic and the RLARF value heuristic.

Recent work has shown that classical planning tasks can be compactly factored into deterministic finite automata and solved optimally with constraint programming (CP). In this setting, finding a plan reduces to finding a word accepted by all automata through constraints. So far, however, these automata have had to be carefully handcrafted from PDDL tasks. In this paper, we show that they can instead be generated automatically and used as the basis of CP models. We also show that the resulting framework is easily extensible with additional constraints from the planning literature that strengthen propagation. Our approach solves more tasks than the state of the art in end-to-end CP for classical planning in almost all domains.

Logistic optimization frequently involves complex routing decisions bound by tight numerical constraints such as vehicle capacities. This paper addresses a real-world industrial multi-batching problem where products must be routed between distributed sites. The objective is to determine optimal routes, travel frequencies, and packing configurations at minimum cost. The problem corresponds to a minimum cost flow problem coupled a bin packing problem. We investigate direct formalizations, decompositions, and scalable sequential approaches across three base technologies: Mixed-Integer Linear Programming, Constraint Programming, and Constraint Answer Set Programming. Our contributions are threefold: we propose a direct formalization of the problem, additional distinct approaches that scale for an industrial use case, and finally an empirical evaluation. By comparing these approaches we highlight the most effective configurations. Results suggests that a three-step approach provides the best results: combining MILP for flow routing, a greedy bin packing and CP for refinement.

We study a routing problem for delivering and picking up multiple commodities with different priorities, motivated by the need to provide basic services to people in depopulated rural areas with a driver shortage. We define our problem as a generalization of the team orienteering problem with time windows, with additional constraints motivated by real-world applications. We develop constraint programming (CP) and mixed-integer programming (MIP) models to solve the formulated problem. In addition, we propose an incremental warm-starting strategy, which obtains an initial solution by solving a problem considering only a subset of commodities. In our experiment, CP outperforms MIP, and incremental warm-starting improves the performance of both approaches.

Heating, Ventilation, and Air Conditioning (HVAC) systems typically aim to regulate a building's indoor environment. Many key design decisions which carry strong consequences on HVAC systems are made during early-stage building design, when architectural and structural layouts are still evolving. Early coordination between disciplines has the potential to minimise re-design of systems as a consequence of changes in other systems. This paper presents an optimization-based framework to support early design coordination among architectural, structural and mechanical designs, with a focus on ductwork layout. The generated layouts are intended to serve as initial candidate designs that engineers can further refine during later stages of the building design process. We develop models for generating feasible duct layouts accounting for structural constraints and cost objectives. The models are implemented in a high-level modelling language MiniZinc and solved in phases using Constraint Programming (CP) and Mixed-Integer Programming (MIP) solvers. Experiments on case studies show that feasible coordinated layouts can be generated, enabling iterative exploration of multiple alternative configurations during early-stage design.

In professional sports, a team has clinched the playoffs if they are guaranteed a postseason spot, regardless of the outcomes of any remaining games. As the season progresses, sports fans and other stakeholders are interested in precisely when, and under what conditions, their team will clinch the playoffs. In this paper, we investigate playoff clinching in the context of the National Hockey League (NHL), where it is computationally challenging to produce clinching scenarios due, in part, to complex tie-breakers. We present an algorithm that determines under which combinations of game outcomes in the next n days a team will clinch the playoffs (i.e., “n-day lookahead clinching”). Our approach is a custom tree search which employs various preprocessing techniques, pruning strategies, and node ordering heuristics to efficiently explore the space of possible outcomes. The tree search leverages a constraint programming (CP)-based subroutine for inference that determines if a team has clinched the playoffs for some snapshot in time of the regular season (i.e., “0-day lookahead clinching”). This CP subroutine aims to find a counter-example in which the team being evaluated is eliminated, taking into account qualification rules and the NHL's extensive list of tie-breakers. We validate the efficacy of our algorithm using hundreds of scenarios based on public NHL data for the seasons 2021-22 through 2024-25. The methods introduced can be readily extended to other metrics of interest, including mathematical proof of playoff elimination, clinching the President's Trophy, as well as clinching (or being eliminated from clinching) any other seed in the standings.

In the wood industry, ensuring the stability and immobility of a workpiece during machining is essential. Vacuum suction cups are commonly used as fixtures, as they can rotate to better conform to the workpiece perimeter. However, this rotational capability introduces additional complexity into fixture placement. This paper addresses the problem of optimally positioning rotatable fixtures by combining two complementary techniques. First, we solve a restricted version of the problem that neglects rotations using a constraint solver, yielding an initial feasible solution. This solution is then refined using a Particle Swarm Optimization algorithm that accounts for rotation. Experimental results show that the quality of the initial solution significantly influences the final placement, and that the proposed approach can effectively support expert operators in making improved decisions.

Recent advances in AI have spurred interest in NeSy architectures that integrate neural and symbolic methods. In particular, combining a Constraint Programming (CP) model with a language model for constrained sequence generation tasks allows the neural component to capture domain knowledge while CP enforces structural constraints. In this paper we propose combining CP with a Masked Language Model (MLM) to perform Large Neighbourhood Search (LNS). Unlike conventional left-to-right Large Language Models, MLMs can complete sequences with gaps in arbitrary positions, making them well-suited for this task. Meanwhile, LNS provides a CP-based iterative framework to explore constrained subspaces whenever searching the whole space would be intractable. We evaluate NeSy LNS on tasks in constrained text generation and molecule discovery. Our experiments show that it can quickly generate many high-quality sentences and molecules, even for highly-constrained tasks.

Inspired by concepts of constraint-based local search, we present a novel scheme for automatically relaxing a given high-level model into an optimisation model that is better suited for large neighbourhood search (LNS). By exploiting the variable sharing and semantics of the constraints in a model, our scheme (1) identifies constraints that can easily be satisfied simultaneously and can thus constrain the neighbourhood, and (2) relaxes the remaining constraints. As a side effect, our scheme enables the LNS solving of a constraint satisfaction problem, by transforming it into an optimisation problem, and the faster solving of a difficult-to-satisfy constrained optimisation problem, by finding the initial incumbent faster. This scheme can be used with any CP-based LNS solver. We tested a portfolio of CP-based LNS variants running in parallel, with a multi-armed bandit to select which LNS variant to run. Our results show that this approach is very competitive.

Algorithms for solving combinatorial optimisation problems often exhibit complementary strengths, motivating automated algorithm selection by training ML models that predict the best algorithm for a given instance. However, collecting training data for such models is computationally expensive, as it requires running all provided algorithms on all training instances. Recent work on frugal algorithm selection shows that the training data collection cost can be reduced substantially through active learning, but the interaction between model choices and data efficiency remains poorly understood. In this work, we empirically investigate how different learning formulations behave under limited training data using the ASLib benchmark. Our results reveal that multiclass classification (MC), despite weak performance when trained on full training data, improves dramatically with active learning. Remarkably, active MC matches strong passive learners while using only a fraction of the training data. This highlights an unexpected efficiency gain: algorithm selectors that underperform with full training data become highly effective when training data is selected actively.

Cancer is often driven by specific combinations of an estimated two to nine gene mutations, known as multi-hit combinations. Identifying these multi-hit combinations of gene mutations that drive cancer is critical for understanding carcinogenesis and designing targeted therapies. We formalize this challenge as the Multi-Hit Cancer Driver Set Cover Problem (MHCDSCP), optimizing the selection of gene combinations to maximize tumor coverage while strictly minimizing normal sample misclassification. While existing approaches rely on exhaustive enumeration and massive parallelization, we introduce fast heuristics based on constraint programming and mixed integer programming formulations. Evaluated on real-world cancer genomics data, our framework matches state-of-the-art supercomputing methods using a single commodity CPU in under a minute. We also propose a price-and-branch heuristic which, by solving the root node to optimality, provides the first provably optimal solutions for over half of the benchmark instances, thereby verifying the near-optimality of our fast heuristics. These findings demonstrate that on real-world problem instances, the MHCDSCP is far less computationally demanding than previously believed, providing an accessible baseline that enables the exploration of previously intractable multi-hit modeling assumptions.

We study generic integer programming (IP) encodings of acyclicity in directed graphs as a key constraint in various real-world problem domains. We analyze both classical and more recently-proposed generic acyclicity encodings, including Miller--Tucker--Zemlin (MTZ), feedback vertex set (FVS), vertex elimination (VE), and cycle elimination (CE) based encodings in terms of their linear programming (LP) relaxation tightness. We also introduce hybrid encodings combining sought-after properties of the individual encodings. For the hybrids, we establish tightness guarantees for their LP relaxations that interpolate smoothly between the individual encodings. Our results show that VE and CE yield equally strong relaxations and strictly dominate MTZ and FVS, while the hybrid encoding schemes become increasingly tight as the elimination prefix grows. Mapping theory to practice, we empirically evaluate the encodings on both direct IP encodings of problem domains, where acyclicity is a key constraint. The results both validate our theoretical findings and yield promising runtime performance.

Many edge-selection problems, such as the Traveling Salesman Problem and Orienteering Problem, are NP-hard, making them expensive to solve with exact methods and challenging to address with hand-crafted heuristics. Learning-based approaches provide an efficient alternative, while self-supervised methods avoid costly solution labels. However, existing approaches often still rely on heavy post-processing or narrow problem-specific designs. We propose a reusable self-supervised framework for edge-selection optimization that learns directly from unlabeled instances. The framework uses differentiable surrogate objectives and feasibility-driven penalties to encourage the model to learn feasibility-aware solution structure during training. To support efficient inference, we introduce a lightweight graph architecture centered on a cost-attention convolution, where edge costs and feasibility information directly shape message passing. Experiments on three problem families demonstrate strong solution quality and efficient inference across diverse edge-selection settings.

Many real-life problems involve multiple conflicting objectives; hence, the decision maker is provided with a set of trade-off solutions, the Pareto front. While many methods to compute Pareto fronts have been proposed in the mathematical programming literature, comparatively few approaches are available for constraint programming (CP). One of the main state-of-the-art algorithms in CP is a branch-and-bound method that uses a Pareto global constraint, denoted here as mobabcp. In this work, we adapt the SAUGMECON algorithm, a well-known and efficient epsilon-constraint method, in a CP solver. We also propose a new algorithm that combines SAUGMECON with the Pareto global constraint. Experimental results show that the proposed algorithm consistently achieves better results than our CP implementation of SAUGMECON and is competitive with mobabcp, outperforming it on several of the studied problems.

Branch-and-bound methods for combinatorial optimization rely critically on the efficient computation of strong bounds during search. Decision diagramÐbased optimization provides such bounds via restricted and relaxed multi-valued decision diagrams (MDDs), but compiling relaxed diagrams can become a computational bottleneck for existing solvers. We present a GPU-accelerated implementation of decision diagramÐbased branch-and-bound using a decoupled architecture. It separates the compilation of relaxed and restricted diagrams and coordinates them through two queues of search states. This design enables heterogeneous parallelization: restricted diagrams are compiled concurrently on CPU threads while relaxed diagrams are constructed in parallel on a GPU. The GPU implementation exploits the layered structure of decision diagrams by expanding states in parallel and performing successor generation, dominance filtering, and state merging on the GPU. Computational experiments on knapsack, maximum independent set, and Golomb ruler benchmarks demonstrate substantial performance improvements over CPU-based decision diagram solvers, including speedups of up to an order of magnitude on hard instances and the ability to solve Golomb ruler instances up to size 16.

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 first introduce a basic Constraint Programming (CP) model to solve MCM. Then, we introduce symmetry breaking rules and a global constraint to ensure them. We experimentally evaluate our approach on a widely used benchmark extracted from a collection of digital filter designs. We show that the basic CP model is competitive with state-of-the-art Integer Linear Programming (ILP) and SAT models, and that the addition of our global symmetry breaking constraint allows us to clearly outperform all other existing approaches on the considered benchmark.

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.

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 for puzzle-style problems 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 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.

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. Across all evaluated logics, it closes at least 30% of the performance gap between the competition winner and the virtual best solver (VBS), and nearly matches the VBS in two logics.

A variety of heuristic search algorithms have been used in Domain-Independent Dynamic Programming (DIDP) for combinatorial optimization. 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 and, 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.

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, with pricing by DIDP, empirically outperform an existing automated B&P solver and B&P with pricing by mixed-integer programming or constraint programming.

Domain-Independent Dynamic Programming (DIDP) is a general framework for solving combinatorial optimization problems using Dynamic Programming (DP), where search 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 introduce 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 use vehicle routing problems as a case study to present GRID 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 mixed-integer programming approaches.

This paper addresses an assembly line balancing problem that combines task assignment, scheduling, and allocation of parallel workstations to minimize cycle time, subject to precedence and shared resource constraints. A key complexity in periodic production environments is the presence of cyclic resource constraints which arise when workers (resources) move between workstations within the same cycle. This scenario is particularly prevalent in large-scale manufacturing industries with long cycle times, such as aerospace assembly. Existing constraint programming (CP) models for this problem schedule tasks on an absolute time horizon. However, this approach relies on modulo operators to project task intervals into a cycle window, which hinders constraint propagation, and makes extending the model beyond fixed factory layouts difficult. We propose a novel cycle-relative CP formulation that addresses both shortcomings. Our model dynamically determines the optimal placement of parallel workstations and defines task decision variables directly within the cycle window, eliminating the need for modulo operators. Experimental evaluations demonstrate the cycle-relative 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.

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.

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.

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

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 explainable graphs (QXGs) 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 QXG 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.

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.

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 greater or equal 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 whether a high-utility UPI exists, for a given utility threshold, is NP-complete. Our global constraint, , integrates utility computation and upper-bound pruning through propagation rules. Experiments demonstrate that our approach performs competitively with the state of the art HUIM algorithms while preserving the modelling flexibility of CP.

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

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.

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. In our setting, the SMS symmetry-breaking propagator is an ordinary IPASIR-UP propagator; the techniques below do not rely on properties specific to symmetry breaking, except in the benchmark instantiations. 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. Our best method reduces total solving time by factors of 2-10x from improved cubing, and reduces the time for the hardest cubes by factors of 2--50x.

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

Given a constraint satisfaction problem (CSP) predicate P subseteq D^r, the non-redundancy (NRD) of P is the maximum-sized instance on n variables such that for every clause of the instance, there is an assignment which satisfies all clauses but that one. 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.