27 Search Results for "Huang, Wen-Hung"

Document
DOI: 10.4230/LIPIcs.ESA.2024.39
List Homomorphisms by Deleting Edges and Vertices: Tight Complexity Bounds for Bounded-Treewidth Graphs

Authors: Barış Can Esmer, Jacob Focke, Dániel Marx, and Paweł Rzążewski

Published in: LIPIcs, Volume 308, 32nd Annual European Symposium on Algorithms (ESA 2024)

Abstract
The goal of this paper is to investigate a family of optimization problems arising from list homomorphisms, and to understand what the best possible algorithms are if we restrict the problem to bounded-treewidth graphs. Given graphs G, H, and lists L(v) ⊆ V(H) for every v ∈ V(G), a list homomorphism from (G,L) to H is a function f:V(G) → V(H) that preserves the edges (i.e., uv ∈ E(G) implies f(u)f(v) ∈ E(H)) and respects the lists (i.e., f(v) ∈ L(v)). The graph H may have loops. For a fixed H, the input of the optimization problem LHomVD(H) is a graph G with lists L(v), and the task is to find a set X of vertices having minimum size such that (G-X,L) has a list homomorphism to H. We define analogously the edge-deletion variant LHomED(H), where we have to delete as few edges as possible from G to obtain a graph that has a list homomorphism. This expressive family of problems includes members that are essentially equivalent to fundamental problems such as Vertex Cover, Max Cut, Odd Cycle Transversal, and Edge/Vertex Multiway Cut. For both variants, we first characterize those graphs H that make the problem polynomial-time solvable and show that the problem is NP-hard for every other fixed H. Second, as our main result, we determine for every graph H for which the problem is NP-hard, the smallest possible constant c_H such that the problem can be solved in time c^t_H⋅ n^{𝒪(1)} if a tree decomposition of G having width t is given in the input. Let i(H) be the maximum size of a set of vertices in H that have pairwise incomparable neighborhoods. For the vertex-deletion variant LHomVD(H), we show that the smallest possible constant is i(H)+1 for every H: - Given a tree decomposition of width t of G, LHomVD(H) can be solved in time (i(H)+1)^t⋅ n^{𝒪(1)}. - For any ε > 0 and H, an (i(H)+1-ε)^t⋅ n^{𝒪(1)} algorithm would violate the Strong Exponential-Time Hypothesis (SETH). The situation is more complex for the edge-deletion version. For every H, one can solve LHomED(H) in time i(H)^t⋅ n^{𝒪(1)} if a tree decomposition of width t is given. However, the existence of a specific type of decomposition of H shows that there are graphs H where LHomED(H) can be solved significantly more efficiently and the best possible constant can be arbitrarily smaller than i(H). Nevertheless, we determine this best possible constant and (assuming the SETH) prove tight bounds for every fixed H.
Cite as

Barış Can Esmer, Jacob Focke, Dániel Marx, and Paweł Rzążewski. List Homomorphisms by Deleting Edges and Vertices: Tight Complexity Bounds for Bounded-Treewidth Graphs. In 32nd Annual European Symposium on Algorithms (ESA 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 308, pp. 39:1-39:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{canesmer_et_al:LIPIcs.ESA.2024.39,
  author =	{Can Esmer, Bar{\i}\c{s} and Focke, Jacob and Marx, D\'{a}niel and Rz\k{a}\.{z}ewski, Pawe{\l}},
  title =	{{List Homomorphisms by Deleting Edges and Vertices: Tight Complexity Bounds for Bounded-Treewidth Graphs}},
  booktitle =	{32nd Annual European Symposium on Algorithms (ESA 2024)},
  pages =	{39:1--39:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-338-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{308},
  editor =	{Chan, Timothy and Fischer, Johannes and Iacono, John and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2024.39},
  URN =		{urn:nbn:de:0030-drops-211103},
  doi =		{10.4230/LIPIcs.ESA.2024.39},
  annote =	{Keywords: Graph Homomorphism, List Homomorphism, Vertex Deletion, Edge Deletion, Multiway Cut, Parameterized Complexity, Tight Bounds, Treewidth, SETH}
}
Document
DOI: 10.4230/LIPIcs.ESA.2024.66
Shortest Path Separators in Unit Disk Graphs

Authors: Elfarouk Harb, Zhengcheng Huang, and Da Wei Zheng

Published in: LIPIcs, Volume 308, 32nd Annual European Symposium on Algorithms (ESA 2024)

Abstract
We introduce a new balanced separator theorem for unit-disk graphs involving two shortest paths combined with the 1-hop neighbours of those paths and two other vertices. This answers an open problem of Yan, Xiang and Dragan [CGTA '12] and improves their result that requires removing the 3-hop neighbourhood of two shortest paths. Our proof uses very different ideas, including Delaunay triangulations and a generalization of the celebrated balanced separator theorem of Lipton and Tarjan [J. Appl. Math. '79] to systems of non-intersecting paths.
Cite as

Elfarouk Harb, Zhengcheng Huang, and Da Wei Zheng. Shortest Path Separators in Unit Disk Graphs. In 32nd Annual European Symposium on Algorithms (ESA 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 308, pp. 66:1-66:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{harb_et_al:LIPIcs.ESA.2024.66,
  author =	{Harb, Elfarouk and Huang, Zhengcheng and Zheng, Da Wei},
  title =	{{Shortest Path Separators in Unit Disk Graphs}},
  booktitle =	{32nd Annual European Symposium on Algorithms (ESA 2024)},
  pages =	{66:1--66:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-338-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{308},
  editor =	{Chan, Timothy and Fischer, Johannes and Iacono, John and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2024.66},
  URN =		{urn:nbn:de:0030-drops-211375},
  doi =		{10.4230/LIPIcs.ESA.2024.66},
  annote =	{Keywords: Balanced shortest path separators, unit disk graphs, crossings}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.13
Pure Methods for roDOT

Authors: Vlastimil Dort, Yufeng Li, Ondřej Lhoták, and Pavel Parízek

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Object-oriented programming languages typically allow mutation of objects, but pure methods are common too. There is great interest in recognizing which methods are pure, because it eases analysis of program behavior and allows modifying the program without changing its behavior. The roDOT calculus is a formal calculus extending DOT with reference mutability. In this paper, we explore purity conditions in roDOT and pose a SEF guarantee, by which the type system guarantees that methods of certain types are side-effect free. We use the idea from ReIm to detect pure methods by argument types. Applying this idea to roDOT required just a few changes to the type system, but necessitated re-working a significant part of the soundness proof. In addition, we state a transformation guarantee, which states that in a roDOT program, calls to SEF methods can be safely reordered without changing the outcome of the program. We proved type soundness of the updated roDOT calculus, using multiple layers of typing judgments. We proved the SEF guarantee by applying the Immutability guarantee, and the transformation guarantee by applying the SEF guarantee within a framework for reasoning about safe transformations of roDOT programs. All proofs are mechanized in Coq.
Cite as

Vlastimil Dort, Yufeng Li, Ondřej Lhoták, and Pavel Parízek. Pure Methods for roDOT. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 13:1-13:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dort_et_al:LIPIcs.ECOOP.2024.13,
  author =	{Dort, Vlastimil and Li, Yufeng and Lhot\'{a}k, Ond\v{r}ej and Par{\'\i}zek, Pavel},
  title =	{{Pure Methods for roDOT}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{13:1--13:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.13},
  URN =		{urn:nbn:de:0030-drops-208624},
  doi =		{10.4230/LIPIcs.ECOOP.2024.13},
  annote =	{Keywords: type systems, DOT calculus, pure methods}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.29
Generalizing Shape Analysis with Gradual Types

Authors: Zeina Migeed, James Reed, Jason Ansel, and Jens Palsberg

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Tensors are multi-dimensional data structures that can represent the data processed by machine learning tasks. Tensor programs tend to be short and readable, and they can leverage libraries and frameworks such as TensorFlow and PyTorch, as well as modern hardware such as GPUs and TPUs. However, tensor programs also tend to obscure shape information, which can cause shape errors that are difficult to find. Such shape errors can be avoided by a combination of shape annotations and shape analysis, but such annotations are burdensome to come up with manually. In this paper, we use gradual typing to reduce the barrier of entry. Gradual typing offers a way to incrementally introduce type annotations into programs. From there, we focus on tool support for type migration, which is a concept that closely models code-annotation tasks and allows us to do shape reasoning and utilize it for different purposes. We develop a comprehensive gradual typing theory to reason about tensor shapes. We then ask three fundamental questions about a gradually typed tensor program. (1) Does the program have a static migration? (2) Given a program and some arithmetic constraints on shapes, can we migrate the program according to the constraints? (3) Can we eliminate branches that depend on shapes? We develop novel tools to address the three problems. For the third problem, there are currently two PyTorch tools that aim to eliminate branches. They do so by eliminating them for just a single input. Our tool is the first to eliminate branches for an infinite class of inputs, using static shape information. Our tools help prevent bugs, alleviate the burden on the programmer of annotating the program, and improves the process of program transformation.
Cite as

Zeina Migeed, James Reed, Jason Ansel, and Jens Palsberg. Generalizing Shape Analysis with Gradual Types. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 29:1-29:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{migeed_et_al:LIPIcs.ECOOP.2024.29,
  author =	{Migeed, Zeina and Reed, James and Ansel, Jason and Palsberg, Jens},
  title =	{{Generalizing Shape Analysis with Gradual Types}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{29:1--29:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.29},
  URN =		{urn:nbn:de:0030-drops-208786},
  doi =		{10.4230/LIPIcs.ECOOP.2024.29},
  annote =	{Keywords: Tensor Shapes, Gradual Types, Migration}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.COSIT.2024.31
Large Language Models: Testing Their Capabilities to Understand and Explain Spatial Concepts (Short Paper)

Authors: Majid Hojati and Rob Feick

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
Interest in applying Large Language Models (LLMs), which use natural language processing (NLP) to provide human-like responses to text-based questions, to geospatial tasks has grown rapidly. Research shows that LLMs can help generate software code and answer some types of geographic questions to varying degrees even without fine-tuning. However, further research is required to explore the types of spatial questions they answer correctly, their abilities to apply spatial reasoning, and the variability between models. In this paper we examine the ability of four LLM models (GPT3.5 and 4, LLAma2.0, Falcon40B) to answer spatial questions that range from basic calculations to more advanced geographic concepts. The intent of this comparison is twofold. First, we demonstrate an extensible method for evaluating LLM’s limitations to supporting spatial data science through correct calculations and code generation. Relatedly, we also consider how these models can aid geospatial learning by providing text-based explanations of spatial concepts and operations. Our research shows common strengths in more basic types of questions, and mixed results for questions relating to more advanced spatial concepts. These results provide insights that may be used to inform strategies for testing and fine-tuning these models to increase their understanding of key spatial concepts.
Cite as

Majid Hojati and Rob Feick. Large Language Models: Testing Their Capabilities to Understand and Explain Spatial Concepts (Short Paper). In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 31:1-31:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hojati_et_al:LIPIcs.COSIT.2024.31,
  author =	{Hojati, Majid and Feick, Rob},
  title =	{{Large Language Models: Testing Their Capabilities to Understand and Explain Spatial Concepts}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{31:1--31:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.31},
  URN =		{urn:nbn:de:0030-drops-208460},
  doi =		{10.4230/LIPIcs.COSIT.2024.31},
  annote =	{Keywords: Geospatial concepts, Large Language Models, LLM, GPT, Llama, Falcon}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.16
Effect Semantics for Quantum Process Calculi

Authors: Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
The development of quantum communication protocols sparked the interest in quantum extensions of process calculi and behavioural equivalences, but defining a bisimilarity that matches the observational properties of a quantum-capable system is a surprisingly difficult task. The two proposals explicitly addressing this issue, qCCS and lqCCS, do not define an algorithmic verification scheme: the bisimilarity of two processes is proven by comparing their behaviour under all input states. We introduce a new semantic model based on effects, i.e. probabilistic predicates on quantum states that represent their observable properties. We define and investigate the properties of effect distributions and effect labelled transition systems (eLTSs), generalizing probability distributions and probabilistic labelled transition systems (pLTSs), respectively. As a proof of concept, we provide an eLTS-based semantics for a minimal quantum process algebra, which we prove sound and complete with respect to the observable probabilistic behaviour of quantum processes. To the best of our knowledge, ours is the first algorithmically verifiable proposal that abides to the properties of quantum theory.
Cite as

Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Effect Semantics for Quantum Process Calculi. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 16:1-16:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ceragioli_et_al:LIPIcs.CONCUR.2024.16,
  author =	{Ceragioli, Lorenzo and Gadducci, Fabio and Lomurno, Giuseppe and Tedeschi, Gabriele},
  title =	{{Effect Semantics for Quantum Process Calculi}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{16:1--16:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.16},
  URN =		{urn:nbn:de:0030-drops-207886},
  doi =		{10.4230/LIPIcs.CONCUR.2024.16},
  annote =	{Keywords: Quantum process calculi, probabilistic LTSs, effect LTSs}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.20
Constraint Modelling with LLMs Using In-Context Learning

Authors: Kostis Michailidis, Dimos Tsouros, and Tias Guns

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Constraint Programming (CP) allows for the modelling and solving of a wide range of combinatorial problems. However, modelling such problems using constraints over decision variables still requires significant expertise, both in conceptual thinking and syntactic use of modelling languages. In this work, we explore the potential of using pre-trained Large Language Models (LLMs) as coding assistants, to transform textual problem descriptions into concrete and executable CP specifications. We present different transformation pipelines with explicit intermediate representations, and we investigate the potential benefit of various retrieval-augmented example selection strategies for in-context learning. We evaluate our approach on 2 datasets from the literature, namely NL4Opt (optimisation) and Logic Grid Puzzles (satisfaction), and a heterogeneous set of exercises from a CP course. The results show that pre-trained LLMs have promising potential for initialising the modelling process, with retrieval-augmented in-context learning significantly enhancing their modelling capabilities.
Cite as

Kostis Michailidis, Dimos Tsouros, and Tias Guns. Constraint Modelling with LLMs Using In-Context Learning. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 20:1-20:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{michailidis_et_al:LIPIcs.CP.2024.20,
  author =	{Michailidis, Kostis and Tsouros, Dimos and Guns, Tias},
  title =	{{Constraint Modelling with LLMs Using In-Context Learning}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{20:1--20:27},
  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.20},
  URN =		{urn:nbn:de:0030-drops-207053},
  doi =		{10.4230/LIPIcs.CP.2024.20},
  annote =	{Keywords: Constraint Modelling, Constraint Acquisition, Constraint Programming, Large Language Models, In-Context Learning, Natural Language Processing, Named Entity Recognition, Retrieval-Augmented Generation, Optimisation}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.22
Learning Lagrangian Multipliers for the Travelling Salesman Problem

Authors: Augustin Parjadis, Quentin Cappart, Bistra Dilkina, Aaron Ferber, and Louis-Martin Rousseau

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Lagrangian relaxation is a versatile mathematical technique employed to relax constraints in an optimization problem, enabling the generation of dual bounds to prove the optimality of feasible solutions and the design of efficient propagators in constraint programming (such as the weighted circuit constraint). However, the conventional process of deriving Lagrangian multipliers (e.g., using subgradient methods) is often computationally intensive, limiting its practicality for large-scale or time-sensitive problems. To address this challenge, we propose an innovative unsupervised learning approach that harnesses the capabilities of graph neural networks to exploit the problem structure, aiming to generate accurate Lagrangian multipliers efficiently. We apply this technique to the well-known Held-Karp Lagrangian relaxation for the traveling salesman problem. The core idea is to predict accurate Lagrangian multipliers and to employ them as a warm start for generating Held-Karp relaxation bounds. These bounds are subsequently utilized to enhance the filtering process carried out by branch-and-bound algorithms. In contrast to much of the existing literature, which primarily focuses on finding feasible solutions, our approach operates on the dual side, demonstrating that learning can also accelerate the proof of optimality. We conduct experiments across various distributions of the metric traveling salesman problem, considering instances with up to 200 cities. The results illustrate that our approach can improve the filtering level of the weighted circuit global constraint, reduce the optimality gap by a factor two for unsolved instances up to a timeout, and reduce the execution time for solved instances by 10%.
Cite as

Augustin Parjadis, Quentin Cappart, Bistra Dilkina, Aaron Ferber, and Louis-Martin Rousseau. Learning Lagrangian Multipliers for the Travelling Salesman Problem. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{parjadis_et_al:LIPIcs.CP.2024.22,
  author =	{Parjadis, Augustin and Cappart, Quentin and Dilkina, Bistra and Ferber, Aaron and Rousseau, Louis-Martin},
  title =	{{Learning Lagrangian Multipliers for the Travelling Salesman Problem}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{22:1--22:18},
  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.22},
  URN =		{urn:nbn:de:0030-drops-207076},
  doi =		{10.4230/LIPIcs.CP.2024.22},
  annote =	{Keywords: Lagrangian relaxation, unsupervised learning, graph neural network}
}
Document
DOI: 10.4230/LIPIcs.WABI.2024.18
RNA Triplet Repeats: Improved Algorithms for Structure Prediction and Interactions

Authors: Kimon Boehmer, Sarah J. Berkemer, Sebastian Will, and Yann Ponty

Published in: LIPIcs, Volume 312, 24th International Workshop on Algorithms in Bioinformatics (WABI 2024)

Abstract
RNAs composed of Triplet Repeats (TR) have recently attracted much attention in the field of synthetic biology. We study the mimimum free energy (MFE) secondary structures of such RNAs and give improved algorithms to compute the MFE and the partition function. Furthermore, we study the interaction of multiple RNAs and design a new algorithm for computing MFE and partition function for RNA-RNA interactions, improving the previously known factorial running time to exponential. In the case of TR, we show computational hardness but still obtain a parameterized algorithm. Finally, we propose a polynomial-time algorithm for computing interactions from a base set of RNA strands and conduct experiments on the interaction of TR based on this algorithm. For instance, we study the probability that a base pair is formed between two strands with the same triplet pattern, allowing an assessment of a notion of orthogonality between TR.
Cite as

Kimon Boehmer, Sarah J. Berkemer, Sebastian Will, and Yann Ponty. RNA Triplet Repeats: Improved Algorithms for Structure Prediction and Interactions. In 24th International Workshop on Algorithms in Bioinformatics (WABI 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 312, pp. 18:1-18:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{boehmer_et_al:LIPIcs.WABI.2024.18,
  author =	{Boehmer, Kimon and Berkemer, Sarah J. and Will, Sebastian and Ponty, Yann},
  title =	{{RNA Triplet Repeats: Improved Algorithms for Structure Prediction and Interactions}},
  booktitle =	{24th International Workshop on Algorithms in Bioinformatics (WABI 2024)},
  pages =	{18:1--18:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-340-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{312},
  editor =	{Pissis, Solon P. and Sung, Wing-Kin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WABI.2024.18},
  URN =		{urn:nbn:de:0030-drops-206625},
  doi =		{10.4230/LIPIcs.WABI.2024.18},
  annote =	{Keywords: RNA folding, RNA interactions, triplet repeats, dynamic programming, NP-hardness}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2024.55
Minimal Obstructions to C₅-Coloring in Hereditary Graph Classes

Authors: Jan Goedgebeur, Jorik Jooken, Karolina Okrasa, Paweł Rzążewski, and Oliver Schaudt

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
For graphs G and H, an H-coloring of G is an edge-preserving mapping from V(G) to V(H). Note that if H is the triangle, then H-colorings are equivalent to 3-colorings. In this paper we are interested in the case that H is the five-vertex cycle C₅. A minimal obstruction to C₅-coloring is a graph that does not have a C₅-coloring, but every proper induced subgraph thereof has a C₅-coloring. In this paper we are interested in minimal obstructions to C₅-coloring in F-free graphs, i.e., graphs that exclude some fixed graph F as an induced subgraph. Let P_t denote the path on t vertices, and let S_{a,b,c} denote the graph obtained from paths P_{a+1},P_{b+1},P_{c+1} by identifying one of their endvertices. We show that there is only a finite number of minimal obstructions to C₅-coloring among F-free graphs, where F ∈ {P₈, S_{2,2,1}, S_{3,1,1}} and explicitly determine all such obstructions. This extends the results of Kamiński and Pstrucha [Discr. Appl. Math. 261, 2019] who proved that there is only a finite number of P₇-free minimal obstructions to C₅-coloring, and of Dębski et al. [ISAAC 2022 Proc.] who showed that the triangle is the unique S_{2,1,1}-free minimal obstruction to C₅-coloring. We complement our results with a construction of an infinite family of minimal obstructions to C₅-coloring, which are simultaneously P_{13}-free and S_{2,2,2}-free. We also discuss infinite families of F-free minimal obstructions to H-coloring for other graphs H.
Cite as

Jan Goedgebeur, Jorik Jooken, Karolina Okrasa, Paweł Rzążewski, and Oliver Schaudt. Minimal Obstructions to C₅-Coloring in Hereditary Graph Classes. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 55:1-55:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{goedgebeur_et_al:LIPIcs.MFCS.2024.55,
  author =	{Goedgebeur, Jan and Jooken, Jorik and Okrasa, Karolina and Rz\k{a}\.{z}ewski, Pawe{\l} and Schaudt, Oliver},
  title =	{{Minimal Obstructions to C₅-Coloring in Hereditary Graph Classes}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{55:1--55:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.55},
  URN =		{urn:nbn:de:0030-drops-206110},
  doi =		{10.4230/LIPIcs.MFCS.2024.55},
  annote =	{Keywords: graph homomorphism, critical graphs, hereditary graph classes}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2024.63
Fully-Adaptive Dynamic Connectivity of Square Intersection Graphs

Authors: Ivor van der Hoog, André Nusser, Eva Rotenberg, and Frank Staals

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract
A classical problem in computational geometry and graph algorithms is: given a dynamic set 𝒮 of geometric shapes in the plane, efficiently maintain the connectivity of the intersection graph of 𝒮. Previous papers studied the setting where, before the updates, the data structure receives some parameter P. Then, updates could insert and delete disks as long as at all times the disks have a diameter that lies in a fixed range [1/P, 1]. As a consequence of that prerequisite, the aspect ratio ψ (i.e. the ratio between the largest and smallest diameter) of the disks would at all times satisfy ψ ≤ P. The state-of-the-art for storing disks in a dynamic connectivity data structure is a data structure that uses O(Pn) space and that has amortized O(P log⁴ n) expected amortized update time. Connectivity queries between disks are supported in O(log n / log log n) time. In the dynamic setting, one wishes for a more flexible data structure in which disks of any diameter may arrive and leave, independent of their diameter, changing the aspect ratio freely. Ideally, the aspect ratio should merely be part of the analysis. We restrict our attention to axis-aligned squares, and study fully-dynamic square intersection graph connectivity. Our result is fully-adaptive to the aspect ratio, spending time proportional to the current aspect ratio ψ, as opposed to some previously given maximum P. Our focus on squares allows us to simplify and streamline the connectivity pipeline from previous work. When n is the number of squares and ψ is the aspect ratio after insertion (or before deletion), our data structure answers connectivity queries in O(log n / log log n) time. We can update connectivity information in O(ψ log⁴ n + log⁶ n) amortized time. We also improve space usage from O(P ⋅ n log n) to O(n log³ n log ψ) - while generalizing to a fully-adaptive aspect ratio - which yields a space usage that is near-linear in n for any polynomially bounded ψ.
Cite as

Ivor van der Hoog, André Nusser, Eva Rotenberg, and Frank Staals. Fully-Adaptive Dynamic Connectivity of Square Intersection Graphs. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 63:1-63:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{vanderhoog_et_al:LIPIcs.MFCS.2024.63,
  author =	{van der Hoog, Ivor and Nusser, Andr\'{e} and Rotenberg, Eva and Staals, Frank},
  title =	{{Fully-Adaptive Dynamic Connectivity of Square Intersection Graphs}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{63:1--63:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.63},
  URN =		{urn:nbn:de:0030-drops-206197},
  doi =		{10.4230/LIPIcs.MFCS.2024.63},
  annote =	{Keywords: Computational geometry, planar geometry, data structures, geometric intersection graphs, fully-dynamic algorithms}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.28
Strategy Extraction by Interpolation

Authors: Friedrich Slivovsky

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
In applications, QBF solvers are often required to generate strategies. This typically involves a process known as strategy extraction, where a Boolean circuit encoding a strategy is computed from a proof. It has previously been observed that Craig interpolation in propositional logic can be seen as a special case of QBF strategy extraction. In this paper we explore this connection further and show that, conversely, any strategy for a false QBF corresponds to a sequence of interpolants in its complete (Herbrand) expansion. Inspired by this correspondence, we present a new strategy extraction algorithm for the expansion-based proof system Exp+Res. Its asymptotic running time matches the best known bound of O(mn) for a proof with m lines and n universally quantified variables. We report on experiments comparing this algorithm with a strategy extraction algorithm based on combining partial strategies, as well as with round-based strategy extraction.
Cite as

Friedrich Slivovsky. Strategy Extraction by Interpolation. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{slivovsky:LIPIcs.SAT.2024.28,
  author =	{Slivovsky, Friedrich},
  title =	{{Strategy Extraction by Interpolation}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{28:1--28:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.28},
  URN =		{urn:nbn:de:0030-drops-205509},
  doi =		{10.4230/LIPIcs.SAT.2024.28},
  annote =	{Keywords: QBF, Expansion, Strategy Extraction, Interpolation}
}
Document
Invited Paper
DOI: 10.4230/OASIcs.WCET.2024.5
Invited Paper: On the Granularity of Bandwidth Regulation in FPGA-Based Heterogeneous Systems on Chip

Authors: Gianluca Brilli, Giacomo Valente, Alessandro Capotondi, Tania Di Mascio, and Andrea Marongiu

Published in: OASIcs, Volume 121, 22nd International Workshop on Worst-Case Execution Time Analysis (WCET 2024)

Abstract
Main memory sharing in commercial, FPGA-based Heterogeneous System on Chips (HeSoCs) can cause significant interference, and ultimately severe slowdown of the executing workload, which bars the adoption of such systems in the context of time-critical applications. Bandwidth regulation approaches based on monitoring and throttling are widely adopted also in commercial hardware to improve the system quality of service (QoS), and previous work has shown that the finer the granularity of the mechanism, the more effective the QoS control. Different mechanisms, however, might exploit more or less effectively the available residual memory bandwidth, provided that the QoS requirement is satisfied. In this paper we present an exhaustive experimental evaluation of how three bandwidth regulation mechanisms with coarse, fine and ultra-fine granularity compare in terms of exploitation of the system memory bandwidth. Our results show that a very fine-grained regulation mechanism might experience worse system-level memory bandwidth exploitation compared to a coarser-grained approach.
Cite as

Gianluca Brilli, Giacomo Valente, Alessandro Capotondi, Tania Di Mascio, and Andrea Marongiu. Invited Paper: On the Granularity of Bandwidth Regulation in FPGA-Based Heterogeneous Systems on Chip. In 22nd International Workshop on Worst-Case Execution Time Analysis (WCET 2024). Open Access Series in Informatics (OASIcs), Volume 121, pp. 5:1-5:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{brilli_et_al:OASIcs.WCET.2024.5,
  author =	{Brilli, Gianluca and Valente, Giacomo and Capotondi, Alessandro and Di Mascio, Tania and Marongiu, Andrea},
  title =	{{Invited Paper: On the Granularity of Bandwidth Regulation in FPGA-Based Heterogeneous Systems on Chip}},
  booktitle =	{22nd International Workshop on Worst-Case Execution Time Analysis (WCET 2024)},
  pages =	{5:1--5:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-346-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{121},
  editor =	{Carle, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2024.5},
  URN =		{urn:nbn:de:0030-drops-204732},
  doi =		{10.4230/OASIcs.WCET.2024.5},
  annote =	{Keywords: Bandwidth Regulation, System-on-Chip, FPGA}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2024.4
Tighter Worst-Case Response Time Bounds for Jitter-Based Self-Suspension Analysis

Authors: Mario Günzel, Georg von der Brüggen, and Jian-Jia Chen

Published in: LIPIcs, Volume 298, 36th Euromicro Conference on Real-Time Systems (ECRTS 2024)

Abstract
Tasks are called self-suspending if they can yield their ready state (specifically, releasing the processor while having highest priority) despite being incomplete, for instance, to offload computation to an external device or when waiting on access rights for shared resources or data. This self-suspending behavior requires special treatment when applying analytical results to compute worst-case response time bounds. One typical treatment is modeling self-suspension as release jitter in a so-called jitter-based analysis. The state of the art, when considering task-level fixed-priority scheduling, individually quantifies the jitter term of each higher-priority task by its worst-case response time minus its worst-case execution time. This work tightens the jitter term by taking the execution behavior of the other higher-priority tasks into account. Our improved jitter-based analysis analytically dominates the previous jitter-based analysis. Moreover, an evaluation for synthetically generated sporadic tasks demonstrates that this jitter term results in tighter worst-case response time bounds for self-suspending tasks. We observe an improvement for up to 55.89 % of the tasksets compared to the previous jitter-based analysis.
Cite as

Mario Günzel, Georg von der Brüggen, and Jian-Jia Chen. Tighter Worst-Case Response Time Bounds for Jitter-Based Self-Suspension Analysis. In 36th Euromicro Conference on Real-Time Systems (ECRTS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 298, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{gunzel_et_al:LIPIcs.ECRTS.2024.4,
  author =	{G\"{u}nzel, Mario and von der Br\"{u}ggen, Georg and Chen, Jian-Jia},
  title =	{{Tighter Worst-Case Response Time Bounds for Jitter-Based Self-Suspension Analysis}},
  booktitle =	{36th Euromicro Conference on Real-Time Systems (ECRTS 2024)},
  pages =	{4:1--4:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-324-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{298},
  editor =	{Pellizzoni, Rodolfo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2024.4},
  URN =		{urn:nbn:de:0030-drops-203074},
  doi =		{10.4230/LIPIcs.ECRTS.2024.4},
  annote =	{Keywords: Worst-Case Response Time, WCRT, Jitter, Self-Suspension, Analysis}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2024.6
Optimizing Per-Core Priorities to Minimize End-To-End Latencies

Authors: Francesco Paladino, Alessandro Biondi, Enrico Bini, and Paolo Pazzaglia

Published in: LIPIcs, Volume 298, 36th Euromicro Conference on Real-Time Systems (ECRTS 2024)

Abstract
Logical Execution Time (LET) allows decoupling the schedule of real-time periodic tasks from their communication, with the advantage of isolating the communication pattern from the variability of the schedule. However, when such tasks are organized in chains, the usage of LET at the task level does not necessarily transfer the same LET properties to the chain level. In this paper, we extend a LET-like model from tasks to chains spanning over multiple cores. We leverage the designed constant latency chains to optimize per-core priority assignment. Finally, we also provide a set of heuristic algorithms, that are compared in a large-scale experimental evaluation.
Cite as

Francesco Paladino, Alessandro Biondi, Enrico Bini, and Paolo Pazzaglia. Optimizing Per-Core Priorities to Minimize End-To-End Latencies. In 36th Euromicro Conference on Real-Time Systems (ECRTS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 298, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{paladino_et_al:LIPIcs.ECRTS.2024.6,
  author =	{Paladino, Francesco and Biondi, Alessandro and Bini, Enrico and Pazzaglia, Paolo},
  title =	{{Optimizing Per-Core Priorities to Minimize End-To-End Latencies}},
  booktitle =	{36th Euromicro Conference on Real-Time Systems (ECRTS 2024)},
  pages =	{6:1--6:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-324-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{298},
  editor =	{Pellizzoni, Rodolfo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2024.6},
  URN =		{urn:nbn:de:0030-drops-203094},
  doi =		{10.4230/LIPIcs.ECRTS.2024.6},
  annote =	{Keywords: Cause-Effect Chains, Logical Execution Time, End-to-End Latency, Design Optimization, Task Priorities, Data Age, Reaction Time}
}
  • Refine by Author
  • 3 Chen, Jian-Jia
  • 2 Huang, Wen-Hung
  • 2 Rzążewski, Paweł
  • 2 von der Brüggen, Georg
  • 1 Anand, Emile
  • Show More...

  • Refine by Classification
  • 4 Computer systems organization → Real-time systems
  • 3 Software and its engineering → Real-time schedulability
  • 3 Theory of computation → Computational geometry
  • 2 Computer systems organization → Embedded and cyber-physical systems
  • 2 Computer systems organization → Embedded systems
  • Show More...

  • Refine by Keyword
  • 2 Large Language Models
  • 2 Real-time systems
  • 1 Analysis
  • 1 Applications of logics
  • 1 Approximate Selection
  • Show More...

  • Refine by Type
  • 27 document

  • Refine by Publication Year
  • 23 2024
  • 2 2018
  • 1 2017
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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