Search Results

Documents authored by Musliu, Nysret

Artifact
Software
DOI: 10.4230/artifacts.26941
From LLM Suggestions to Lean Proofs: Verified Redundant Constraints for MiniZinc (Software Artifact)

Authors: Philipp Danzinger and Nysret Musliu

Abstract
Cite as

Philipp Danzinger, Nysret Musliu. From LLM Suggestions to Lean Proofs: Verified Redundant Constraints for MiniZinc (Software Artifact) (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26941,
   title = {{From LLM Suggestions to Lean Proofs: Verified Redundant Constraints for MiniZinc (Software Artifact)}}, 
   author = {Danzinger, Philipp and Musliu, Nysret},
   note = {Software, This research was funded in whole or in part by the Austrian Science Fund (FWF) 10.55776/COE12, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:d20d03c35fe8085bb06a80406c7900a162979876;origin=https://github.com/pdanzinger/cp2026-minizinc-lean;visit=swh:1:snp:7459f5eea9458bf2313ad31b0303597acd94f2b2;anchor=swh:1:rev:0d52168d1fad1c96f295c46308c99c416187e147}{\texttt{swh:1:dir:d20d03c35fe8085bb06a80406c7900a162979876}} (visited on 2026-07-13)},
   url = {https://github.com/pdanzinger/cp2026-minizinc-lean/releases/tag/cp2026-artifact},
   doi = {10.4230/artifacts.26941},
}
Document
DOI: 10.4230/LIPIcs.CP.2026.17
From LLM Suggestions to Lean Proofs: Verified Redundant Constraints for MiniZinc

Authors: Philipp Danzinger and Nysret Musliu

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

Abstract
The performance of constraint models strongly depends on the formulation used. Redundant constraints, which are logically implied by the model, can strengthen propagation and speed up solving, but finding effective ones requires substantial expertise. Recent work has shown that Large Language Models (LLMs) can generate performance-improving constraints for MiniZinc models. However, such approaches offer no soundness guarantees and the generated constraints may exclude optimal solutions or render instances infeasible. We present a pipeline that combines LLM-based constraint generation with empirical evaluation and formal verification. At its core is a novel formalization of a supported MiniZinc subset for verifying redundancy of a constraint schema over all instances by translating MiniZinc models to Lean 4 theorems. We handle MiniZinc’s partial semantics by requiring the base model to be safe and separately proving that the proposed constraint is well-defined for all instances and solutions of the base model. We evaluate the approach on three constraint optimization problems from the literature, starting from published expert-crafted models. The augmented models show a clear improvement on one problem, improved MiniZinc Challenge scores with metric trade-offs on another, and small but non-significant changes on the third.
Cite as

Philipp Danzinger and Nysret Musliu. From LLM Suggestions to Lean Proofs: Verified Redundant Constraints for MiniZinc. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{danzinger_et_al:LIPIcs.CP.2026.17,
  author =	{Danzinger, Philipp and Musliu, Nysret},
  title =	{{From LLM Suggestions to Lean Proofs: Verified Redundant Constraints for MiniZinc}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{17:1--17: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.17},
  URN =		{urn:nbn:de:0030-drops-266504},
  doi =		{10.4230/LIPIcs.CP.2026.17},
  annote =	{Keywords: Redundant constraints, constraint programming, MiniZinc, formal verification, Lean 4, large language models, automated theorem proving}
}
Document
DOI: 10.4230/LIPIcs.CP.2022.41
Modeling and Solving Parallel Machine Scheduling with Contamination Constraints in the Agricultural Industry

Authors: Felix Winter, Sebastian Meiswinkel, Nysret Musliu, and Daniel Walkiewicz

Published in: LIPIcs, Volume 235, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022)

Abstract
Modern-day factories of the agricultural industry need to produce and distribute large amounts of compound feed to handle the daily demands of livestock farming. As a highly-automated production process is utilized to fulfill the large-scale requirements in this domain, finding efficient machine schedules is a challenging task which requires the consideration of complex constraints and the execution of optional cleaning jobs to prevent a contamination of the final products. Furthermore, it is critical to minimize job tardiness in the schedule, since the truck routes which are used to distribute the products to customers are sensitive to delays. Thus, there is a strong need for efficient automated methods which are able to produce optimized schedules in this domain. This paper formally introduces a novel real-life problem from this area and investigates constraint-modeling techniques as well as a metaheuristic approach to efficiently solve practical scenarios. In particular, we investigate two innovative constraint programming model variants as well as a mixed integer quadratic programming formulation to model the contamination constraints which require an efficient utilization of variables with a continuous domain. To tackle large-scale instances, we additionally provide a local search approach based on simulated annealing that utilizes problem-specific neighborhood operators. We provide a set of new real-life problem instances that we use in an extensive experimental evaluation of all proposed approaches. Computational results show that our models can be successfully used together with state-of-the-art constraint solvers to provide several optimal results as well as high-quality bounds for many real-life instances. Additionally, the proposed metaheuristic approach could reach many optimal results and delivers the best upper bounds on many of the large practical instances in our experiments.
Cite as

Felix Winter, Sebastian Meiswinkel, Nysret Musliu, and Daniel Walkiewicz. Modeling and Solving Parallel Machine Scheduling with Contamination Constraints in the Agricultural Industry. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 41:1-41:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{winter_et_al:LIPIcs.CP.2022.41,
  author =	{Winter, Felix and Meiswinkel, Sebastian and Musliu, Nysret and Walkiewicz, Daniel},
  title =	{{Modeling and Solving Parallel Machine Scheduling with Contamination Constraints in the Agricultural Industry}},
  booktitle =	{28th International Conference on Principles and Practice of Constraint Programming (CP 2022)},
  pages =	{41:1--41:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-240-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{235},
  editor =	{Solnon, Christine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2022.41},
  URN =		{urn:nbn:de:0030-drops-166701},
  doi =		{10.4230/LIPIcs.CP.2022.41},
  annote =	{Keywords: Parallel Machine Scheduling, Contamination Constraints, Constraint Programming, Mixed Integer Quadratic Progamming, Metaheuristics, Local Search, Simulated Annealing}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.37
Minimizing Cumulative Batch Processing Time for an Industrial Oven Scheduling Problem

Authors: Marie-Louise Lackner, Christoph Mrkvicka, Nysret Musliu, Daniel Walkiewicz, and Felix Winter

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
We introduce the Oven Scheduling Problem (OSP), a new parallel batch scheduling problem that arises in the area of electronic component manufacturing. Jobs need to be scheduled to one of several ovens and may be processed simultaneously in one batch if they have compatible requirements. The scheduling of jobs must respect several constraints concerning eligibility and availability of ovens, release dates of jobs, setup times between batches as well as oven capacities. Running the ovens is highly energy-intensive and thus the main objective, besides finishing jobs on time, is to minimize the cumulative batch processing time across all ovens. This objective distinguishes the OSP from other batch processing problems which typically minimize objectives related to makespan, tardiness or lateness. We propose to solve this NP-hard scheduling problem via constraint programming (CP) and integer linear programming (ILP) and present corresponding CP- and ILP-models. For an experimental evaluation, we introduce a multi-parameter random instance generator to provide a diverse set of problem instances. Using state-of-the-art solvers, we evaluate the quality and compare the performance of our CP- and ILP-models, which could find optimal solutions for many instances. Furthermore, using our models we are able to provide upper bounds for the whole benchmark set including large-scale instances.
Cite as

Marie-Louise Lackner, Christoph Mrkvicka, Nysret Musliu, Daniel Walkiewicz, and Felix Winter. Minimizing Cumulative Batch Processing Time for an Industrial Oven Scheduling Problem. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 37:1-37:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{lackner_et_al:LIPIcs.CP.2021.37,
  author =	{Lackner, Marie-Louise and Mrkvicka, Christoph and Musliu, Nysret and Walkiewicz, Daniel and Winter, Felix},
  title =	{{Minimizing Cumulative Batch Processing Time for an Industrial Oven Scheduling Problem}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{37:1--37:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.37},
  URN =		{urn:nbn:de:0030-drops-153286},
  doi =		{10.4230/LIPIcs.CP.2021.37},
  annote =	{Keywords: Oven Scheduling Problem, Parallel Batch Processing, Constraint Programming, Integer Linear Programming}
}
Document
DOI: 10.4230/OASIcs.SCOR.2016.7
Feature Extractors for Describing Vehicle Routing Problem Instances

Authors: Jussi Rasku, Tommi Kärkkäinen, and Nysret Musliu

Published in: OASIcs, Volume 50, 5th Student Conference on Operational Research (SCOR 2016)

Abstract
The vehicle routing problem comes in varied forms. In addition to usual variants with diverse constraints and specialized objectives, the problem instances themselves – even from a single shared source - can be distinctly different. Heuristic, metaheuristic, and hybrid algorithms that are typically used to solve these problems are sensitive to this variation and can exhibit erratic performance when applied on new, previously unseen instances. To mitigate this, and to improve their applicability, algorithm developers often choose to expose parameters that allow customization of the algorithm behavior. Unfortunately, finding a good set of values for these parameters can be a tedious task that requires extensive experimentation and experience. By deriving descriptors for the problem classes and instances, one would be able to apply learning and adaptive methods that, when taught, can effectively exploit the idiosyncrasies of a problem instance. Furthermore, these methods can generalize from previously learnt knowledge by inferring suitable values for these parameters. As a necessary intermediate step towards this goal, we propose a set of feature extractors for vehicle routing problems. The descriptors include dimensionality of the problem; statistical descriptors of distances, demands, etc.; clusterability of the vertex locations; and measures derived using fitness landscape analysis. We show the relevancy of these features by performing clustering on classical problem instances and instance-specific algorithm configuration of vehicle routing metaheuristics.
Cite as

Jussi Rasku, Tommi Kärkkäinen, and Nysret Musliu. Feature Extractors for Describing Vehicle Routing Problem Instances. In 5th Student Conference on Operational Research (SCOR 2016). Open Access Series in Informatics (OASIcs), Volume 50, pp. 7:1-7:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{rasku_et_al:OASIcs.SCOR.2016.7,
  author =	{Rasku, Jussi and K\"{a}rkk\"{a}inen, Tommi and Musliu, Nysret},
  title =	{{Feature Extractors for Describing Vehicle Routing Problem Instances}},
  booktitle =	{5th Student Conference on Operational Research (SCOR 2016)},
  pages =	{7:1--7:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-004-0},
  ISSN =	{2190-6807},
  year =	{2016},
  volume =	{50},
  editor =	{Hardy, Bradley and Qazi, Abroon and Ravizza, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SCOR.2016.7},
  URN =		{urn:nbn:de:0030-drops-65193},
  doi =		{10.4230/OASIcs.SCOR.2016.7},
  annote =	{Keywords: Metaheuristics, Vehicle Routing Problem, Feature extraction, Unsupervised learning, Automatic Algorithm Configuration}
}
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