27 Search Results for "Rossi, Francesca"

Document
Research
DOI: 10.4230/TGDK.3.3.1
A Logic Programming Approach to Repairing SHACL Constraint Violations

Authors: Shqiponja Ahmetaj, Robert David, Axel Polleres, and Mantas Šimkus

Published in: TGDK, Volume 3, Issue 3 (2025). Transactions on Graph Data and Knowledge, Volume 3, Issue 3

Abstract
The Shapes Constraint Language (SHACL) is a recent standard, a W3C recommendation, for validating RDF graphs against shape constraints to be checked on target nodes of a data graph. The standard also describes the notion of validation reports, which detail the results of the validation process. In case of violation of constraints, the validation report should explain the reasons for non-validation, offering guidance on how to identify or fix violations in the data graph. Since the specification left it open to SHACL processors to define such explanations, a recent work proposed the use of explanations in the style of database repairs, where a repair is a set of additions to or deletions from the data graph so that the resulting graph validates against the constraints. In this paper, we study such repairs for non-recursive SHACL, the largest fragment of SHACL that is fully defined in the specification. We propose an algorithm to compute repairs by encoding the explanation problem - using Answer Set Programming (ASP) - into a logic program, where the answer sets contain (minimal) repairs. We then study a scenario where it is not possible to simultaneously repair all the targets, which may be the case due to overall unsatisfiability or conflicting constraints. We introduce a relaxed notion of validation, which allows to validate a (maximal) subset of the targets and adapt the ASP translation to take into account this relaxation. Finally, we add support for repairing constraints which use property paths and equality of paths. Our implementation in clingo is - to the best of our knowledge - the first implementation of a repair program for SHACL.
Cite as

Shqiponja Ahmetaj, Robert David, Axel Polleres, and Mantas Šimkus. A Logic Programming Approach to Repairing SHACL Constraint Violations. In Transactions on Graph Data and Knowledge (TGDK), Volume 3, Issue 3, pp. 1:1-1:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{ahmetaj_et_al:TGDK.3.3.1,
  author =	{Ahmetaj, Shqiponja and David, Robert and Polleres, Axel and \v{S}imkus, Mantas},
  title =	{{A Logic Programming Approach to Repairing SHACL Constraint Violations}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{1:1--1:36},
  ISSN =	{2942-7517},
  year =	{2025},
  volume =	{3},
  number =	{3},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.3.3.1},
  URN =		{urn:nbn:de:0030-drops-252124},
  doi =		{10.4230/TGDK.3.3.1},
  annote =	{Keywords: SHACL, Shapes Constraint Language, Database Repairs, Knowledge Graphs, Semantic Web, Answer Set Programming}
}
Document
DOI: 10.4230/OASIcs.DX.2025.1
Beyond Static Diagnosis: A Temporal ASP Framework for HVAC Fault Detection

Authors: Roxane Koitz-Hristov, Liliana Marie Prikler, and Franz Wotawa

Published in: OASIcs, Volume 136, 36th International Conference on Principles of Diagnosis and Resilient Systems (DX 2025)

Abstract
Improving sustainability in the building sector requires more efficient operation of energy-intensive systems such as Heating, Ventilation, and Air Conditioning (HVAC). We present a novel diagnostic framework for HVAC systems that integrates Answer Set Programming (ASP) with Functional Event Calculus (FEC). Our approach exploits the declarative nature of ASP for modeling and incorporates FEC to capture temporal system dynamics. We demonstrate the feasibility of our approach through a case study on a real-world heating system, where we model key components and system constraints. Our evaluation on nominal and faulty traces shows that exploiting ASP in combination with FEC can identify plausible diagnoses. Moreover, we explore the difference between static and rolling-window strategies and provide insights into runtime versus soundness on those variants. Our work provides a step toward the practical application of ASP-based temporal reasoning in building diagnostics.
Cite as

Roxane Koitz-Hristov, Liliana Marie Prikler, and Franz Wotawa. Beyond Static Diagnosis: A Temporal ASP Framework for HVAC Fault Detection. In 36th International Conference on Principles of Diagnosis and Resilient Systems (DX 2025). Open Access Series in Informatics (OASIcs), Volume 136, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{koitzhristov_et_al:OASIcs.DX.2025.1,
  author =	{Koitz-Hristov, Roxane and Prikler, Liliana Marie and Wotawa, Franz},
  title =	{{Beyond Static Diagnosis: A Temporal ASP Framework for HVAC Fault Detection}},
  booktitle =	{36th International Conference on Principles of Diagnosis and Resilient Systems (DX 2025)},
  pages =	{1:1--1:20},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-394-2},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{136},
  editor =	{Quinones-Grueiro, Marcos and Biswas, Gautam and Pill, Ingo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.DX.2025.1},
  URN =		{urn:nbn:de:0030-drops-247901},
  doi =		{10.4230/OASIcs.DX.2025.1},
  annote =	{Keywords: Model-based diagnosis, Answer set programming, HVAC, Modeling for diagnosis, Experimental evaluation}
}
Document
DOI: 10.4230/OASIcs.SpaceCHI.2025.31
Monitoring the Structural Health of Space Habitats Through Immersive Data Art Visualization

Authors: Ze Gao, Yuan Zhuang, Kunqi Wang, and Mengyao Guo

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)

Abstract
As humanity advances toward long-term space habitation, traditional SHM systems - reliant on abstract data representations - struggle to support rapid decision-making in extreme environments. This study addresses this critical gap by introducing an engineering-art-human factors framework that transforms SHM through immersive data-art visualization. By integrating sensor networks and machine learning, structural data (stress, vibration, deformation) is converted into intuitive visual languages: dynamic color gradients and biomimetic morphologies leverage perceptual laws (e.g., Weber-Fechner) to amplify critical signals. Multimodal interfaces (AR, haptic feedback) and natural elements mitigate cognitive load and psychological stress in confined habitats. Our contribution lies in redefining SHM as a synergy of precision and intuition, enabling "at-a-glance" assessments while balancing functionality and human-centric design. The urgency of this research stems from the inadequacy of conventional systems in extreme space conditions and the growing demand for astronaut safety and operational efficiency. This framework not only pioneers a sustainable monitoring paradigm for space habitats but also extends to terrestrial high-risk infrastructure, demonstrating the necessity of interdisciplinary innovation in extreme environments.
Cite as

Ze Gao, Yuan Zhuang, Kunqi Wang, and Mengyao Guo. Monitoring the Structural Health of Space Habitats Through Immersive Data Art Visualization. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 31:1-31:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gao_et_al:OASIcs.SpaceCHI.2025.31,
  author =	{Gao, Ze and Zhuang, Yuan and Wang, Kunqi and Guo, Mengyao},
  title =	{{Monitoring the Structural Health of Space Habitats Through Immersive Data Art Visualization}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{31:1--31:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.31},
  URN =		{urn:nbn:de:0030-drops-240217},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.31},
  annote =	{Keywords: Structural health monitoring, space habitats, immersive visualization, human-centered design, interdisciplinary innovation}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.61
Quantum Relaxations of CSP and Structure Isomorphism

Authors: Amin Karamlou

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We investigate quantum relaxations of two key decision problems in computer science: the constraint satisfaction problem (CSP) and the structure isomorphism problem. CSP asks whether a homomorphism exists between two relational structures, while structure isomorphism seeks an isomorphism between them. In recent years, it has become increasingly apparent that many special cases of CSP can be reformulated in terms of the existence of perfect classical strategies in non-local games, a key topic of study in quantum information theory. These games have allowed us to study quantum advantage in relation to many important decision problems, such as the k-colouring problem, and the problem of solving binary constraint systems. Abramsky et al. (2017) have shown that all of these games can be seen as special instances of a non-local CSP game. Moreover, they show that perfect quantum strategies in this CSP game can be viewed as Kleisli morphisms of a graded monad on the category of relational structures, which they dub the quantum monad. In this way, the quantum monad provides a categorical characterisation of quantum advantage for the non-local CSP game. In this work we solidify and expand the results of Abramsky et al., answering several of their open questions. Firstly, we compare the definition of quantum graph homomorphisms arising from this work with an earlier definition of the concept due to Mančinska and Roberson and show that there are graphs which exhibit quantum advantage under one definition but not the other. Our second contribution is to extend the results of Abramsky et al. which only hold in the tensor product framework of quantum mechanics to the commuting operator framework. Next, we study a non-local structure isomorphism game, which generalises the well-studied graph isomorphism game. We show how the construction of the quantum monad can be refined to provide categorical semantics for quantum strategies in this game. This results in a category where morphisms coincide with quantum homomorphisms and isomorphisms coincide with quantum isomorphisms.
Cite as

Amin Karamlou. Quantum Relaxations of CSP and Structure Isomorphism. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 61:1-61:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{karamlou:LIPIcs.MFCS.2025.61,
  author =	{Karamlou, Amin},
  title =	{{Quantum Relaxations of CSP and Structure Isomorphism}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{61:1--61:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.61},
  URN =		{urn:nbn:de:0030-drops-241686},
  doi =		{10.4230/LIPIcs.MFCS.2025.61},
  annote =	{Keywords: CSP, graph isomorphism, quantum information, non-local game, quantum graph homomorphism, monad}
}
Document
DOI: 10.4230/LIPIcs.WABI.2025.12
Extension of Partial Atom-To-Atom Maps: Uniqueness and Algorithms

Authors: Marcos E. González Laffitte, Tieu-Long Phan, and Peter F. Stadler

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

Abstract
Chemical reaction databases typically report the molecular structures of reactant and product compounds, as well as their stoichiometry, but lack information, in particular, on the correspondence of reactant and product atoms. These atom-to-atom maps (AAM), however, are crucial for applications including chemical synthesis planning in organic chemistry and the analysis of isotope labeling experiments in modern metabolomics. AAMs therefore need to be reconstructed computationally. This situation is aggravated, furthermore, by the fact that chemically correct AAMs are, fundamentally, determined by quantum-mechanical phenomena and thus cannot be reliably computed by solving graph-theoretical optimization problems defined by the reactant and product structures. A viable solution for this problem is to shift the focus into first identifying a partial AAM containing the reaction center, i.e., covering the atoms incident with all bonds that change during a reaction. This then leads to the problem of extending the partial map to the full reaction. The AAM of a reaction is faithfully represented by the Imaginary Transition State (ITS) graph, providing a convenient graph-theoretic framework to address the questions of when and how a partial AAM can be extended. We show that an unique extension exists whenever, and only if, these partial AAMs cover the reaction center. In this case their extension can be computed by solving a constrained graph-isomorphism search between specific subgraphs of ITS graphs. We close by benchmarking different tools for this task.
Cite as

Marcos E. González Laffitte, Tieu-Long Phan, and Peter F. Stadler. Extension of Partial Atom-To-Atom Maps: Uniqueness and Algorithms. In 25th International Conference on Algorithms for Bioinformatics (WABI 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 344, pp. 12:1-12:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gonzalezlaffitte_et_al:LIPIcs.WABI.2025.12,
  author =	{Gonz\'{a}lez Laffitte, Marcos E. and Phan, Tieu-Long and Stadler, Peter F.},
  title =	{{Extension of Partial Atom-To-Atom Maps: Uniqueness and Algorithms}},
  booktitle =	{25th International Conference on Algorithms for Bioinformatics (WABI 2025)},
  pages =	{12:1--12:26},
  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.12},
  URN =		{urn:nbn:de:0030-drops-239410},
  doi =		{10.4230/LIPIcs.WABI.2025.12},
  annote =	{Keywords: atom-to-atom maps, imaginary transition state (ITS) graphs, condensed graph of the reaction (CGR), chemical reaction mechanisms, molecular graphs, metabolic networks, chemical synthesis planning, constrained graph isomorphism}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.38
Reducing Quantum Circuit Synthesis to #SAT

Authors: Dekel Zak, Jingyi Mei, Jean-Marie Lagniez, and Alfons Laarman

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

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
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}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.4
Conflict Analysis Based on Cutting-Planes for Constraint Programming

Authors: Robbin Baauw, Maarten Flippo, and Emir Demirović

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

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
DOI: 10.4230/LIPIcs.CP.2025.6
Modeling and Explaining an Industrial Workforce Allocation and Scheduling Problem

Authors: Ignace Bleukx, Ryma Boumazouza, Tias Guns, Nadine Laage, and Guillaume Poveda

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

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
DOI: 10.4230/LIPIcs.CP.2025.35
Unite and Lead: Finding Disjunctive Cliques for Scheduling Problems

Authors: Konstantin Sidorov, Imko Marijnissen, and Emir Demirović

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

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
DOI: 10.4230/LIPIcs.SAT.2025.15
RustSAT: A Library for SAT Solving in Rust

Authors: Christoph Jabs

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
State-of-the-art Boolean satisfiability (SAT) solvers constitute a practical and competitive approach for solving various real-world problems. To encourage their widespread adoption, the relatively high barrier of entry following from the low level syntax of SAT and the expert knowledge required to achieve tight integration with SAT solvers should be further reduced. We present RustSAT, a library with the aim of making SAT solving technology readily available in the Rust programming language. RustSAT provides functionality for helping with generating (Max)SAT instances, writing them to, or reading them from files. Furthermore, RustSAT includes interfaces to various state-of-the-art SAT solvers available with a unified Rust API. Lastly, RustSAT implements several encodings for higher level constraints (at-most-one, cardinality, and pseudo-Boolean), which are also available via a C and Python API.
Cite as

Christoph Jabs. RustSAT: A Library for SAT Solving in Rust. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 15:1-15:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jabs:LIPIcs.SAT.2025.15,
  author =	{Jabs, Christoph},
  title =	{{RustSAT: A Library for SAT Solving in Rust}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{15:1--15:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.15},
  URN =		{urn:nbn:de:0030-drops-237498},
  doi =		{10.4230/LIPIcs.SAT.2025.15},
  annote =	{Keywords: Rust, library, SAT solvers, constraint encodings}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.3
Problem Partitioning via Proof Prefixes

Authors: Zachary Battleman, Joseph E. Reeves, and Marijn J. H. Heule

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Satisfiability solvers have been instrumental in tackling hard problems, including mathematical challenges that require years of computation. A key obstacle in efficiently solving such problems lies in effectively partitioning them into many, frequently millions of subproblems. Existing automated partitioning techniques, primarily based on lookahead methods, perform well on some instances but fail to generate effective partitions for many others. This paper introduces a powerful partitioning approach that leverages prefixes of proofs derived from conflict-driven clause-learning solvers. This method enables non-experts to harness the power of massively parallel SAT solving for their problems. We also propose a semantically-driven partitioning technique tailored for problems with large cardinality constraints, which frequently arise in optimization tasks. We evaluate our methods on diverse benchmarks, including combinatorial problems and formulas from SAT and MaxSAT competitions. Our results demonstrate that these techniques outperform existing partitioning strategies in many cases, offering improved scalability and efficiency.
Cite as

Zachary Battleman, Joseph E. Reeves, and Marijn J. H. Heule. Problem Partitioning via Proof Prefixes. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{battleman_et_al:LIPIcs.SAT.2025.3,
  author =	{Battleman, Zachary and Reeves, Joseph E. and Heule, Marijn J. H.},
  title =	{{Problem Partitioning via Proof Prefixes}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{3:1--3:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.3},
  URN =		{urn:nbn:de:0030-drops-237378},
  doi =		{10.4230/LIPIcs.SAT.2025.3},
  annote =	{Keywords: Satisfiability solving, parallel computing, problem partitioning}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.26
Analyzing Reformulation Performance in Core-Guided MaxSAT Solving

Authors: André Schidler and Stefan Szeider

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Core-guided algorithms like OLL are among the best methods for solving the Maximum Satisfiability problem (MaxSAT). Although some performance characteristics of OLL have been studied, a comprehensive experimental analysis of its reformulation behavior is still missing. In this paper, we present a large-scale study on how different reformulations of a MaxSAT instance produced by OLL affect solver performance. By representing these reformulations as a directed acyclic graph (DAG), we isolate the impact of structural features - such as the size and interconnectivity of unsatisfiable cores - on solver runtime. Our extensive experimental evaluation of over 600k solver runs reveals clear correlations between DAG properties and performance outcomes. These results suggest a new avenue for designing heuristics that steer the solver toward more tractable reformulations. All OLL DAGs and performance data from our experiments are publicly available to foster further research.
Cite as

André Schidler and Stefan Szeider. Analyzing Reformulation Performance in Core-Guided MaxSAT Solving. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{schidler_et_al:LIPIcs.SAT.2025.26,
  author =	{Schidler, Andr\'{e} and Szeider, Stefan},
  title =	{{Analyzing Reformulation Performance in Core-Guided MaxSAT Solving}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.26},
  URN =		{urn:nbn:de:0030-drops-237605},
  doi =		{10.4230/LIPIcs.SAT.2025.26},
  annote =	{Keywords: maximum satisfiability, OLL, core-guided}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2025.10
EGGs Are Adhesive!

Authors: Roberto Biondo, Davide Castelnovo, and Fabio Gadducci

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
The use of rewriting-based visual formalisms is on the rise. In the formal methods community, this is due also to the introduction of adhesive categories, where most properties of classical approaches to graph transformation, such as those on parallelism and confluence, can be rephrased and proved in a general and uniform way. E-graphs (EGGs) are a formalism for program optimisation via an efficient implementation of equality saturation. In short, EGGs can be defined as (acyclic) term graphs with an additional notion of equivalence on nodes that is closed under the operators of the signature. Instead of replacing the components of a program, the optimisation step is performed by adding new components and linking them to the existing ones via an equivalence relation, until an optimal program is reached. This work describes EGGs via adhesive categories. Besides the benefits in itself of a formal presentation, which renders precise the properties of the data structure, the description of the addition of equivalent program components using standard graph transformation tools offers the advantages of the adhesive framework in modelling, for example, concurrent updates.
Cite as

Roberto Biondo, Davide Castelnovo, and Fabio Gadducci. EGGs Are Adhesive!. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{biondo_et_al:LIPIcs.CALCO.2025.10,
  author =	{Biondo, Roberto and Castelnovo, Davide and Gadducci, Fabio},
  title =	{{EGGs Are Adhesive!}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.10},
  URN =		{urn:nbn:de:0030-drops-235690},
  doi =		{10.4230/LIPIcs.CALCO.2025.10},
  annote =	{Keywords: Hypergraphs, terms graphs, e-graphs, adhesive categories}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2025.14
Algorithms for the Diverse-k-SAT Problem: The Geometry of Satisfying Assignments

Authors: Per Austrin, Ioana O. Bercea, Mayank Goswami, Nutan Limaye, and Adarsh Srinivasan

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Given a k-CNF formula and an integer s ≥ 2, we study algorithms that obtain s solutions to the formula that are as dispersed as possible. For s = 2, this problem of computing the diameter of a k-CNF formula was initiated by Creszenzi and Rossi, who showed strong hardness results even for k = 2. The current best upper bound [Angelsmark and Thapper '04] goes to 4ⁿ as k → ∞. As our first result, we show that this quadratic blow up is not necessary by utilizing the Fast-Fourier transform (FFT) to give a O^*(2ⁿ) time exact algorithm for computing the diameter of any k-CNF formula. For s > 2, the problem was raised in the SAT community (Nadel '11) and several heuristics have been proposed for it, but no algorithms with theoretical guarantees are known. We give exact algorithms using FFT and clique-finding that run in O^*(2^{(s-1)n}) and O^*(s² |Ω_{𝐅}|^{ω ⌈ s/3 ⌉}) respectively, where |Ω_{𝐅}| is the size of the solutions space of the formula 𝐅 and ω is the matrix multiplication exponent. However, current SAT algorithms for finding one solution run in time O^*(2^{ε_{k}n}) for ε_{k} ≈ 1-Θ(1/k), which is much faster than all above run times. As our main result, we analyze two popular SAT algorithms - PPZ (Paturi, Pudlák, Zane '97) and Schöning’s ('02) algorithms, and show that in time poly(s)O^*(2^{ε_{k}n}), they can be used to approximate diameter as well as the dispersion (s > 2) problem. While we need to modify Schöning’s original algorithm for technical reasons, we show that the PPZ algorithm, without any modification, samples solutions in a geometric sense. We believe this geometric sampling property of PPZ may be of independent interest. Finally, we focus on diverse solutions to NP-complete optimization problems, and give bi-approximations running in time poly(s)O^*(2^{ε n}) with ε < 1 for several problems such as Maximum Independent Set, Minimum Vertex Cover, Minimum Hitting Set, Feedback Vertex Set, Multicut on Trees and Interval Vertex Deletion. For all of these problems, all existing exact methods for finding optimal diverse solutions have a runtime with at least an exponential dependence on the number of solutions s. Our methods show that by relaxing to bi-approximations, this dependence on s can be made polynomial.
Cite as

Per Austrin, Ioana O. Bercea, Mayank Goswami, Nutan Limaye, and Adarsh Srinivasan. Algorithms for the Diverse-k-SAT Problem: The Geometry of Satisfying Assignments. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{austrin_et_al:LIPIcs.ICALP.2025.14,
  author =	{Austrin, Per and Bercea, Ioana O. and Goswami, Mayank and Limaye, Nutan and Srinivasan, Adarsh},
  title =	{{Algorithms for the Diverse-k-SAT Problem: The Geometry of Satisfying Assignments}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.14},
  URN =		{urn:nbn:de:0030-drops-233916},
  doi =		{10.4230/LIPIcs.ICALP.2025.14},
  annote =	{Keywords: Exponential time algorithms, Satisfiability, k-SAT, PPZ, Sch\"{o}ning, Dispersion, Diversity}
}
  • Refine by Type
  • 27 Document/PDF
  • 22 Document/HTML

  • Refine by Publication Year
  • 18 2025
  • 1 2024
  • 4 2023
  • 1 2020
  • 1 2016
  • Show More...

  • Refine by Author
  • 4 Rossi, Francesca
  • 2 Demirović, Emir
  • 2 Endriss, Ulle
  • 2 Lang, Jérôme
  • 2 Polleres, Axel
  • Show More...

  • Refine by Series/Journal
  • 17 LIPIcs
  • 3 OASIcs
  • 5 TGDK
  • 2 DagSemProc

  • Refine by Classification
  • 8 Theory of computation → Constraint and logic programming
  • 2 Computing methodologies → Knowledge representation and reasoning
  • 2 Computing methodologies → Logic programming and answer set programming
  • 2 Computing methodologies → Planning and scheduling
  • 1 Computing methodologies → Causal reasoning and diagnostics
  • Show More...

  • Refine by Keyword
  • 2 Computational social choice
  • 2 Constraint Programming
  • 2 Knowledge Graphs
  • 2 Scheduling
  • 2 algorithms
  • 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