Publications

2026

1. Domain-Independent Dynamic Programming with Constraint Propagation

   Imko Marijnissen, J. Christopher Beck, Emir Demirović, and Ryo Kuroiwa

   Proceedings of the International Conference on Automated Planning and Scheduling, Jun 2026

   Abs DOI Bib

   There are two prevalent model-based paradigms for combinatorial problems: 1) state-based representations, such as heuristic search, dynamic programming (DP), and decision diagrams, and 2) constraint and domain-based representations, such as constraint programming (CP), (mixed-)integer programming, and Boolean satisfiability. In this paper, we bridge the gap between the DP and CP paradigms by integrating constraint propagation into DP, enabling a DP solver to prune states and transitions using constraint propagation. To this end, we implement constraint propagation using a general-purpose CP solver in the Domain-Independent Dynamic Programming framework and evaluate using heuristic search on three combinatorial optimisation problems: Single Machine Scheduling with Time Windows, the Resource Constrained Project Scheduling Problem (RCPSP), and the Travelling Salesperson Problem with Time Windows (TSPTW). Our evaluation shows that constraint propagation significantly reduces the number of state expansions, causing our approach to solve more instances than a DP solver for Single Machine Scheduling and RCPSP, and showing similar improvements for tightly constrained TSPTW instances. The runtime performance indicates that the benefits of propagation outweigh the overhead for constrained instances, but that further work into reducing propagation overhead could improve performance further. Our work is a key step in understanding the value of constraint propagation in DP solvers, providing a model-based approach to integrating DP and CP.

   @article{Marijnissen_Beck_Demirović_Kuroiwa_2026,
     title = {Domain-Independent Dynamic Programming with Constraint Propagation},
     volume = {36},
     url = {http://dx.doi.org/10.1609/icaps.v36i1.42826},
     doi = {10.1609/icaps.v36i1.42826},
     number = {1},
     journal = {Proceedings of the International Conference on Automated Planning and Scheduling},
     publisher = {Association for the Advancement of Artificial Intelligence (AAAI)},
     author = {Marijnissen, Imko and Beck, J. Christopher and Demirović, Emir and Kuroiwa, Ryo},
     year = {2026},
     month = jun,
     pages = {171–180},
   }

2025

1. Unite and Lead: Finding Disjunctive Cliques for Scheduling Problems

   Konstantin Sidorov, Imko Marijnissen, and Emir Demirović

   In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025), Jun 2025

   Abs DOI Bib

   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.

   @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},
   }

2024

1. A Multi-Stage Proof Logging Framework to Certify the Correctness of CP Solvers

   Maarten Flippo, Konstantin Sidorov, Imko Marijnissen, Jeff Smits, and Emir Demirović

   In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024), Jun 2024

   Abs DOI Bib

   Proof logging is used to increase trust in the optimality and unsatisfiability claims of solvers. However, to this date, no constraint programming solver can practically produce proofs without significantly impacting performance, which hinders mainstream adoption. We address this issue by introducing a novel proof generation framework, together with a CP proof format and proof checker. Our approach is to divide the proof generation into three steps. At runtime, we require the CP solver to only produce a proof sketch, which we call a scaffold. After the solving is done, our proof processor trims and expands the scaffold into a full CP proof, which is subsequently verified. Our framework is agnostic to the solver and the verification approach. Through MiniZinc benchmarks, we demonstrate that with our framework, the overhead of logging during solving is often less than 10%, significantly lower than other approaches, and that our proof processing step can reduce the overall size of the proof by orders of magnitude and by extension the proof checking time. Our results demonstrate that proof logging has the potential to become an integral part of the CP community.

   @inproceedings{flippo_et_al:LIPIcs.CP.2024.11,
     author = {Flippo, Maarten and Sidorov, Konstantin and Marijnissen, Imko and Smits, Jeff and Demirovi\'{c}, Emir},
     title = {{A Multi-Stage Proof Logging Framework to Certify the Correctness of CP Solvers}},
     booktitle = {30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
     pages = {11:1--11:20},
     series = {Leibniz International Proceedings in Informatics (LIPIcs)},
     isbn = {978-3-95977-336-2},
     issn = {1868-8969},
     year = {2024},
     volume = {307},
     editor = {Shaw, Paul},
     publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
     address = {Dagstuhl, Germany},
     url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.11},
     urn = {urn:nbn:de:0030-drops-206969},
     doi = {10.4230/LIPIcs.CP.2024.11},
     annote = {Keywords: proof logging, formal verification, constraint programming},
   }

2023

1. Master Thesis: Towards the unification of the Core-Guided and Hitting Set Maximum Satisfiability approaches

   Imko Marijnissen

   Jun 2023

   Abs

   Core-guided solvers and Implicit Hitting Set (IHS) solvers have become ubiquitous within the field of Maximum Satisfiability (MaxSAT). While both types of solvers iteratively increase the solution cost until a satisfiable solution is found, the manner in which this relaxation is performed leads to the belief that these techniques are wholly separate from one another. This work exhibits the difficulty of directly translating the cores found by an IHS-solver to cores utilizable by an OLL-solver due to an inherent disconnect between the manner in which both approaches explore the solution space. It will then be shown how this translation can be performed more easily given certain assumptions. Finally, several techniques are introduced for performing a translation from cores of the original formula to OLL-cores which avoids the aforementioned issue, resulting in a hybrid IHS-OLL algorithm. The comparison between the performance of the hybrid algorithm and RC2 shows that the hybrid algorithm achieves analogous performance in terms of the number of instances solved while indicating that utilising cores of the original formula as a starting point for an OLL solver can be beneficial for the performance of the solver in certain cases.

2021

1. Bachelor Thesis: Solving Cluster Editing Using MaxSAT-based Techniques

   Imko Marijnissen

   Jun 2021

   Abs

   Clustering is a well-studied problem and several algorithms have been developed to find these clusterings under certain constraints. This work will show the applicability of propositional logic (MaxSAT) based approaches to a specific version of correlation clustering called cluster editing. This is the problem of finding the minimum number of edits to turn a given graph into a disjoint union of cliques. This work proposes a combination of modelling, preprocessing and solving techniques to solve the cluster editing problem via propositional logic. This approach’s performance is experimentally evaluated and compared to another search algorithm based on merging vertices and adding/deleting edges. The results show that for certain instances propositional logic based approaches have a satisfactory performance while for other instances the theoretical approach provides a more guided search of the solution space.