Volume
LIPIcs, Volume 340
31st International Conference on Principles and Practice of Constraint Programming (CP 2025)
Event
CP 2025, August 10-15, 2025, Glasgow, ScotlandEditor
Publication Details
- published at: 2025-08-08
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-380-5
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 340, CP 2025, Complete Volume
Abstract
LIPIcs, Volume 340, CP 2025, Complete Volume
Cite as
31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 1-870, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Proceedings{delabanda:LIPIcs.CP.2025,
title = {{LIPIcs, Volume 340, CP 2025, Complete Volume}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {1--870},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025},
URN = {urn:nbn:de:0030-drops-242168},
doi = {10.4230/LIPIcs.CP.2025},
annote = {Keywords: LIPIcs, Volume 340, CP 2025, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 0:i-0:xxii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{delabanda:LIPIcs.CP.2025.0,
author = {de la Banda, Maria Garcia},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {0:i--0:xxii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.0},
URN = {urn:nbn:de:0030-drops-242152},
doi = {10.4230/LIPIcs.CP.2025.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Privacy-Preserving SAT Solving (Invited Talk)
Abstract
This is an extended abstract of the invited talk presented at the joint conferences "28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)" and "31st International Conference on Principles and Practice of Constraint Programming (CP 2025)". The talk is based on a series of three papers published previously, and it provides a unified overview of their key ideas and results.
Cite as
Ruzica Piskac. Privacy-Preserving SAT Solving (Invited Talk). In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{piskac:LIPIcs.CP.2025.1,
author = {Piskac, Ruzica},
title = {{Privacy-Preserving SAT Solving}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {1:1--1:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.1},
URN = {urn:nbn:de:0030-drops-238626},
doi = {10.4230/LIPIcs.CP.2025.1},
annote = {Keywords: SAT solving, Privacy-preserving reasoning, Zero-knowledge proofs, Propositional unsatisfiability}
}
Document
Invited Talk
Anytime and Exact Search for Planning Problems: How to explore a DP-based state transition graph with A*, CP and LS? (Invited Talk)
Abstract
Many planning problems may be solved with Dynamic Programming (DP) by decomposing the problem into subproblems which are recursively solved. These decompositions induce state transition graphs which are closely related to decision diagrams [J. N. Hooker, 2013], and where optimal solutions correspond to best paths in these graphs. A* is a well known algorithm which extends Djikstra’s algorithm with heuristics for guiding the path search [Hart et al., 1968]. It is exact (provided that the heuristic function is admissible), but it is not anytime. In other words, it computes a best path but it does not output sub-optimal paths while computing it. Hence, when state transition graphs have exponential sizes, A* may run out of time or memory without producing any solution. Various anytime extensions of A* have been proposed to compute a sequence of paths of increasing quality until finding an optimal path and proving its optimality.
In this talk, we will provide an overview of these exact and anytime extensions of A*, with a more detailed focus on Anytime Column Search (ACS) [Vadlamudi et al., 2012], and Iterative Memory Bounded A* (IMBA*) [L. Libralesso and F. Fontan, 2021]. Both approaches iterate A* searches while bounding the number of states that are stored or expanded at each iteration. We will also show how to combine them with Local Search (LS) in order to find better paths faster, and with bounding and constraint propagation in order to prune the graph, as proposed in [R. Fontaine et al., 2023].
This will be illustrated using the Travelling Salesman Problem (TSP) as a running example. The DP formulation introduced by Bellman in [Bellman, 1962] for the TSP has been extended to handle Time Windows (TWs) in [Christofides et al., 1981], and Time Dependent (TD) cost functions in [Malandraki and Dial, 1996]. It has also been extended to {Vehicle Routing Problems} (VRPs) in [van Hoorn, 2016] and to TD-VRPs in [Rifki et al., 2020]. We will finish by presenting an experimental comparison with state-of-the-art approaches for solving the TSP with TWs on classical benchmarks and on a new benchmark which contains hard Euclidean instances located in the phase transition zone [O. Rifki and C. Solnon, 2025].
Cite as
Christine Solnon. Anytime and Exact Search for Planning Problems: How to explore a DP-based state transition graph with A*, CP and LS? (Invited Talk). In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{solnon:LIPIcs.CP.2025.2,
author = {Solnon, Christine},
title = {{Anytime and Exact Search for Planning Problems: How to explore a DP-based state transition graph with A*, CP and LS?}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {2:1--2:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.2},
URN = {urn:nbn:de:0030-drops-238635},
doi = {10.4230/LIPIcs.CP.2025.2},
annote = {Keywords: Dynamic Programming, A*, Anytime search, Time Dependent TSP-TW}
}
Document
Solving the Agile Earth Observation Satellite Scheduling Problem with CP and Local Search
Abstract
The increasing hunger for remote sensing data fuels a boom in satellite imagery, leading to larger agile Earth observation satellite (AEOS) constellations. Therefore, instances of the AEOS scheduling problem (AEOSSP) has become harder to solve. As most existing approaches to solve AEOSSP are designed for a single spacecraft or smaller constellations in mind, they are not tailored to the need of our industrial partner that is about to launch a constellation of 20 AEOSs. Hence, we designed a local search solver able to schedule observations and downloads at such a scale. It relies on solving a series of sub-problems as travelling salesman problem with time windows (TSPTW), first greedily, then using a CP-SAT exact solver in order to find a solution when the greedy insertion fails. Lastly, it schedules downloads and enforces memory constraints with greedy algorithms. Experiments were carried out on instances from the literature as well as generated instances from a simulator we designed. Our experiments show that using CP to solve the sub-problem significantly improve the solutions, and overall our method is slightly better than state-of-the-art approaches.
Cite as
Valentin Antuori, Damien T. Wojtowicz, and Emmanuel Hebrard. Solving the Agile Earth Observation Satellite Scheduling Problem with CP and Local Search. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 3:1-3:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{antuori_et_al:LIPIcs.CP.2025.3,
author = {Antuori, Valentin and Wojtowicz, Damien T. and Hebrard, Emmanuel},
title = {{Solving the Agile Earth Observation Satellite Scheduling Problem with CP and Local Search}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {3:1--3:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.3},
URN = {urn:nbn:de:0030-drops-238647},
doi = {10.4230/LIPIcs.CP.2025.3},
annote = {Keywords: Local Search, Greedy Algorithms, Aerospace Applications}
}
Document
Conflict Analysis Based on Cutting-Planes for Constraint Programming
Abstract
This paper introduces a novel constraint learning mechanism for Constraint Programming (CP) solvers that integrates cutting planes reasoning into the conflict analysis procedure. Drawing inspiration from Lazy Clause Generation (LCG), our approach, named Lazy Linear Generation (LLG), can generate linear integer inequalities to prune the search space, rather than propositional clauses as in LCG. This combines the strengths of constraint programming (strong propagation through global constraints) with cutting-planes reasoning. We present linear constraint explanations for various arithmetic constraints and the element constraint. An experimental evaluation shows that the improved generality of linear constraints has a practical impact on a CP solver by reducing the number of encountered conflicts in 45% of our benchmark instances. Our analysis and prototype implementation show promising results and are an important step towards a new paradigm to make constraint programming solvers more effective.
Cite as
Robbin Baauw, Maarten Flippo, and Emir Demirović. Conflict Analysis Based on Cutting-Planes for Constraint Programming. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{baauw_et_al:LIPIcs.CP.2025.4,
author = {Baauw, Robbin and Flippo, Maarten and Demirovi\'{c}, Emir},
title = {{Conflict Analysis Based on Cutting-Planes for Constraint Programming}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {4:1--4:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.4},
URN = {urn:nbn:de:0030-drops-238655},
doi = {10.4230/LIPIcs.CP.2025.4},
annote = {Keywords: constraint programming, learning, conflict analysis}
}
Document
Transition Dominance in Domain-Independent Dynamic Programming
Abstract
Domain-independent dynamic programming (DIDP) is a model-based paradigm for dynamic programming (DP) that enables users to define DP models based on a state transition system. Heuristic search-based solvers have demonstrated strong performance in solving combinatorial optimization problems. In this paper, we formally define transition dominance in DIDP, where one transition consistently leads to better solutions than another, allowing the search process to safely ignore dominated transitions. To facilitate the efficient use of transition dominance, we introduce an interface for defining transition dominance and propose the use of state functions to cache values, thereby avoiding redundant computations when verifying transition dominance. Experimental results on DP models across multiple problem classes indicate that incorporating transition dominance and state functions yields a 5 to 10 times speed-up on average for different search algorithms within the DIDP framework compared to the baseline.
Cite as
J. Christopher Beck, Ryo Kuroiwa, Jimmy H. M. Lee, Peter J. Stuckey, and Allen Z. Zhong. Transition Dominance in Domain-Independent Dynamic Programming. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{beck_et_al:LIPIcs.CP.2025.5,
author = {Beck, J. Christopher and Kuroiwa, Ryo and Lee, Jimmy H. M. and Stuckey, Peter J. and Zhong, Allen Z.},
title = {{Transition Dominance in Domain-Independent Dynamic Programming}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {5:1--5:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.5},
URN = {urn:nbn:de:0030-drops-238661},
doi = {10.4230/LIPIcs.CP.2025.5},
annote = {Keywords: Dominance, Dynamic Programming, Combinatorial Optimization}
}
Document
Modeling and Explaining an Industrial Workforce Allocation and Scheduling Problem
Abstract
We present an industrial case on workforce allocation and scheduling in the aircraft manufacturing industry, where available teams need to be assigned to logistical operations. This application presents several challenges such as the scale of the problem, the need for fair workload distribution, and the need for methods for mitigating unforeseen disruptions due to technical malfunctions or incompatible weather conditions. We compare different Constraint Programming (CP) models for the allocation and scheduling problems, with extra focus on modeling the workload balancing component. Additionally, we investigate different techniques for explaining infeasibility of a disrupted schedule, such as conflict computation using Minimal Unsatisfiable Subsets (MUSes) and feasibility restoration using Minimal Correction Subsets (MCSes) or constraint relaxations. Our experimental results show that by using appropriate modeling techniques, the problem can be solved in reasonable time, thereby producing fair schedules. Additionally, we show how invalidated schedules can be explained and restored efficiently to help human operators in solving disruptions to the schedule.
Cite as
Ignace Bleukx, Ryma Boumazouza, Tias Guns, Nadine Laage, and Guillaume Poveda. Modeling and Explaining an Industrial Workforce Allocation and Scheduling Problem. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 6:1-6:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bleukx_et_al:LIPIcs.CP.2025.6,
author = {Bleukx, Ignace and Boumazouza, Ryma and Guns, Tias and Laage, Nadine and Poveda, Guillaume},
title = {{Modeling and Explaining an Industrial Workforce Allocation and Scheduling Problem}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {6:1--6:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.6},
URN = {urn:nbn:de:0030-drops-238670},
doi = {10.4230/LIPIcs.CP.2025.6},
annote = {Keywords: modeling, scheduling, fairness, explanations, feasibility restoration}
}
Document
Optimizing 2D Cutting: A Bin Packing Approach to Minimize Scraps and Maximize Their Reusability
Abstract
In industrial settings, cutting predefined pieces from one or multiple sheets of material is a common optimization challenge. This problem can be formulated as a variant of the 2D bin packing problem, where the edges of the pieces define the cut lines. This paper presents a constraint programming model developed in collaboration with an industrial partner in construction to minimize scrap waste generated when cutting insulation pieces. The model introduces an objective function designed to maximize the reusability of leftover material. To fully leverage the model’s efficiency, an initial process transforms irregular insulation pieces into rectangles using one of four processing methods. A comparative analysis is conducted to evaluate the impact of these methods, as well as to benchmark the model’s results against the partner’s manual approach.
Cite as
Manuel Chastenay, Xavier Zwingmann, Claude-Guy Quimper, and Jonathan Gaudreault. Optimizing 2D Cutting: A Bin Packing Approach to Minimize Scraps and Maximize Their Reusability. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{chastenay_et_al:LIPIcs.CP.2025.7,
author = {Chastenay, Manuel and Zwingmann, Xavier and Quimper, Claude-Guy and Gaudreault, Jonathan},
title = {{Optimizing 2D Cutting: A Bin Packing Approach to Minimize Scraps and Maximize Their Reusability}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {7:1--7:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.7},
URN = {urn:nbn:de:0030-drops-238685},
doi = {10.4230/LIPIcs.CP.2025.7},
annote = {Keywords: Combinatorial optimization, constraint programming, 2D bin packing}
}
Document
Breaking Symmetries with Involutions
Abstract
Symmetry breaking for graphs and other combinatorial objects is notoriously hard. On the one hand, complete symmetry breaks are exponential in size. On the other hand, current, state-of-the-art, partial symmetry breaks are often considered too weak to be of practical use. Recently, the concept of graph patterns has been introduced and provides a concise representation for (large) sets of non-canonical graphs, i.e. graphs that are not lex-leaders and can be excluded from search. In particular, four (specific) graph patterns apply to identify about 3/4 of the set of all non-canonical graphs. Taking this approach further, we discover that graph patterns that derive from permutations that are involutions play an important role in the construction of symmetry breaks for graphs. We take advantage of this to guide the construction of partial and complete symmetry-breaking constraints based on graph patterns. The resulting constraints are small in size and strong in the number of symmetries they break.
Cite as
Michael Codish and Mikoláš Janota. Breaking Symmetries with Involutions. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{codish_et_al:LIPIcs.CP.2025.8,
author = {Codish, Michael and Janota, Mikol\'{a}\v{s}},
title = {{Breaking Symmetries with Involutions}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {8:1--8:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.8},
URN = {urn:nbn:de:0030-drops-238699},
doi = {10.4230/LIPIcs.CP.2025.8},
annote = {Keywords: graph symmetry, patterns, permutation, Ramsey graphs, greedy, CEGAR}
}
Document
Constraint Models for Klondike
Abstract
Klondike is the most famous single-player card game, and remains a challenging search problem even in the "thoughtful" variant where all card locations are known. We consider the full game of Klondike except for one restriction that the unusual move of "worrying back" is disallowed. This model is able to determine the winnability of all instances of the game and in practice does so in less than 2000 secs for 10,000 instances we tested, which no other known algorithm can achieve. On some instances, however, other techniques can produce answers more quickly. We use constraint modelling to produce schedules for running our constraint model in combination with other techniques. The combination outperforms any single solver across a range of time limits. Using this combination we are able to significantly improve the best estimate of winnability of Klondike without worrying back. Finally we show how we can use this work to also improve the estimate of winnability of the regular game of Klondike.
Cite as
Nguyen Dang, Ian P. Gent, Peter Nightingale, Felix Ulrich-Oltean, and Jack Waller. Constraint Models for Klondike. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dang_et_al:LIPIcs.CP.2025.9,
author = {Dang, Nguyen and Gent, Ian P. and Nightingale, Peter and Ulrich-Oltean, Felix and Waller, Jack},
title = {{Constraint Models for Klondike}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {9:1--9:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.9},
URN = {urn:nbn:de:0030-drops-238702},
doi = {10.4230/LIPIcs.CP.2025.9},
annote = {Keywords: AI Planning, Modelling, Constraint Programming, Solitaire and Patience Games}
}
Document
Unit Types for MiniZinc
Abstract
Discrete optimization models often reason about discrete sets of objects, but discrete optimization solvers only deal with integers. One of the key challenges when building models for discrete optimization problems is avoiding bugs. Because the model only defines constraints, decisions, and an objective that are then run on a solver, bugs in the model can be very difficult to track down. Hence, modelling languages should have strong type systems to detect as many bugs as possible at the modelling level. In this paper, we propose unit types for MiniZinc. Unit types allow us to differentiate between different integers appearing in the model. Almost all integer decisions in models are either about a set of objects or some measurable resource type. Using unit types, we can add more type safety to our models by avoiding confusion of decisions on different resource types. Compared to other programming languages, unit types in our proposal are unusual. MiniZinc models often deal with multiple levels of granularity of the same resource, e.g., scheduling to the minute, but doing resource allocation on the half day, or use an unspecified granularity, e.g., the same job-shop scheduling model could use task durations given in minutes or days. Our proposed unit types also differentiate between coordinate unit types, e.g., the time when an event occurred, and the usual delta unit types, e.g., the time difference between two events. Errors arising from mixing coordinate and delta types can be very challenging to debug, so we extend the type system to track this for us.
Cite as
Jip J. Dekker, Jason Nguyen, Peter J. Stuckey, and Guido Tack. Unit Types for MiniZinc. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dekker_et_al:LIPIcs.CP.2025.10,
author = {Dekker, Jip J. and Nguyen, Jason and Stuckey, Peter J. and Tack, Guido},
title = {{Unit Types for MiniZinc}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {10:1--10:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.10},
URN = {urn:nbn:de:0030-drops-238718},
doi = {10.4230/LIPIcs.CP.2025.10},
annote = {Keywords: Modelling, Type Safety, Unit Types}
}
Document
Cargo Routing Optimization in Liner Shipping Networks
Abstract
Given a maritime liner network, the cargo routing problem consists of determining which maritime routes containers will take to be transported from their loading port to their destination port. This constrained optimization problem is an essential task in the context of maritime commodity transportation, both in terms of network design and operational implementation. Several variants of this problem have been considered depending on their usage (e.g. for designing the network or for carrying containers in practice), the constraints taken into account or the criterion to be optimized.
In this article, we address several variants of this problem, relying on the flexibility of Constraint Programming. First, we propose two general COP models. Then, we describe a local search method that can be easily adapted to the desired context. Finally, we experimentally compare our two models and the proposed method.
Cite as
Yousra El Ghazi, Djamal Habet, and Cyril Terrioux. Cargo Routing Optimization in Liner Shipping Networks. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{elghazi_et_al:LIPIcs.CP.2025.11,
author = {El Ghazi, Yousra and Habet, Djamal and Terrioux, Cyril},
title = {{Cargo Routing Optimization in Liner Shipping Networks}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {11:1--11:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.11},
URN = {urn:nbn:de:0030-drops-238720},
doi = {10.4230/LIPIcs.CP.2025.11},
annote = {Keywords: Constraint optimization problem, modeling, solving, industrial application}
}
Document
An Expansion-Based Approach for Quantified Integer Programming
Abstract
Quantified Integer Programming (QIP) bridges multiple domains by extending Quantified Boolean Formulas (QBF) to incorporate general integer variables and linear constraints while also generalizing Integer Programming through variable quantification. As a special case of Quantified Constraint Satisfaction Problems (QCSP), QIP provides a versatile framework for addressing complex decision-making scenarios. Additionally, the inclusion of a linear objective function enables QIP to effectively model multistage robust discrete linear optimization problems, making it a powerful tool for tackling uncertainty in optimization.
While two primary solution paradigms exist for QBF - search-based and expansion-based approaches - only search-based methods have been explored for QIP and QCSP. We introduce an expansion-based approach for QIP using Counterexample-Guided Abstraction Refinement (CEGAR), adapting techniques from QBF. We extend this methodology to tackle multistage robust discrete optimization problems with linear constraints and further embed it in an optimization framework, enhancing its applicability. Our experimental results highlight the advantages of this approach, demonstrating superior performance over existing search-based solvers for QIP in specific instances. Furthermore, the ability to model problems using linear constraints enables notable performance gains over state-of-the-art expansion-based solvers for QBF.
Cite as
Michael Hartisch and Leroy Chew. An Expansion-Based Approach for Quantified Integer Programming. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 12:1-12:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{hartisch_et_al:LIPIcs.CP.2025.12,
author = {Hartisch, Michael and Chew, Leroy},
title = {{An Expansion-Based Approach for Quantified Integer Programming}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {12:1--12:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.12},
URN = {urn:nbn:de:0030-drops-238736},
doi = {10.4230/LIPIcs.CP.2025.12},
annote = {Keywords: Quantified Integer Programming, Quantified Constraint Satisfaction, Robust Discrete Optimization, Expansion, CEGAR}
}
Document
Disjunctive Scheduling in Tempo
Abstract
In this paper we introduce a constraint programming lazy clause and literal generation solver embarking ideas from SAT Modulo theories. A key aspect of the solver are Boolean variables with an associated semantic in difference logic, i.e., systems of binary numeric difference constraints or edges, making it particularly adapted to scheduling and other temporal problems. We apply this solver to disjunctive scheduling problems, where edges are used as branching variables, can be inferred via the edge finding rule as well as by transitivity reasoning, and can in turn strengthen propagation via temporal graph reasoning. Our experiments on job-shop scheduling show that a deep integration of these techniques makes our solver competitive with state-of-the-art approaches on these problems.
Cite as
Emmanuel Hebrard. Disjunctive Scheduling in Tempo. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{hebrard:LIPIcs.CP.2025.13,
author = {Hebrard, Emmanuel},
title = {{Disjunctive Scheduling in Tempo}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {13:1--13:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.13},
URN = {urn:nbn:de:0030-drops-238746},
doi = {10.4230/LIPIcs.CP.2025.13},
annote = {Keywords: Scheduling, Constraint solvers, Clause-learning}
}
Document
Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification
Abstract
Formal verification of arithmetic circuits using computer algebra has been shown to be highly successful. The circuit is encoded as a system of polynomials, which automatically generates a lexicographic Gröbner basis. Correctness is then verified by computing the polynomial remainder of the specification. To optimize the remainder computation, prior work extracts linear polynomials. However, this required recomputing a Gröbner basis with respect to a degree-compatible order.
In this paper, we show that this computationally expensive step is unnecessary and propose a novel hybrid verification approach that combines an FGLM-style linearization technique with a guess-and-prove method using SAT solving to derive the linear relations directly from lexicographic Gröbner bases. We enhance our approach using caching techniques and propagating vanishing monomials. Our experimental results demonstrate that our method significantly outperforms previous linearization techniques.
Cite as
Clemens Hofstadler and Daniela Kaufmann. Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{hofstadler_et_al:LIPIcs.CP.2025.14,
author = {Hofstadler, Clemens and Kaufmann, Daniela},
title = {{Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {14:1--14:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.14},
URN = {urn:nbn:de:0030-drops-238752},
doi = {10.4230/LIPIcs.CP.2025.14},
annote = {Keywords: Computer Algebra, FGLM, And-Inverter Graphs, Hardware Verification}
}
Document
Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets
Abstract
We propose symmetric core learning (SCL) as a novel approach to making the implicit hitting set approach (IHS) to constraint optimization more symmetry-aware. SCL has the potential of significantly reducing the number of iterations and, in particular, the number of calls to an NP decision solver for extracting individual unsatisfiable cores. As the technique is focused on generating symmetric cores to the hitting set component of IHS, SCL is generally applicable in IHS-style search for essentially any constraint optimization paradigm. In this work, we focus in particular on integrating SCL to IHS for pseudo-Boolean optimization (PBO), as earlier proposed static symmetry breaking through lex-leader constraints generated before search turns out to often degrade the performance of the IHS approach to PBO. In contrast, we show that SCL can improve the runtime performance of a state-of-the-art IHS approach to PBO and generally does not impose significant overhead in terms of runtime performance.
Cite as
Hannes Ihalainen, Jeremias Berg, Matti Järvisalo, and Bart Bogaerts. Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 15:1-15:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{ihalainen_et_al:LIPIcs.CP.2025.15,
author = {Ihalainen, Hannes and Berg, Jeremias and J\"{a}rvisalo, Matti and Bogaerts, Bart},
title = {{Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {15:1--15:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.15},
URN = {urn:nbn:de:0030-drops-238767},
doi = {10.4230/LIPIcs.CP.2025.15},
annote = {Keywords: Implicit hitting sets, symmetries, unsatisfiable cores, pseudo-Boolean optimization}
}
Document
PrintTalk: A Language for Constraint-Based 3D Modelling
Abstract
Programmatic CAD (PCAD) is an emerging alternative to traditional visual CAD software. However, state-of-the-art PCAD tools have limited or no support for constraints. Consequently, these tools depend solely on parametrisation for variability, reusability, and composition of shapes. This leads to problems such as parameter explosion, leaky compositional abstraction, and prevents a declarative approach to defining spatial patterns (linear, grid, circular, etc.) for the constituents of a composition. This paper describes the design of PrintTalk, a PCAD language that supports 3D modelling by composing shapes and expressing relations between them using first-class constraints. Evaluating PrintTalk against state-of-the-art PCAD tools demonstrates that its expressive abstraction and composition mechanisms facilitate the design and promotes the reuse of shapes.
Cite as
Jef Jacobs, Wolfgang De Meuter, and Jens Nicolay. PrintTalk: A Language for Constraint-Based 3D Modelling. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 16:1-16:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{jacobs_et_al:LIPIcs.CP.2025.16,
author = {Jacobs, Jef and De Meuter, Wolfgang and Nicolay, Jens},
title = {{PrintTalk: A Language for Constraint-Based 3D Modelling}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {16:1--16:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.16},
URN = {urn:nbn:de:0030-drops-238775},
doi = {10.4230/LIPIcs.CP.2025.16},
annote = {Keywords: Programmatic 3D Modelling, PCAD, Domain specific language, Constraints}
}
Document
Scalable Counting of Minimal Trap Spaces and Fixed Points in Boolean Networks
Abstract
Boolean Networks (BNs) serve as a fundamental modeling framework for capturing complex dynamical systems across various domains, including systems biology, computational logic, and artificial intelligence. A crucial property of BNs is the presence of trap spaces - subspaces of the state space that, once entered, cannot be exited. Minimal trap spaces, in particular, play a significant role in analyzing the long-term behavior of BNs, making their efficient enumeration and counting essential. The fixed points in BNs are a special case of minimal trap spaces. In this work, we formulate several meaningful counting problems related to minimal trap spaces and fixed points in BNs. These problems provide valuable insights both within BN theory (e.g., in probabilistic reasoning and dynamical analysis) and in broader application areas, including systems biology, abstract argumentation, and logic programming. To address these computational challenges, we propose novel methods based on approximate answer set counting, leveraging techniques from answer set programming. Our approach efficiently approximates the number of minimal trap spaces and the number of fixed points without requiring exhaustive enumeration, making it particularly well-suited for large-scale BNs. Our experimental evaluation on an extensive and diverse set of benchmark instances shows that our methods significantly improve the feasibility of counting minimal trap spaces and fixed points, paving the way for new applications in BN analysis and beyond.
Cite as
Mohimenul Kabir, Van-Giang Trinh, Samuel Pastva, and Kuldeep S Meel. Scalable Counting of Minimal Trap Spaces and Fixed Points in Boolean Networks. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 17:1-17:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kabir_et_al:LIPIcs.CP.2025.17,
author = {Kabir, Mohimenul and Trinh, Van-Giang and Pastva, Samuel and Meel, Kuldeep S},
title = {{Scalable Counting of Minimal Trap Spaces and Fixed Points in Boolean Networks}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {17:1--17:26},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.17},
URN = {urn:nbn:de:0030-drops-238780},
doi = {10.4230/LIPIcs.CP.2025.17},
annote = {Keywords: Computational systems biology, Boolean network, Fixed point, Trap space, Answer set counting, Projected counting, Abstract argumentation, Logic programming}
}
Document
Greed Is Slow on Sparse Graphs of Oriented Valued Constraints
Abstract
Greedy local search is especially popular for solving valued constraint satisfaction problems (VCSPs). Since any method will be slow for some VCSPs, we ask: what is the simplest VCSP on which greedy local search is slow? We construct a VCSP on 6n Boolean variables for which greedy local search takes 7(2ⁿ - 1) steps to find the unique peak. Our VCSP is simple in two ways. First, it is very sparse: its constraint graph has pathwidth 2 and maximum degree 3. This is the simplest VCSP on which some local search could be slow. Second, it is "oriented" – there is an ordering on the variables such that later variables are conditionally-independent of earlier ones. Being oriented allows many non-greedy local search methods to find the unique peak in a quadratic number of steps. Thus, we conclude that - among local search methods - greed is particularly slow.
Cite as
Artem Kaznatcheev and Sofia Vazquez Alferez. Greed Is Slow on Sparse Graphs of Oriented Valued Constraints. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 18:1-18:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kaznatcheev_et_al:LIPIcs.CP.2025.18,
author = {Kaznatcheev, Artem and Vazquez Alferez, Sofia},
title = {{Greed Is Slow on Sparse Graphs of Oriented Valued Constraints}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {18:1--18:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.18},
URN = {urn:nbn:de:0030-drops-238793},
doi = {10.4230/LIPIcs.CP.2025.18},
annote = {Keywords: valued constraint satisfaction problem, local search, algorithm analysis, constraint graphs}
}
Document
Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability
Abstract
Synchronous unison is a classical clock synchronization problem in distributed computing, and especially in self-stabilization. This paper explores the self-stabilization of a synchronous unison algorithm proposed by Arora et al. using a propositional satisfiability-based approach. We give a logical formulation of the algorithm. This formulation includes the uniqueness of clock values at each node, the updates of clocks based on the minimum clock value in the neighborhood, and the detection of convergence or divergence. To optimize the models, additional constraints are introduced to reduce redundant cases of initial configurations to be analyzed. Our approach not only verifies the algorithm’s behaviour but also offers insights into enhancing its robustness and applicability to broader distributed systems.
Cite as
Asma Khoualdia, Sami Cherif, Stéphane Devismes, and Léo Robert. Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 19:1-19:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{khoualdia_et_al:LIPIcs.CP.2025.19,
author = {Khoualdia, Asma and Cherif, Sami and Devismes, St\'{e}phane and Robert, L\'{e}o},
title = {{Analyzing Self-Stabilization of Synchronous Unison via Propositional Satisfiability}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {19:1--19:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.19},
URN = {urn:nbn:de:0030-drops-238806},
doi = {10.4230/LIPIcs.CP.2025.19},
annote = {Keywords: Self-stabilization, Synchronous Unison, Satisfiability}
}
Document
Dependency-Curated Large Neighbourhood Search
Abstract
In large neighbourhood search (LNS), an incumbent initial solution is incrementally improved by selecting a subset of the variables, called the freeze set, and fixing them to their values in the incumbent solution, while a value for each remaining variable is found and assigned via solving (such as constraint programming-style propagation and search). Much research has been performed on finding generic and problem-specific LNS selection heuristics that select freeze sets that lead to high-quality solutions. In constraint-based local search (CBLS), the relations between the variables via the constraints are fundamental and well-studied, as they capture dependencies of the variables. In this paper, we apply these ideas from CBLS to the LNS context, presenting the novel dependency curation scheme, which exploits them to find a low-cardinality set of variables that the freeze set of any selection heuristic should be a subset of. The scheme often improves the overall performance of generic selection heuristics. Even when the scheme is used with a naïve generic selection heuristic that selects random freeze sets, the performance is competitive with more elaborate generic selection heuristics.
Cite as
Frej Knutar Lewander, Pierre Flener, and Justin Pearson. Dependency-Curated Large Neighbourhood Search. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{knutarlewander_et_al:LIPIcs.CP.2025.20,
author = {Knutar Lewander, Frej and Flener, Pierre and Pearson, Justin},
title = {{Dependency-Curated Large Neighbourhood Search}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {20:1--20:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.20},
URN = {urn:nbn:de:0030-drops-238810},
doi = {10.4230/LIPIcs.CP.2025.20},
annote = {Keywords: Combinatorial Optimisation, Large Neighbourhood Search (LNS), Constraint-Based Local Search (CBLS)}
}
Document
Practically Feasible Proof Logging for Pseudo-Boolean Optimization
Abstract
Certifying solvers have long been standard for decision problems in Boolean satisfiability (SAT), allowing for proof logging and checking with very limited overhead, but developing similar tools for combinatorial optimization has remained a challenge. A recent promising approach covering a wide range of solving paradigms is pseudo-Boolean proof logging, but this has mostly consisted of proof-of-concept works far from delivering the performance required for real-world deployment.
In this work, we present an efficient toolchain based on VeriPB and CakePB for formally verified pseudo-Boolean optimization. We implement proof logging for the full range of techniques in the state-of-the-art solvers RoundingSat and Sat4j, including core-guided search and linear programming integration with Farkas certificates and cut generation. Our experimental evaluation shows that proof logging and checking performance in this much more expressive paradigm is now quite close to the level of SAT solving, and hence is clearly practically feasible.
Cite as
Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, and Marc Vinyals. Practically Feasible Proof Logging for Pseudo-Boolean Optimization. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 21:1-21:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{koops_et_al:LIPIcs.CP.2025.21,
author = {Koops, Wietze and Le Berre, Daniel and Myreen, Magnus O. and Nordstr\"{o}m, Jakob and Oertel, Andy and Tan, Yong Kiam and Vinyals, Marc},
title = {{Practically Feasible Proof Logging for Pseudo-Boolean Optimization}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {21:1--21:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.21},
URN = {urn:nbn:de:0030-drops-238825},
doi = {10.4230/LIPIcs.CP.2025.21},
annote = {Keywords: proof logging, certifying algorithms, combinatorial optimization, certification, pseudo-Boolean solving, 0-1 integer linear programming}
}
Document
Learning to Bound for Maximum Common Subgraph Algorithms
Abstract
Identifying the maximum common subgraph between two graphs is a computationally challenging NP-hard problem. While the McSplit algorithm represents a state-of-the-art approach within a branch-and-bound (BnB) framework, several extensions have been proposed to enhance its vertex pair selection strategy, often utilizing reinforcement learning techniques. Nonetheless, the quality of the upper bound remains a critical factor in accelerating the search process by effectively pruning unpromising branches. This research introduces a novel, more restrictive upper bound derived from a detailed analysis of the McSplit algorithm’s generated partitions. To enhance the effectiveness of this bound, we propose a reinforcement learning approach that strategically directs computational effort towards the most promising regions within the search space.
Cite as
Buddhi W. Kothalawala, Henning Koehler, and Qing Wang. Learning to Bound for Maximum Common Subgraph Algorithms. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kothalawala_et_al:LIPIcs.CP.2025.22,
author = {Kothalawala, Buddhi W. and Koehler, Henning and Wang, Qing},
title = {{Learning to Bound for Maximum Common Subgraph Algorithms}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {22:1--22:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.22},
URN = {urn:nbn:de:0030-drops-238837},
doi = {10.4230/LIPIcs.CP.2025.22},
annote = {Keywords: Combinatorial Search, Branch and Bound, Graph Theory}
}
Document
RPID: Rust Programmable Interface for Domain-Independent Dynamic Programming
Abstract
In domain-independent dynamic programming (DIDP), a problem is formulated as a dynamic programming (DP) model and then solved by a general-purpose solver. In the existing software for DIDP, a model is defined using expressions composed of a predefined set of operations. In this paper, we propose the Rust Programmable Interface for DIDP (RPID), new software for DIDP, where a model is defined by Rust functions. We discuss the design of RPID and compare it with existing DP-based frameworks, including decision diagram-based (DD-based) solvers. In our experiments, RPID is up to hundreds of times faster than the existing DIDP implementation with the same models. In addition, new DIDP models, enabled by the flexibility of RPID, outperform existing models in multiple problem classes. We also show that the relative performance of RPID and existing DD-based solvers depends on problem class with, so far, no clear dominant solver technology.
Cite as
Ryo Kuroiwa and J. Christopher Beck. RPID: Rust Programmable Interface for Domain-Independent Dynamic Programming. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kuroiwa_et_al:LIPIcs.CP.2025.23,
author = {Kuroiwa, Ryo and Beck, J. Christopher},
title = {{RPID: Rust Programmable Interface for Domain-Independent Dynamic Programming}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {23:1--23:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.23},
URN = {urn:nbn:de:0030-drops-238845},
doi = {10.4230/LIPIcs.CP.2025.23},
annote = {Keywords: Decision Diagrams \& Dynamic Programming, Modelling \& Modelling Languages}
}
Document
The Work Task Variation Problem
Abstract
This paper introduces the Work Task Variation (WTV) problem, a novel scheduling post-processing challenge focused on improving worker shift quality by rearranging tasks within their assigned time slots. The objective is to avoid excessively short or long durations of specific task types, creating smoother and more ergonomic work patterns.
We present RosterLogic Variation, a constraint-based local search (CBLS) inspired solver originally developed at Optischedule and successfully deployed in real-world retail settings. This solver rapidly improves existing schedules using tailored invariants and heuristics. We also provide a complete MiniZinc model and a set of generated realistic publicly available benchmark instances.
We compare our solver’s performance with that of modern CP solvers using the MiniZinc model. Contemporary state-of-the-art CP solvers are approaching the interactive performance of our CBLS solver for coarse planning, representing a significant advancement since the original design and implementation of our solver.
Cite as
Mikael Z. Lagerkvist and Magnus Rattfeldt. The Work Task Variation Problem. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 24:1-24:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{lagerkvist_et_al:LIPIcs.CP.2025.24,
author = {Lagerkvist, Mikael Z. and Rattfeldt, Magnus},
title = {{The Work Task Variation Problem}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {24:1--24:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.24},
URN = {urn:nbn:de:0030-drops-238850},
doi = {10.4230/LIPIcs.CP.2025.24},
annote = {Keywords: Constraint-Based Local Search, Constraint Programming, Metaheuristics, Scheduling}
}
Document
Aircraft Resource-Constrained Assembly Line Balancing with Learning Effect: A Constraint Programming Approach
Abstract
Balancing aeronautical assembly lines is a major challenge in modern aerospace manufacturing. Aircraft manufacturing plants typically have a predetermined production rate, but the production system requires a period of adaptation at start-up. This phenomenon, known as the learning effect, refers to the gradual improvement in efficiency through task repetition, thereby reducing task duration. However, the stability of an assembly line is also a critical factor, as any change in the production process incurs costs. In this study, Constraint Programming (CP) is used to optimise assembly line balancing, taking into account the learning effect to address the trade-off between achieving target production rates and minimising adjustments to the line.
Cite as
Duc Anh Le, Stéphanie Roussel, and Christophe Lecoutre. Aircraft Resource-Constrained Assembly Line Balancing with Learning Effect: A Constraint Programming Approach. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 25:1-25:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{le_et_al:LIPIcs.CP.2025.25,
author = {Le, Duc Anh and Roussel, St\'{e}phanie and Lecoutre, Christophe},
title = {{Aircraft Resource-Constrained Assembly Line Balancing with Learning Effect: A Constraint Programming Approach}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {25:1--25:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.25},
URN = {urn:nbn:de:0030-drops-238863},
doi = {10.4230/LIPIcs.CP.2025.25},
annote = {Keywords: Assembly Line Balancing, Resource-Constrained, Learning Effect, Ramp-Up, Aeronautic, Constraint Programming, Dominance-Breaking}
}
Document
Parallel MIP Solving with Dynamic Task Decomposition
Abstract
Mixed Integer Programming (MIP) is a foundational model in operations research. Although significant progress has been made in enhancing sequential MIP solvers through sophisticated techniques and heuristics, remarkable developments in computing resources have made parallel solving a promising direction for performance improvement. In this work, we propose a novel parallel MIP solving framework that employs dynamic task decomposition in a divide-and-conquer paradigm. Our framework incorporates a hardness estimate heuristic to identify challenging solving tasks and a reward decaying mechanism to reinforce the task decomposition decision. We apply our framework to two state-of-the-art open-source MIP solvers, SCIP and HiGHS, yielding efficient parallel solvers. Extensive experiments on the full MIPLIB benchmark, using up to 128 cores, demonstrate that our framework yields substantial performance improvements over modern divide-and-conquer parallel solvers. Moreover, our parallel solvers have established new best known solutions for 16 open MIPLIB instances.
Cite as
Peng Lin, Shaowei Cai, Mengchuan Zou, and Shengqi Chen. Parallel MIP Solving with Dynamic Task Decomposition. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 26:1-26:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{lin_et_al:LIPIcs.CP.2025.26,
author = {Lin, Peng and Cai, Shaowei and Zou, Mengchuan and Chen, Shengqi},
title = {{Parallel MIP Solving with Dynamic Task Decomposition}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {26:1--26:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.26},
URN = {urn:nbn:de:0030-drops-238871},
doi = {10.4230/LIPIcs.CP.2025.26},
annote = {Keywords: Mixed Integer Programming, Parallel Computing, Complete Search, Task Decomposition}
}
Document
Understanding the Impact of Value Selection Heuristics in Scheduling Problems
Abstract
It has been observed that value selection heuristics have less impact than other heuristic choices when solving hard combinatorial optimization (CO) problems. It is often thought that this is because more time is spent on unsatisfiable sub-problems where the value ordering is irrelevant. In this paper we investigate this belief in the scheduling domain and come up with a more detailed explanation. We find that, even though there are less relevant choices to be made on hard instances, each mistake tends to have a bigger impact, to a point where the potential gain from a value heuristic predominates. Moreover, we observe two interesting and relatively surprising phenomena when solving scheduling problems. First, the accuracy of a given value selection heuristic decreases with the optimality gap. Second, the computational penalty of a mistake increases with the accuracy of the heuristic. For the first observation, we argue that on hard problems, constraint propagation removes a large portion of choices that align with the intuition behind the heuristic. This means that the heuristic faces mostly difficult choices. For the second observation, we argue that simple heuristics tend to make more mistakes on intuitive choice points, and the computational cost for refuting these mistakes is smaller than for those made by a more accurate heuristic.
Cite as
Tim Luchterhand, Emmanuel Hebrard, and Sylvie Thiébaux. Understanding the Impact of Value Selection Heuristics in Scheduling Problems. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{luchterhand_et_al:LIPIcs.CP.2025.27,
author = {Luchterhand, Tim and Hebrard, Emmanuel and Thi\'{e}baux, Sylvie},
title = {{Understanding the Impact of Value Selection Heuristics in Scheduling Problems}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {27:1--27:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.27},
URN = {urn:nbn:de:0030-drops-238885},
doi = {10.4230/LIPIcs.CP.2025.27},
annote = {Keywords: Scheduling, Branching Heuristics, Constraint Programming}
}
Document
SLS-Enhanced Core-Boosted Linear Search for Anytime Maximum Satisfiability
Abstract
Maximum Satisfiability (MaxSAT), the constraint paradigm of minimizing a linear expression over Boolean (0-1) variables subject to a set of propositional clauses, is today used for solving NP-hard combinatorial optimization problems in various domains. Especially anytime MaxSAT solvers that compute low-cost solutions within a limited available computational time have significantly improved in recent years. Such solvers can be divided into SAT-based methods that use sophisticated reasoning, and stochastic local search (SLS) methods that heuristically explore the search space. The two are complementary; roughly speaking, SLS struggles with finding feasible solutions, and SAT-based methods with minimizing cost. Consequently, most state-of-the-art anytime MaxSAT solvers run SLS before a SAT-based algorithm with minimal communication between the two.
In this paper, we aim to harness the complementary strengths of SAT-based, and SLS approaches in the context of anytime MaxSAT. More precisely, we describe several ways to enhance the performance of the so-called core-boosted linear search algorithm for anytime MaxSAT with SLS techniques. Core-boosted linear search is a three-phase algorithm where each phase uses different types of reasoning. Beyond MaxSAT, core-boosted search has also been successful in the related paradigms of pseudo-boolean optimization and constraint programming. We describe how an SLS approach to MaxSAT can be tightly integrated with all three phases of the algorithm, resulting in non-trivial information exchange in both directions between the SLS algorithm and the reasoning methods. We evaluate our techniques on standard benchmarks from the latest MaxSAT Evaluation and demonstrate that our techniques can noticeably improve on implementations of core-boosted search and SLS.
Cite as
Ole Lübke and Jeremias Berg. SLS-Enhanced Core-Boosted Linear Search for Anytime Maximum Satisfiability. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{lubke_et_al:LIPIcs.CP.2025.28,
author = {L\"{u}bke, Ole and Berg, Jeremias},
title = {{SLS-Enhanced Core-Boosted Linear Search for Anytime Maximum Satisfiability}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {28:1--28:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.28},
URN = {urn:nbn:de:0030-drops-238897},
doi = {10.4230/LIPIcs.CP.2025.28},
annote = {Keywords: Maximum Satisfiability, MaxSAT, SAT, SLS, Anytime Optimization}
}
Document
From Prediction to Action: A Constraint-Based Approach to Predictive Policing
Abstract
Crime prevention in urban environments demands both accurate crime forecasting and the efficient deployment of limited law enforcement resources. In this paper, we present an integrated framework that combines a machine learning module (i.e. PredRNN++ [Wang et al., 2018]) for spatiotemporal crime prediction with a constraint programming module for patrol route optimization. Our approach operates within the ICON loop framework [Bessiere et al., 2017], facilitating iterative refinement of predictions and immediate adaptation of patrol strategies. We validate our method using the City of Chicago Crime Dataset. Experimental results show that routes informed by crime predictions significantly outperform strategies relying solely on historical patterns or operational constraints. These findings illustrate how coupling predictive analytics with constraint programming can substantially enhance resource allocation and overall crime deterrence.
Cite as
Younes Mechqrane and Ismail Elabbassi. From Prediction to Action: A Constraint-Based Approach to Predictive Policing. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{mechqrane_et_al:LIPIcs.CP.2025.29,
author = {Mechqrane, Younes and Elabbassi, Ismail},
title = {{From Prediction to Action: A Constraint-Based Approach to Predictive Policing}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {29:1--29:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.29},
URN = {urn:nbn:de:0030-drops-238902},
doi = {10.4230/LIPIcs.CP.2025.29},
annote = {Keywords: Inductive Constraint Programming (ICON) Loop, Next Frame Prediction, PredRNN++}
}
Document
Exact Methods for the Travelling Salesperson Problem with Self-Deleting Graphs
Abstract
Finding the minimal-cost closed loop on a weighted graph where every vertex is visited exactly once is known as the Travelling Salesperson Problem (TSP). In a recently proposed variant, TSP with Self-Deleting graphs (TSP-SD), visiting a vertex i deletes a set of edges in the graph, preventing their subsequent traversal. Due to the dependency between vertex visits and edge deletion, in TSP-SD the feasibility of a cycle depends on the start node. The best performing solution approaches in the literature rely on a simple problem reformulation to find a backward tour where vertex visits add edges rather than delete them. This paper investigates exact model-based approaches, specifically Constraint Programming (CP), Domain-Independent Dynamic Programming (DIDP), and Mixed Integer Linear Programming (MIP) to solve TSP-SD. We show that simple preprocessing can substantially reduce the options for start/end vertex pairs but typically has a limited positive impact on search performance. Our numerical results demonstrate that the difference between the deletion and addition variants is small for CP and MIP but that the reformulation is critical for DIDP performance. Overall, the DIDP addition model is the best of the exact methods on all test instances and outperforms existing heuristic solvers for small and medium-sized instances while trailing in terms of solution quality on larger instances.
Cite as
Daniel Pekar and J. Christopher Beck. Exact Methods for the Travelling Salesperson Problem with Self-Deleting Graphs. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{pekar_et_al:LIPIcs.CP.2025.30,
author = {Pekar, Daniel and Beck, J. Christopher},
title = {{Exact Methods for the Travelling Salesperson Problem with Self-Deleting Graphs}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {30:1--30:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.30},
URN = {urn:nbn:de:0030-drops-238914},
doi = {10.4230/LIPIcs.CP.2025.30},
annote = {Keywords: Decision Diagrams \& Dynamic Programming, Operations Research \& Mathematical Optimization, Modelling \& Modelling Languages}
}
Document
Transformer-Based Feature Learning for Algorithm Selection in Combinatorial Optimisation
Abstract
Given a combinatorial optimisation problem, there are typically multiple ways of modelling it for presentation to an automated solver. Choosing the right combination of model and target solver can have a significant impact on the effectiveness of the solving process. The best combination of model and solver can also be instance-dependent: there may not exist a single combination that works best for all instances of the same problem. We consider the task of building machine learning models to automatically select the best combination for a problem instance. Critical to the learning process is to define instance features, which serve as input to the selection model. Our contribution is the automatic learning of instance features directly from the high-level representation of a problem instance using a transformer encoder. We evaluate the performance of our approach using the Essence modelling language via a case study of three problem classes.
Cite as
Alessio Pellegrino, Özgür Akgün, Nguyen Dang, Zeynep Kiziltan, and Ian Miguel. Transformer-Based Feature Learning for Algorithm Selection in Combinatorial Optimisation. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 31:1-31:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{pellegrino_et_al:LIPIcs.CP.2025.31,
author = {Pellegrino, Alessio and Akg\"{u}n, \"{O}zg\"{u}r and Dang, Nguyen and Kiziltan, Zeynep and Miguel, Ian},
title = {{Transformer-Based Feature Learning for Algorithm Selection in Combinatorial Optimisation}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {31:1--31:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.31},
URN = {urn:nbn:de:0030-drops-238928},
doi = {10.4230/LIPIcs.CP.2025.31},
annote = {Keywords: Constraint modelling, algorithm selection, feature extraction, machine learning, transformer architecture}
}
Document
BFS-Based Canonical Codes for Generating Graphs with Constraint Programming
Abstract
We consider the problem of generating all graphs that satisfy some given additional constraints (on vertex degrees, or cycle lengths, for example). Most previous works have proposed to generate canonical codes associated with adjacency matrices. In this paper, we consider canonical codes based on Breadth First Search (BFS), and we show how to generate them with Constraint Programming (CP): we introduce a set of basic constraints that must be satisfied by all canonical codes, thus breaking many symmetries, and we introduce a global constraint to break other symmetries. We illustrate the interest of our approach on connected claw-free cubic graphs, and show that it outperforms state-of-the-art CP and SAT Modulo Theory (SMT) approaches.
Cite as
Xiao Peng and Christine Solnon. BFS-Based Canonical Codes for Generating Graphs with Constraint Programming. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{peng_et_al:LIPIcs.CP.2025.32,
author = {Peng, Xiao and Solnon, Christine},
title = {{BFS-Based Canonical Codes for Generating Graphs with Constraint Programming}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {32:1--32:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.32},
URN = {urn:nbn:de:0030-drops-238935},
doi = {10.4230/LIPIcs.CP.2025.32},
annote = {Keywords: Graph Generation, Automorphisms, Symmetry Breaking}
}
Document
Constraint-Based In-Station Train Dispatching
Abstract
In-station dispatching is the problem of planning the movements of scheduled trains inside a railway station. Effective solutions for in-station dispatching are important for maximising the utilisation of railway infrastructure and for mitigating the impact of incidents and delays in the broader network.
In this paper, we explore a constraint-based approach to perform in-station train dispatching. Our extensive empirical analysis of multiple modelling, search strategy, and solver choices, performed over synthetically generated, yet realistic, data, shows that our method outperforms the existing planning-based state-of-the-art approach. In addition, we present different optimisation criteria, which can be effortless defined thanks to the constraint-based approach.
Cite as
Andreas Schutt, Matteo Cardellini, Jip J. Dekker, Daniel Harabor, Marco Maratea, and Mauro Vallati. Constraint-Based In-Station Train Dispatching. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 33:1-33:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{schutt_et_al:LIPIcs.CP.2025.33,
author = {Schutt, Andreas and Cardellini, Matteo and Dekker, Jip J. and Harabor, Daniel and Maratea, Marco and Vallati, Mauro},
title = {{Constraint-Based In-Station Train Dispatching}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {33:1--33:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.33},
URN = {urn:nbn:de:0030-drops-238941},
doi = {10.4230/LIPIcs.CP.2025.33},
annote = {Keywords: in-station train dispatching, train scheduling, railway scheduling, constraint programming, mixed-integer programming}
}
Document
DynamicSAT: Dynamic Configuration Tuning for SAT Solving
Abstract
Boolean Satisfiability (SAT) problem serves as a foundation for solving numerous real-world challenges. As problem complexity increases, so does the demand for sophisticated SAT solvers, which incorporate a variety of heuristics tailored to optimize performance for specific problem instances. However, a major limitation persists: a configuration that performs well on one instance may lead to inefficiencies on others. While previous approaches to automatic algorithm configuration set parameters prior to runtime, they fail to adapt to the dynamic evolution of problem characteristics during the solving process. We introduce DynamicSAT, a novel SAT solver framework that dynamically tunes configuration parameters during solving process. By adjusting parameters on-the-fly, DynamicSAT adapts to changes arising from clause learning, elimination, and other transformations, thus improving efficiency and robustness across diverse SAT instances. We demonstrate that DynamicSAT achieves significant performance gains over the state-of-the-art solver on 2024 SAT Competition Benchmark.
Cite as
Zhengyuan Shi, Wentao Jiang, Xindi Zhang, Jin Luo, Yun Liang, Zhufei Chu, and Qiang Xu. DynamicSAT: Dynamic Configuration Tuning for SAT Solving. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 34:1-34:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{shi_et_al:LIPIcs.CP.2025.34,
author = {Shi, Zhengyuan and Jiang, Wentao and Zhang, Xindi and Luo, Jin and Liang, Yun and Chu, Zhufei and Xu, Qiang},
title = {{DynamicSAT: Dynamic Configuration Tuning for SAT Solving}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {34:1--34:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.34},
URN = {urn:nbn:de:0030-drops-238952},
doi = {10.4230/LIPIcs.CP.2025.34},
annote = {Keywords: Boolean satisfiability problem, configuration tuning, multi-armed bandit}
}
Document
Unite and Lead: Finding Disjunctive Cliques for Scheduling Problems
Abstract
Constraint programming solvers have seen much success in scheduling problems owing to their efficient reasoning over constraints to solve complex problems in practice. Many algorithms have been proposed for propagating information from a single constraint. However, inferring and exchanging information across multiple constraints can provide deeper insight into the global structure of a problem. In this work, we propose to exchange information amongst constraints by inferring the disjointness of tasks in scheduling problems from many constraints. We do this by (i) augmenting existing propagators, such as the Cumulative and nogoods, to report when pairs of tasks are disjoint, and (ii) leveraging this information by introducing the SelectiveDisjunctive propagator which generates a lower bound on the earliest completion time of cliques of disjoint tasks to determine conflicts. This allows us to aggregate disjointness information spanning multiple constraints to gain a better global overview of the problem, as well as more precise local information. We also identify a problem structure where an LCG solver reasoning over Cumulative constraints separately, without any reformulations, requires an exponential amount of time to prove infeasibility, which we both justify theoretically and show empirically; on the other hand, our approach solves those instances in polynomial time. On particular known RCPSP and RCPSP/max benchmarks, our approach significantly reduces the number of conflicts required to prove optimality when resource contention is high. Additionally, we discover new lower bounds for 16 RCPSP/max instances (closing six of them) and four RCPSP instances (closing one), as well as new upper bounds for two RCPSP/max instances and four RCPSP instances. Furthermore, we empirically analyse our proposed approach to determine which features are beneficial for performance, showing that finding cliques is one of the main bottlenecks and that detecting disjointness during search can lead to improved bounds on certain instances, but it generally negatively impacts learning. This work paves the way for reasoning over the disjointness of tasks inferred from a variety of standard constraints to discover novel information sourced from multiple constraints during search.
Cite as
Konstantin Sidorov, Imko Marijnissen, and Emir Demirović. Unite and Lead: Finding Disjunctive Cliques for Scheduling Problems. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 35:1-35:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{sidorov_et_al:LIPIcs.CP.2025.35,
author = {Sidorov, Konstantin and Marijnissen, Imko and Demirovi\'{c}, Emir},
title = {{Unite and Lead: Finding Disjunctive Cliques for Scheduling Problems}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {35:1--35:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.35},
URN = {urn:nbn:de:0030-drops-238969},
doi = {10.4230/LIPIcs.CP.2025.35},
annote = {Keywords: Constraint Programming, Lazy Clause Generation, Propagation, Scheduling, Cumulative, Disjunctive}
}
Document
Balancing Latin Rectangles with LLM-Generated Streamliners
Abstract
We present an integration of Large Language Models (LLMs) with streamlining techniques to find well-balanced Latin rectangles. Our approach combines LLM-generated streamlining constraints that effectively partition the search space, directing constraint solvers toward structured subspaces containing high-quality solutions. Our methodology extends LLM-generated streamliners, as Voboril et al. (2024) introduced for decision problems, to the optimization context through techniques that incrementally refine the objective function value.
We propose two complementary strategies to orchestrate sets of streamliners: an incremental mechanism that utilizes improving solutions to initialize subsequent search processes, and an evolutionary framework that maintains and refines effective streamliner populations. Our experiments demonstrate that our approach successfully reduces established minimum imbalance values for partially spatially balanced Latin rectangles across multiple problem dimensions. The results validate the efficacy of combining LLMs with constraint programming methodologies for tackling problems characterized by complex global constraints.
Cite as
Florentina Voboril, Vaidyanathan Peruvemba Ramaswamy, and Stefan Szeider. Balancing Latin Rectangles with LLM-Generated Streamliners. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{voboril_et_al:LIPIcs.CP.2025.36,
author = {Voboril, Florentina and Peruvemba Ramaswamy, Vaidyanathan and Szeider, Stefan},
title = {{Balancing Latin Rectangles with LLM-Generated Streamliners}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {36:1--36:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.36},
URN = {urn:nbn:de:0030-drops-238970},
doi = {10.4230/LIPIcs.CP.2025.36},
annote = {Keywords: Balanced Latin Rectangles, Streamliners, Large Language Models, Warmstarts, Evolutionary Search}
}
Document
Multi-League Sports Scheduling with Team Interdependencies: An Optimization Model
Abstract
Every year, a large number of matches must be scheduled for professional and amateur sports teams. Several constraints have to be considered, including the overall capacity of venues and interdependencies between teams of the same club. As interdependent teams of a club play in different leagues, finding an optimal solution is very challenging for practitioners. While the problem of respecting capacity restrictions is well-addressed in prior work, interdependencies between teams are widely neglected, despite being a problem of major importance in practice. This paper enhances the formal definition of the multi-league-sports scheduling problem to take team interdependencies into account. We create an optimization problem to be solved by means of integer linear programming, and prove the corresponding decision problem to be NP-complete by a polynomial reduction from 3-SAT. An implementation which was used to schedule German table tennis leagues of a certain district demonstrates the practical applicability of the approach.
Cite as
Nils Weidmann. Multi-League Sports Scheduling with Team Interdependencies: An Optimization Model. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{weidmann:LIPIcs.CP.2025.37,
author = {Weidmann, Nils},
title = {{Multi-League Sports Scheduling with Team Interdependencies: An Optimization Model}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {37:1--37:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.37},
URN = {urn:nbn:de:0030-drops-238986},
doi = {10.4230/LIPIcs.CP.2025.37},
annote = {Keywords: sports scheduling, linear optimization, constraint programming}
}
Document
Reducing Quantum Circuit Synthesis to #SAT
Abstract
Quantum circuit synthesis is the task of decomposing a given quantum operator into a sequence of elementary quantum gates. Since the finite target gate set cannot exactly implement any given operator, approximation is often necessary. Model counting, or #SAT, has recently been demonstrated as a promising new approach for tackling core problems in quantum circuit analysis. In this work, we show for the first time that the universal quantum circuit synthesis problem can be reduced to maximum model counting. We formulate a #SAT encoding for exact and approximate depth-optimal quantum circuit synthesis into the Clifford+T gate set. We evaluate our method with an open-source implementation that uses the maximum model counter d4Max as a backend. For this purpose, we extended d4Max with support for complex and negative weights to represent amplitudes. Experimental results show that existing classical tools have potential for the quantum circuit synthesis problem.
Cite as
Dekel Zak, Jingyi Mei, Jean-Marie Lagniez, and Alfons Laarman. Reducing Quantum Circuit Synthesis to #SAT. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{zak_et_al:LIPIcs.CP.2025.38,
author = {Zak, Dekel and Mei, Jingyi and Lagniez, Jean-Marie and Laarman, Alfons},
title = {{Reducing Quantum Circuit Synthesis to #SAT}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {38:1--38:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.38},
URN = {urn:nbn:de:0030-drops-238997},
doi = {10.4230/LIPIcs.CP.2025.38},
annote = {Keywords: Maximum weighted model counting, quantum circuit synthesis}
}
Document
The 3-Decomposition Conjecture: A SAT-Based Approach with Specialized Propagators
Abstract
We investigate the 3-decomposition conjecture, which states that every connected cubic graph can be decomposed into a spanning tree, a collection of cycles, and a matching. Using a SAT-based approach enhanced with specialized propagators, we verify the conjecture for all relevant graphs up to 28 vertices. Our method extends the Satisfiability Modulo Symmetries (SMS) framework with specialized propagators that exploit theoretical properties of minimal counterexamples (counterexamples with the minimal number of vertices), enabling efficient pruning. We demonstrate that graphs containing certain substructures cannot be minimal counterexamples to the conjecture, allowing us to exclude these patterns during the search dynamically. Our experimental results quantify the impact of different propagator configurations and forbidden subgraph constraints on solving efficiency, showing significant performance improvements when leveraging these techniques. The approach scales effectively to graphs of 28 vertices. Our work illustrates how combining SAT solving with specialized constraint propagation techniques can successfully address challenging combinatorial problems in contemporary graph theory.
Cite as
Tianwei Zhang and Stefan Szeider. The 3-Decomposition Conjecture: A SAT-Based Approach with Specialized Propagators. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 39:1-39:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{zhang_et_al:LIPIcs.CP.2025.39,
author = {Zhang, Tianwei and Szeider, Stefan},
title = {{The 3-Decomposition Conjecture: A SAT-Based Approach with Specialized Propagators}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {39:1--39:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.39},
URN = {urn:nbn:de:0030-drops-239005},
doi = {10.4230/LIPIcs.CP.2025.39},
annote = {Keywords: SAT, Symmetry Breaking, Subgraphs, Propagators, Combinatorics}
}
Document
An Efficient and Uniform CSP Solution Generator Generator
Abstract
Constraint-based random testing is a powerful technique which aims at generating random test cases to verify functional properties of a program. Its objective is to determine whether a function satisfies a given property for every possible input. This approach requires firstly defining the property to satisfy, then secondly to provide a "generator of inputs" able to feed the program with the inputs generated. Besides, function inputs often need to satisfy certain constraints to ensure the function operates correctly, which makes the crafting of such a generator a hard task. In this paper, we are interested in the problem of manufacturing a uniform and efficient generator for the solutions of a CSP. In order to do that, we propose a specialized solving method that produces a well-suited representation for random sampling. Our solving method employs a dedicated propagation scheme based on the hypergraph representation of a CSP, and a custom split heuristic called birdge-first that emphasizes the interests of our propagation scheme. The generators we build are general enough to handle a wide range of use-cases. They are moreover uniform by construction, iterative and self-improving. We present a prototype built upon the AbSolute constraint solving library and demonstrate its performances on several realistic examples.
Cite as
Ghiles Ziat and Martin Pépin. An Efficient and Uniform CSP Solution Generator Generator. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 40:1-40:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{ziat_et_al:LIPIcs.CP.2025.40,
author = {Ziat, Ghiles and P\'{e}pin, Martin},
title = {{An Efficient and Uniform CSP Solution Generator Generator}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {40:1--40:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.40},
URN = {urn:nbn:de:0030-drops-239010},
doi = {10.4230/LIPIcs.CP.2025.40},
annote = {Keywords: Constraint Programming, Property-based Testing}
}
Document
Short Paper
Modeling and Solving a Composite Structure Design Problem with Constraint Programming (Short Paper)
Abstract
Composite structures are composed of plies (layers) of carbon fibers. For each ply, one must decide its orientation from the set of possible angles: -45°, 0°, 45°, and 90°. The stack of plies must follow strict constraints on the chosen orientations to achieve mechanical properties of the composite, such as sufficient buckling load. The design problem becomes more complex when determining the stack of plies for a complete surface material, that does not require the same number of plies in every region of the surface. Not only must the orientations be selected in each region, but it is also necessary to decide which plies are discontinued between adjacent regions. Thanks to its declarative nature, Constraint Programming (CP) offers an elegant modeling of the constraints, making it easy for designers to activate or deactivate them as needed. We propose a CP model, implemented in MiniZinc. The performance of this model on synthetic yet realistic instances when solved by different exact solvers, including Mixed Integer Programming (MIP) solvers, demonstrates the superiority of CP over MIP on our MiniZinc model, and over a commercial solution implemented by an industrial partner. It opens up the adoption of CP as an efficient building block of Computer-Aided Design tools for composite structures. By making the model and instances publicly available, we also hope to facilitate the inclusion of this problem in CP solver competitions and stimulate further research in this area.
Cite as
Miguel Antoons, Augustin Delecluse, Samih Zein, and Pierre Schaus. Modeling and Solving a Composite Structure Design Problem with Constraint Programming (Short Paper). In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 41:1-41:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{antoons_et_al:LIPIcs.CP.2025.41,
author = {Antoons, Miguel and Delecluse, Augustin and Zein, Samih and Schaus, Pierre},
title = {{Modeling and Solving a Composite Structure Design Problem with Constraint Programming}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {41:1--41:9},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.41},
URN = {urn:nbn:de:0030-drops-239022},
doi = {10.4230/LIPIcs.CP.2025.41},
annote = {Keywords: Constraint Programming, Composite Structures, Design Rules, MiniZinc}
}
Document
Short Paper
Towards Modern and Modular SAT for LCG (Short Paper)
Abstract
Lazy Clause Generation (LCG) is an architecture for building Constraint Programming (CP) solvers using an underlying Boolean Satisfiability (SAT) engine. The CP propagation engine lazily creates clauses that define the integer variables and impose problem restrictions. The SAT engine uses the clausal model to reason and search, including, crucially, the generation of nogoods. However, while SAT solving has made significant advances recently, the underlying SAT technology in most LCG solvers has largely remained the same. Using a new interface to SAT engines, IPASIR-UP, we can construct an LCG solver which can swap out the underlying SAT engine with any that supports the interface. This new approach means we need to revisit many of the design and engineering decisions for LCG solvers, to take maximum advantage of a better underlying SAT engine while adhering to the restrictions of the interface. In this paper, we explore the possibilities and challenges of using IPASIR-UP for LCG, showing that it can be used to create a highly competitive solver.
Cite as
Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong. Towards Modern and Modular SAT for LCG (Short Paper). In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 42:1-42:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{dekker_et_al:LIPIcs.CP.2025.42,
author = {Dekker, Jip J. and Ignatiev, Alexey and Stuckey, Peter J. and Zhong, Allen Z.},
title = {{Towards Modern and Modular SAT for LCG}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {42:1--42:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.42},
URN = {urn:nbn:de:0030-drops-239038},
doi = {10.4230/LIPIcs.CP.2025.42},
annote = {Keywords: Lazy Clause Generation, Boolean Satisfiability, IPASIR-UP}
}
Document
Short Paper
Scheduling Telescope Observations for the European Southern Observatory (Short Paper)
Abstract
The European Southern Observatory (ESO) provides state-of-the-art large telescope facilities at three sites in Chile, supported by 16 European member states. Astronomers submit proposals for sets of observations which are reviewed and ranked based on scientific merit, then a schedule is constructed respecting the ranking and aiming to make the fullest use of the various telescopes and numerous instruments. Currently a schedule covers six months, but in the near future ESO will switch to annual schedules.
Here we examine the most challenging scheduling problem encountered by ESO: scheduling the operations of the Very Large Telescope Interferometer (VLTI) on Paranal, Chile. Tasks to be scheduled include observations performed by ESO staff, "visitor mode" periods where astronomers visit the site to use the telescopes, various maintenance tasks, and reconfiguration tasks taking multiple days. Typically a VLTI six-month schedule would contain approximately 450 activities. We explore global constraint models and a SAT encoding of the problem.
Cite as
Michael Prümm, Peter Nightingale, and Felix Ulrich-Oltean. Scheduling Telescope Observations for the European Southern Observatory (Short Paper). In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 43:1-43:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{prumm_et_al:LIPIcs.CP.2025.43,
author = {Pr\"{u}mm, Michael and Nightingale, Peter and Ulrich-Oltean, Felix},
title = {{Scheduling Telescope Observations for the European Southern Observatory}},
booktitle = {31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
pages = {43:1--43:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-380-5},
ISSN = {1868-8969},
year = {2025},
volume = {340},
editor = {de la Banda, Maria Garcia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.43},
URN = {urn:nbn:de:0030-drops-239041},
doi = {10.4230/LIPIcs.CP.2025.43},
annote = {Keywords: Modelling, Constraint Programming, Scheduling, SAT, Global Constraints}
}