Search Results

Documents authored by Dekker, Jip J.

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
DOI: 10.4230/LIPIcs.CP.2025.10
Unit Types for MiniZinc

Authors: Jip J. Dekker, Jason Nguyen, Peter J. Stuckey, and Guido Tack

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

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
DOI: 10.4230/LIPIcs.CP.2025.33
Constraint-Based In-Station Train Dispatching

Authors: Andreas Schutt, Matteo Cardellini, Jip J. Dekker, Daniel Harabor, Marco Maratea, and Mauro Vallati

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

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
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}
}
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact