Diverse combinatorial optimization problems can be modeled as instances of the Pseudo-boolean Optimization (PBO) problem. The Predict-and-Search (PaS) framework is a powerful technique applied to Mixed Integer Linear Programming (MIP) that uses Graph Neural Networks (GNNs) to predict candidate variable values for guiding the search process of an optimization solver. Current PaS implementations rely on heuristically chosen labels during training and produce fast, good solutions, sacrificing optimality guarantees. We present Backbone-based Predict and Search (BackPaS), a specialized PaS framework for PBO. Our main contribution is redefining the GNN prediction task to identify backbones—literals fixed across all optimal solutions. Predicting these critical variables accelerates the search toward optimality if the network’s prediction is correct. BackPaS uses a specialized GNN architecture built on a literal-based bipartite graph to predict backbone membership and polarity, formulated as a multi-class classification problem. Then, a parameterized adaptive trust region incorporates these GNN predictions to adjust the solver’s search space. Empirically, we demonstrate that BackPaS effectively learns backbone patterns across PBO benchmarks, including Maximum Independent Set (MIS), Minimum Vertex Cover (MVC), and Combinatorial Auctions (CA). We trained the model on small instances for which we computed their backbones. When tested on much larger instances (up to 6 × the training size), our method achieves significant performance gains compared to the commercial solver Gurobi and the state-of-the-art PaS implementation ConPaS, substantially improving its anytime behavior and demonstrating strong generalization capabilities.
The Quadratic Assignment Problem (QAP) consists of finding a permutation that minimizes a quadratic objective function. Exact methods generally rely on a branch-and-bound procedure, the efficiency of which depends heavily on the quality of its lower bound. In integer linear programming, several bounds have been investigated, exhibiting different trade-offs between speed and quality. The Gilmore-Lawler bound appears to be the most commonly used in practice. It requires solving a linear assignment problem (LAP) for each variable-value pair. We show how to obtain this bound using Singleton Node Consistency (SNC) and LAP. In Cost Function Networks (CFNs), we propose a reformulation that transforms the result of applying LAP to a given variable-value pair into cost functions of arity 1 and 2, which can be added to the original problem. Combined with existing lower bounds for CFNs, including EDAC and a recent CFN propagator for AllDifferent, this method (SNC-LAP-GLB), used as a preprocessing, significantly increases the initial lower bound and accelerates the search, resulting in competitive results on the QAPLIB benchmark. We then propose an extension of the AllDifferent propagator for the Global Cardinality Constraint. It allows us to exploit variable symmetries on some challenging QAPLIB instances, thus improving the results.
We consider the problem of determining the minimax regret of a set of utility vectors, where the minimax regret is defined with respect to a given space of possible weight vectors. We present two novel approaches for this problem. The first one improves on an existing method based on the set of undominated utility vectors, by adding maximum regret upper bounds in order to reduce the number of linear programming computations. Our second approach uses a branch-and-bound algorithm that can be applied when the utility vectors are given in the form of sub-utility functions over a set of Boolean variables. Both of our approaches make heavy use of two particular sets of weight vectors, one that approximates the convex hull of the weight space from within, and the other from without. We show that our two approaches complement each other well, with each one having its own combinations of parameters for which it outperforms the other.
We consider a dynamic stochastic capacity problem in which tasks arrive according to a Poisson Process. Release times, stochastic deadlines and masses characterize tasks. A task might be scheduled within its time windows at a given time slot of bounded mass capacity. Each non-empty slot induces a deterministic setup cost. We aim to define a dynamic scheduling policy that maximizes the expected mass of scheduled tasks minus the setup costs over a long time horizon. This type of problem has many applications in planning, scheduling, and yield management. We use a rolling horizon approach: at each step, a particular case of the Multiple Knapsack with Restriction Assignment must be solved. We present and benchmark myopic heuristics, lookahead heuristics, and the exact solution provided by integer linear programming. We provide an extensive comparison in our dynamic and stochastic context. Finally, rather than searching for the most robust heuristic, we devise an algorithm selection process, based on random forests, to select the most effective heuristic for a given instance, considering its parameters. This achieves significant improvements.
Modern combinatorial solvers can be understood as searching for proofs of unsatisfiability or optimality. The proof system implemented by a solver, therefore, fundamentally shapes solver performance. While propositional resolution is simple and complete for propositional formulas, no existing practical resolution-based system offers unrestricted complete reasoning over integer linear inequalities. We introduce hypercube linear resolution, a new proof system that is both sound and complete for integer linear reasoning. Hypercube linear resolution integrates propositional resolution with Fourier resolution through a new constraint type, the hypercube linear constraint, which captures linear relations within a discrete hypercube. Our main contribution is the theory of the proof system, establishing its soundness and completeness. Our proof system generalises propositional and Fourier resolution, and can be seen as an extended cutting planes proof system. We also provide a conflict-driven search algorithm that exploits the system in practice. Our preliminary experiments demonstrate that the new system reduces conflicts compared to propositional resolution. This shows that the structure captured by hypercube linear constraints can be exploited to improve constraint solving.
Significant advances in practical approaches to maximum satisfiability (MaxSAT) solving have made MaxSAT a viable approach to solving complex NP-hard combinatorial optimization problems. Several recent works have extended single-objective MaxSAT algorithms to the multi-objective setting, enabling the enumeration of Pareto-optimal solutions for problems expressed as multi-objective MaxSAT (MO-MaxSAT). We propose and instantiate an alternative approach to MO-MaxSAT solving. Phrased as an implicit hitting set (IHS) approach, our algorithm works by iteratively invoking a single-objective IHS oracle on a scalarization of the multi-objective instance at hand. Our open-source implementation significantly outperforms an earlier-proposed IHS-style approach and complements the current state of the art in algorithmic approaches to MO-MaxSAT.
We present BaB-PoNN, the first formal verification framework for verified robustness of neural networks that use posit arithmetic. BaB-PoNN reasons under the exact posit-8 operational semantics used at inference time, including quire-8 fused accumulation and a single quire-to-posit rounding per affine layer, so every robustness verdict is sound for the deployed implementation. The framework verifies mixed-budget robustness properties in which perturbations are constrained jointly by (i) the number of input coordinates that may change and (ii) the total number of bit flips across those coordinates. We formalize both local robustness, where search is restricted to a data-driven region of interest, and global robustness, where any coordinate may be perturbed within the same hybrid coordinate-bit neighborhood. BaB-PoNN performs an explicit-state search guided by admissible bounds from coordinate swings and per-bit gains, enabling sound pruning while remaining complete: for each input and budget, it either returns a concrete adversarial witness or proves robustness for the specified neighbourhood. Evaluations on posit-8 multilayer perceptron (MLP) and LeNet-5 convolutional neural network (CNN) architectures trained on MNIST show that BaB-PoNN can verify robustness under non-trivial mixed budgets and locate bit-precise adversarial witnesses.
The vehicle routing problem with stochastic demands is a combinatorial optimization problem that arises in industrial applications such as waste management and facility replenishment. In these applications, one could aim at using a specific number of vehicles to better align with available resources, thereby including a fixed-fleet constraint in the problem. Standard column generation heuristics, that are usually efficient in this context, struggle to handle this additional constraint and cannot quickly produce good feasible solutions, mainly because the labeling algorithm used during the pricing becomes inefficient. We introduce a hybrid pricing heuristic that generates columns by combining a greedy component aiming for a quick generation of good columns, a reinforcement learning module to compute critical routes disregarded by the greedy construction, and a tabu search procedure to explore the search space around the generated routes. We embed our method within an existing restricted master heuristic framework: we first perform a column generation phase using our pricing heuristic to quickly generate a set of high-quality columns, which we then complete with a greedy randomized adaptive search procedure. The resulting restricted master problem is then solved as a mixed-integer program. We evaluate our approach on 40 benchmark instances with up to 60 customers and achieve an average optimality gap of 1% within a 5-min total computation time. Our matheuristic also provides more best average solution cost and optimal solutions than the competing heuristics considered.
Vehicle routing problems aim to efficiently serve customer requests while respecting constraints such as vehicle capacities and delivery time windows. When it is not possible to fulfill all requests, orienteering problems are considered, where only a subset of locations is visited to maximize the total collected scores. This paper presents an open-source implementation of the slack induction by string removals (SISRs) heuristic [9] for three representative variants of the vehicle routing problem. Our implementations match the solution quality of the original solver, and their runtimes scale better with increasing instance sizes. We propose an SISRs extension to solve three variants of the orienteering problem, with specific modifications to address their unique requirements. The developed solver achieves strong performance compared to the current state of the art, computing 49 new best-known solutions and delivering about 85
Decision-Diagram-based Branch-and-Bound solves discrete optimization problems by exploiting bounds provided by two types of bounded-width decision diagram. The first is the restricted decision diagram obtained by discarding less promising states that provide primal bounds. The second is the relaxed decision diagram obtained by state merging that yields a dual bound. Their performance depends heavily on the heuristic used to discard or merge nodes. While traditional methods discard or merge nodes based on the cost, recent research suggests that clustering nodes based on state similarity (e.g., via k-means) can help produce tighter bounds. However, current clustering methods are difficult to apply to complex, non-vector states. We propose to use a more general clustering framework that accepts user-defined distance metrics, allowing it to be applied to any state definition and scales to very large state spaces. We test this approach against standard cost-based strategies on three distinct problems exhibiting different merge-function properties. We additionally introduce a definition framework that characterizes these properties. Our results show that, counter-intuitively, sophisticated clustering does not always pay off, especially when the merge operator produces states that differ greatly from the originals. We provide a detailed analysis explaining when clustering is beneficial versus when simple cost-based strategies suffice, offering some guidelines for solver configuration.
Scheduling is a highly relevant aspect of industrial work. From assigning jobs to machines to creating shift plans for employees; schedules must be created to ensure efficiency, cover requirements and adhere to working regulations. As creating schedules while keeping track of all constraints is often a notoriously difficult job, automated methods can be employed. However, sometimes no solution can be found due to conflicting problem specifications. In this case, it is important to explain which constraints contribute to infeasibility and how the problem can be relaxed. We study the Rotating Workforce Scheduling Problem, for which we develop a framework that generates explanations for instances with incompatible constraints. We show how Minimal Correction Sets can be used to provide detailed explanations for infeasible problems, caused by hard constraint violations or by conflicting optimisation goals. We perform a case study and experiments on (real-life) instances that reveal that explanations can be efficiently generated.
For NP-hard problems like Pseudo-Boolean Optimization (PBO), solver performance varies dramatically across instances, making algorithm selection a critical bottleneck. Current Automatic Algorithm Selection (AAS) systems for PBO depend primarily on static problem features, ignoring crucial dynamic information. In contrast, AAS for Boolean Satisfiability (SAT) has demonstrated that “probing” features, gathered from short solver runs, are essential for making high-quality, time-sensitive predictions. This work improves AAS for PBO by systematically integrating and evaluating these powerful probing features. We investigate their impact across a range of machine learning frameworks, including regression, multiclass/multilabel classification, and a novel hybrid model. This investigation culminates in MetaPB, a new open-source meta-solver that combines both static and probing features for superior solver selection. On benchmarks from the 2024 PBO competition, MetaPB outperforms the best individual solver. Remarkably, it closes the gap with leading commercial solvers, achieving performance competitive with Gurobi while using an entirely open-source portfolio. This study establishes a new state of the art for AAS in PBO and challenges the prevailing view in this domain that algorithm selection should be treated purely as a classification task, highlighting the effectiveness of hybrid, regression-informed approaches.
In space missions, scientific data collected by various instruments must be stored onboard before being downlinked to Earth during designated communication windows. For many long range missions, the available bandwidth is shared according to a priority assigned to each memory buffer during such downlink window. The overlapping Memory Dumping Problem (oMDP) consists in finding the priority assignment that minimizes the highest memory peak. This problem has been shown to be weakly NP-hard and has so far only been addressed with heuristic methods. In this paper, we complete the complexity analysis by proving that the problem is strongly NP-hard in the general case, and we propose the first exact method to solve the oMDP. We present a constraint programming approach combining new global constraints and a heuristic branching strategy, and show that our method is competitive with state-of-the-art heuristics while being more generic and able to produce optimality proofs on small instances.
Decision diagrams (DDs) have emerged as a state-of-the-art method for exact multiobjective integer linear programming. When the DD is too large to fit into memory or the decision-maker prefers a fast approximation to the Pareto frontier, the complete DD must be restricted to a subset of its states (or nodes). We introduce new node-selection heuristics for constructing restricted DDs that produce a high-quality approximation of the Pareto frontier. Depending on the structure of the problem, our heuristics are based on either simple rules, machine learning with feature engineering, or end-to-end deep learning. Experiments on multiobjective knapsack, set packing, and traveling salesperson problems show that our approach is highly effective, recovering over 85% of the Pareto frontier while achieving 2.5× speedups compared to exact DD on average, with very few non-Pareto solutions. The code is available at https://github.com/rahulptel/HMORDD .
Solving parity games is a core problem in formal verification, specifically when using model checking and synthesis methods, which have several industrial-scale applications. In this paper, we propose a constraint-based approach for parity games, built upon a new propagation algorithm that eliminates opponent cycles from the game graph. This approach results in an efficient method that exploits the duality between the players in a parity game. Our implementation within a Lazy Clause Generation framework outperforms all existing constraint-based methods for parity games and performs competitively against the most specialized non-CP-based algorithms—often matching and sometimes exceeding their performance—while retaining the flexibility inherent to general constraint-based approaches. Since new constraints can be easily added, our method provides a flexible framework for refining existing problem formulations to search for preferred solutions by satisfying additional constraints. This feature can also be used to solve parity games where additional quantitative constraints (e.g., cost or resource-bounded requirements) need to be satisfied. We present the theoretical foundations of the approach, an experimental evaluation, and a discussion of the results, including an analysis of different versions of the new propagator.
We study the problem of selecting optimal design parameters for Low-Earth-Orbit (LEO) satellite constellations, where the performance of a design is determined by the maximum Satellite–Ground Link (SGL) duration it enables. The design space spans altitude, inclination, plane count, satellites per plane, and phasing, rendering a full mathematical programming model intractable. We propose a two-layer optimization framework: Bayesian Optimization (BO) explores the constellation design space, while each candidate design is evaluated by solving a large Satellite–Ground Link Scheduling Problem (SGLSP). The SGLSP is solved using PINCH, our fast primal heuristic based on LP-relaxation-guided fixing and clustering. PINCH produces high-quality schedules significantly faster than Gurobi, one of the most advanced commercial mixed-integer linear programming solvers. This acceleration allows BO to evaluate constellation designs for 40 ground stations within hours, making large-scale exploration of the design space computationally feasible. The framework scales to large instances and offers a practical approach for complex space-system design problems with combinatorial structure. Moreover, by modifying the weights in the cost–quality trade-off, the same computational pipeline can be steered toward different design priorities (e.g., longer SGL duration, lower deployment cost, or reduced latency), enabling users to obtain constellation configurations that match their specific requirements and preferences.
Managing railway disruptions is a complex multi-agent routing problem where a single train failure can propagate delays across the network. Traditional approaches rely on heuristic optimization solvers, which are effective but assume access to a global system view and require substantial expert design, limiting their applicability and generalization. Reinforcement learning (RL) offers an alternative by learning adaptive strategies from interactions with the environment. In this paper, we show that none of the available paradigms is sufficient in isolation: (i) heuristic solvers encode valuable global expertise but cannot be deployed directly, (ii) world models improve sample efficiency but struggle to leverage expert knowledge, and (iii) pure RL can adapt policies but often lacks stability without strong guidance. We propose a hybrid framework that integrates the strengths of these approaches. First, imitation learning transfers knowledge from a global expert solver to initialize a neural policy. Then, model-based RL fine-tunes this policy using the DreamerV2 world model to enhance generalization and responsiveness to local perturbations. Our method builds on the Multi-Agent Model-Based Architecture (MAMBA) to model agent interactions and addresses the challenge of transferring expertise from global solvers to decentralized agents operating on local latent observations. Experiments on a train rescheduling problem using the Flatland environment show that our method outperforms MAMBA, improving performance by up to 23 https://github.com/corail-research/Imitation-Guided_World_Models .
Logic-based Benders decomposition (LBBD) effectively combines mixed integer programming and constraint programming to solve difficult optimisation problems. While the decomposition exploits different solution and modelling paradigms, the separation destroys problem information connecting master and subproblem decisions. Alongside cut generation, a standard way of re-introducing this connection is through the addition of valid inequalities in the master problem. These inequalities typically constitute subproblem relaxations and they are usually problem specific and derived by hand. This paper proposes a general approach for deriving valid inequalities and demonstrates how they can be applied to cumulative and disjunctive constraints. In an effort to develop a general purpose LBBD solver, the general derivation of valid inequalities have been implemented as part of a new cumulative constraint handler for SCIP and the effectiveness is evaluated on two variants of scheduling problems. The computational experiments show the potential of applying these general valid inequalities to the master problem.
CP-based Lagrangian filtering has proven to be a reliable method for enhancing constraint programming solvers. The general theory lacks a uniform framework to explain many known observations. This paper introduces such a framework, along with theoretical results and illustrations. We show why optimal Lagrange multipliers are not always the most effective for filtering. We propose a strategy to move the Lagrange multipliers away from the optimal one to launch a gradient descent that leads to filtering. This paper presents an application of this framework to the versatile Multidimensional Knapsack constraint. The algorithm is tested on two well-known problems : the multidimensional knapsack problem and the uncapacitated facility location problem. The results show a significant speed up compared to the traditional CP-based Lagrangian filtering method on both problems.
In this paper, we introduce a novel variant of the Resource-Constrained Project Scheduling Problem (RCPSP), called RCPSP with Transfer Times using Secondary Resources with Instant Self-transfers (RCPSPTT-2I). This variant extends the classical RCPSP by modeling resource transfers between activities and hierarchical resource interactions. Specifically, we consider two types of resources: (i) the primary resources used to execute the activities and (ii) secondary resources that help facilitate transfers of primary resources between activities they execute. Transfer lengths depend on both the pair of activities and the primary resource being transferred. Secondary resources can facilitate part or all of the transfer process, and their own transfers without primary resource are assumed instant. This problem definition captures practical scenarios, such as digital or decision-making secondary resources, that (i) do not require physical movement or (ii) have negligible/constant transfers, combining elements of RCPSP with Transfer Times and RCPSP with First- and Second-Tier Transfers variants from the literature. We formalize RCPSPTT-2I using both Integer Linear Programming and Constraint Programming (CP). These models obtain feasible solutions for most 30-activity instances within a 10-minute runtime but struggle to scale to larger instances. To address this limitation, we introduce a heuristic warm-start and a multi-phase procedure that incrementally refines partial solutions. Computational results show that the multi-phase procedure, combined with the Constraint Programming model, significantly improves scalability and solution quality, while preserving optimality guarantees, making it well-suited for practical instance sizes.
