52 Search Results for "Stuckey, Peter"

Artifact
Software
DOI: 10.4230/artifacts.26917
Table Constraints for Integer Programming

Authors: Hendrik Bierlee, Wout Piessens, Tias Guns, and Peter J. Stuckey

Abstract
Cite as

Hendrik Bierlee, Wout Piessens, Tias Guns, Peter J. Stuckey. Table Constraints for Integer Programming (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26917,
   title = {{Table Constraints for Integer Programming}}, 
   author = {Bierlee, Hendrik and Piessens, Wout and Guns, Tias and Stuckey, Peter J.},
   note = {Software, https://wms.cs.kuleuven.be/chat-opt, https://www.fwo.be/, https://optima.org.au/, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:1b22a434c54cd6bb28794cf6c9771f6a002e07f0;origin=https://github.com/ML-KULeuven/table-constraints-for-integer-programming;visit=swh:1:snp:993c9810181126cd29c2384d17d88d3c58cbdc58;anchor=swh:1:rev:3a9a6ff8e84d1d4ea474c2da6cf466a6be923128}{\texttt{swh:1:dir:1b22a434c54cd6bb28794cf6c9771f6a002e07f0}} (visited on 2026-07-13)},
   url = {https://github.com/ML-KULeuven/table-constraints-for-integer-programming},
   doi = {10.4230/artifacts.26917},
}
Document
DOI: 10.4230/LIPIcs.CP.2026.6
Table Constraints for Integer Programming

Authors: Hendrik Bierlee, Wout Piessens, Tias Guns, and Peter J. Stuckey

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

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

Hendrik Bierlee, Wout Piessens, Tias Guns, and Peter J. Stuckey. Table Constraints for Integer Programming. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bierlee_et_al:LIPIcs.CP.2026.6,
  author =	{Bierlee, Hendrik and Piessens, Wout and Guns, Tias and Stuckey, Peter J.},
  title =	{{Table Constraints for Integer Programming}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.6},
  URN =		{urn:nbn:de:0030-drops-266397},
  doi =		{10.4230/LIPIcs.CP.2026.6},
  annote =	{Keywords: Table constraints, integer programming, cut generation, modelling}
}
Document
DOI: 10.4230/LIPIcs.CP.2026.35
Automatic Relaxation and Multi-Armed Bandit Learning for Large Neighbourhood Search

Authors: Frej Knutar Lewander, Pierre Flener, Justin Pearson, and Peter J. Stuckey

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

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

Frej Knutar Lewander, Pierre Flener, Justin Pearson, and Peter J. Stuckey. Automatic Relaxation and Multi-Armed Bandit Learning for Large Neighbourhood Search. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{knutarlewander_et_al:LIPIcs.CP.2026.35,
  author =	{Knutar Lewander, Frej and Flener, Pierre and Pearson, Justin and Stuckey, Peter J.},
  title =	{{Automatic Relaxation and Multi-Armed Bandit Learning for Large Neighbourhood Search}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{35:1--35:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.35},
  URN =		{urn:nbn:de:0030-drops-266675},
  doi =		{10.4230/LIPIcs.CP.2026.35},
  annote =	{Keywords: Combinatorial Optimisation, Large Neighbourhood Search (LNS), Constraint-Based Local Search (CBLS)}
}
Document
DOI: 10.4230/LIPIcs.CP.2026.42
From Literals to Atomic Constraints: Generalising Conflict-Driven Clause Learning for Constraint Programming

Authors: Imko Marijnissen, Maarten Flippo, and Emir Demirović

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

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

Imko Marijnissen, Maarten Flippo, and Emir Demirović. From Literals to Atomic Constraints: Generalising Conflict-Driven Clause Learning for Constraint Programming. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 42:1-42:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{marijnissen_et_al:LIPIcs.CP.2026.42,
  author =	{Marijnissen, Imko and Flippo, Maarten and Demirovi\'{c}, Emir},
  title =	{{From Literals to Atomic Constraints: Generalising Conflict-Driven Clause Learning for Constraint Programming}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{42:1--42:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.42},
  URN =		{urn:nbn:de:0030-drops-266744},
  doi =		{10.4230/LIPIcs.CP.2026.42},
  annote =	{Keywords: LCG, CP, CDCL, Lazy Literal, Conflict Analysis, Nogood Propagation}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.CP.2026.62
Towards Step-Wise Explanations of Large Search Trees (Short Paper)

Authors: Ignace Bleukx, Peter J. Stuckey, and Tias Guns

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

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

Ignace Bleukx, Peter J. Stuckey, and Tias Guns. Towards Step-Wise Explanations of Large Search Trees (Short Paper). In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 62:1-62:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bleukx_et_al:LIPIcs.CP.2026.62,
  author =	{Bleukx, Ignace and Stuckey, Peter J. and Guns, Tias},
  title =	{{Towards Step-Wise Explanations of Large Search Trees}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{62:1--62:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.62},
  URN =		{urn:nbn:de:0030-drops-266958},
  doi =		{10.4230/LIPIcs.CP.2026.62},
  annote =	{Keywords: Explanation, search, propagation, proof}
}
Document
DOI: 10.4230/LIPIcs.CPM.2026.12
Maximizing Diversity in (Near-)Median String Selection

Authors: Diptarka Chakraborty, Rudrayan Kundu, Nidhi Purohit, and Aravinda Kanchana Ruwanpathirana

Published in: LIPIcs, Volume 369, 37th Annual Symposium on Combinatorial Pattern Matching (CPM 2026)

Abstract
Given a set of strings over a specified alphabet, identifying a median or consensus string that minimizes the total distance to all input strings is a fundamental data aggregation problem. When the Hamming distance is considered as the underlying metric, this problem has extensive applications, ranging from bioinformatics to pattern recognition. However, modern applications often require the generation of multiple (near-)optimal yet diverse median strings to enhance flexibility and robustness in decision-making. In this study, we address this need by focusing on two prominent diversity measures: sum dispersion and min dispersion. We first introduce an exact algorithm for the diameter variant of the problem, which identifies pairs of near-optimal medians that are maximally diverse. Subsequently, we propose a (1-ε)-approximation algorithm (for any ε > 0) for sum dispersion, as well as a bi-criteria approximation algorithm for the more challenging min dispersion case, allowing the generation of multiple (more than two) diverse near-optimal Hamming medians. Our approach primarily leverages structural insights into the Hamming median space and also draws on techniques from error-correcting code construction to establish these results.
Cite as

Diptarka Chakraborty, Rudrayan Kundu, Nidhi Purohit, and Aravinda Kanchana Ruwanpathirana. Maximizing Diversity in (Near-)Median String Selection. In 37th Annual Symposium on Combinatorial Pattern Matching (CPM 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 369, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{chakraborty_et_al:LIPIcs.CPM.2026.12,
  author =	{Chakraborty, Diptarka and Kundu, Rudrayan and Purohit, Nidhi and Ruwanpathirana, Aravinda Kanchana},
  title =	{{Maximizing Diversity in (Near-)Median String Selection}},
  booktitle =	{37th Annual Symposium on Combinatorial Pattern Matching (CPM 2026)},
  pages =	{12:1--12:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-420-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{369},
  editor =	{Bille, Philip and Prezza, Nicola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CPM.2026.12},
  URN =		{urn:nbn:de:0030-drops-259382},
  doi =		{10.4230/LIPIcs.CPM.2026.12},
  annote =	{Keywords: Diversity maximization, Hamming median, diameter, dispersion, approximation algorithms}
}
Document
DOI: 10.4230/DagRep.15.9.1
Interactions in Constraint Optimization (Dagstuhl Seminar 25371)

Authors: Katalin Fazekas, Matti Järvisalo, Nina Narodytska, Peter J. Stuckey, and Christoph Jabs

Published in: Dagstuhl Reports, Volume 15, Issue 9 (2026)

Abstract
This report documents the Dagstuhl Seminar 25371 "Interactions in Constraint Optimization". Our Dagstuhl Seminar gathered 41 researchers from 15 countries, working on different constraint optimization paradigms. The report consists of an executive summary, and abstracts on tutorials, research talks, and panel discussions.
Cite as

Katalin Fazekas, Matti Järvisalo, Nina Narodytska, Peter J. Stuckey, and Christoph Jabs. Interactions in Constraint Optimization (Dagstuhl Seminar 25371). In Dagstuhl Reports, Volume 15, Issue 9, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{fazekas_et_al:DagRep.15.9.1,
  author =	{Fazekas, Katalin and J\"{a}rvisalo, Matti and Narodytska, Nina and Stuckey, Peter J. and Jabs, Christoph},
  title =	{{Interactions in Constraint Optimization (Dagstuhl Seminar 25371)}},
  pages =	{1--20},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2026},
  volume =	{15},
  number =	{9},
  editor =	{Fazekas, Katalin and J\"{a}rvisalo, Matti and Narodytska, Nina and Stuckey, Peter J. and Jabs, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.9.1},
  URN =		{urn:nbn:de:0030-drops-249811},
  doi =		{10.4230/DagRep.15.9.1},
  annote =	{Keywords: constraint programming, maximum satisfiability, mixed integer linear programming, optimization modulo theories, pseudo-boolean optimization}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.26
Optimal Concolic Dynamic Partial Order Reduction

Authors: Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Stateless model checking (SMC) software implementations requires exploring both concurrency- and data nondeterminism. Unfortunately, most SMC algorithms focus on efficient exploration of concurrency nondeterminism, thereby neglecting an important source of bugs. We present ConDpor, an SMC algorithm for unmodified Java programs that combines optimal dynamic partial order reduction (DPOR) for concurrency nondeterminism, with concolic execution for data nondeterminism. ConDpor is sound, complete, optimal, and parametric w.r.t. the memory consistency model. Our experiments confirm that ConDpor is exponentially faster than DPOR with small-domain enumeration. Overall, ConDpor opens the door for efficient exploration of concurrent programs with data nondeterminism.
Cite as

Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra. Optimal Concolic Dynamic Partial Order Reduction. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{khoshechinjorshari_et_al:LIPIcs.CONCUR.2025.26,
  author =	{Khoshechin Jorshari, Mohammad Hossein and Kokologiannakis, Michalis and Majumdar, Rupak and Nagendra, Srinidhi},
  title =	{{Optimal Concolic Dynamic Partial Order Reduction}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{26:1--26:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.26},
  URN =		{urn:nbn:de:0030-drops-239765},
  doi =		{10.4230/LIPIcs.CONCUR.2025.26},
  annote =	{Keywords: Stateless model checking, dynamic symbolic execution}
}
Document
DOI: 10.4230/LIPIcs.WABI.2025.11
Mutational Signature Refitting on Sparse Pan-Cancer Data

Authors: Gal Gilad, Teresa M. Przytycka, and Roded Sharan

Published in: LIPIcs, Volume 344, 25th International Conference on Algorithms for Bioinformatics (WABI 2025)

Abstract
Mutational processes shape cancer genomes, leaving characteristic marks that are termed signatures. The level of activity of each such process, or its signature exposure, provides important information on the disease, improving patient stratification and the prediction of drug response. Thus, there is growing interest in developing refitting methods that decipher those exposures. Previous work in this domain was unsupervised in nature, employing algebraic decomposition and probabilistic inference methods. Here we provide a supervised approach to the problem of signature refitting and show its superiority over current methods. Our method, SuRe, leverages a neural network model to capture correlations between signature exposures in real data. We show that SuRe outperforms previous methods on sparse mutation data from tumor type specific data sets, as well as pan-cancer data sets, with an increasing advantage as the data become sparser. We further demonstrate its utility in clinical settings.
Cite as

Gal Gilad, Teresa M. Przytycka, and Roded Sharan. Mutational Signature Refitting on Sparse Pan-Cancer Data. In 25th International Conference on Algorithms for Bioinformatics (WABI 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 344, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gilad_et_al:LIPIcs.WABI.2025.11,
  author =	{Gilad, Gal and Przytycka, Teresa M. and Sharan, Roded},
  title =	{{Mutational Signature Refitting on Sparse Pan-Cancer Data}},
  booktitle =	{25th International Conference on Algorithms for Bioinformatics (WABI 2025)},
  pages =	{11:1--11:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-386-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{344},
  editor =	{Brejov\'{a}, Bro\v{n}a and Patro, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WABI.2025.11},
  URN =		{urn:nbn:de:0030-drops-239374},
  doi =		{10.4230/LIPIcs.WABI.2025.11},
  annote =	{Keywords: mutational signatures, signature refitting, cancer genomics, genomic data analysis, somatic mutations}
}
Artifact
Software
DOI: 10.4230/artifacts.24103
Huub: Lazy Clause Generation Solver

Authors: Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong

Abstract
Cite as

Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, Allen Z. Zhong. Huub: Lazy Clause Generation Solver (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{huub2025zenodo,
   title = {{Huub: Lazy Clause Generation Solver}}, 
   author = {Dekker, Jip J. and Ignatiev, Alexey and Stuckey, Peter J. and Zhong, Allen Z.},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:b28854946ae60e86a37051ea89465cce8b84b7ed}{\texttt{swh:1:dir:b28854946ae60e86a37051ea89465cce8b84b7ed}} (visited on 2025-08-08)},
   url = {https://github.com/huub-solver/huub},
   doi = {10.4230/artifacts.24103},
}
Document
Short Paper
DOI: 10.4230/LIPIcs.CP.2025.42
Towards Modern and Modular SAT for LCG (Short Paper)

Authors: Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

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
DOI: 10.4230/LIPIcs.CP.2025.39
The 3-Decomposition Conjecture: A SAT-Based Approach with Specialized Propagators

Authors: Tianwei Zhang and Stefan Szeider

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

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
Short Paper
DOI: 10.4230/LIPIcs.CP.2025.41
Modeling and Solving a Composite Structure Design Problem with Constraint Programming (Short Paper)

Authors: Miguel Antoons, Augustin Delecluse, Samih Zein, and Pierre Schaus

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

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
DOI: 10.4230/LIPIcs.CP.2025.20
Dependency-Curated Large Neighbourhood Search

Authors: Frej Knutar Lewander, Pierre Flener, and Justin Pearson

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

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
DOI: 10.4230/LIPIcs.CP.2025.24
The Work Task Variation Problem

Authors: Mikael Z. Lagerkvist and Magnus Rattfeldt

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

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}
}
  • Refine by Type
  • 50 Document/PDF
  • 32 Document/HTML
  • 2 Artifact

  • Refine by Publication Year
  • 7 2026
  • 31 2025
  • 1 2024
  • 3 2023
  • 2 2022
  • Show More...

  • Refine by Author
  • 16 Stuckey, Peter J.
  • 4 Dekker, Jip J.
  • 4 Guns, Tias
  • 4 Ignatiev, Alexey
  • 3 Berg, Jeremias
  • Show More...

  • Refine by Series/Journal
  • 43 LIPIcs
  • 5 OASIcs
  • 1 DagRep
  • 1 DagSemProc

  • Refine by Classification
  • 17 Theory of computation → Constraint and logic programming
  • 6 Mathematics of computing → Combinatorial optimization
  • 5 Computing methodologies → Planning and scheduling
  • 4 Applied computing → Operations research
  • 4 Software and its engineering → Constraint and logic languages
  • Show More...

  • Refine by Keyword
  • 7 Constraint Programming
  • 5 Scheduling
  • 5 constraint programming
  • 3 SAT
  • 2 Combinatorial Optimisation
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact