79 Search Results for "An, Hyung-Chan"

Document
DOI: 10.4230/LIPIcs.STACS.2024.16
Gapped String Indexing in Subquadratic Space and Sublinear Query Time

Authors: Philip Bille, Inge Li Gørtz, Moshe Lewenstein, Solon P. Pissis, Eva Rotenberg, and Teresa Anna Steiner

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
In Gapped String Indexing, the goal is to compactly represent a string S of length n such that for any query consisting of two strings P₁ and P₂, called patterns, and an integer interval [α, β], called gap range, we can quickly find occurrences of P₁ and P₂ in S with distance in [α, β]. Gapped String Indexing is a central problem in computational biology and text mining and has thus received significant research interest, including parameterized and heuristic approaches. Despite this interest, the best-known time-space trade-offs for Gapped String Indexing are the straightforward 𝒪(n) space and 𝒪(n+ occ) query time or Ω(n²) space and Õ(|P₁| + |P₂| + occ) query time. We break through this barrier obtaining the first interesting trade-offs with polynomially subquadratic space and polynomially sublinear query time. In particular, we show that, for every 0 ≤ δ ≤ 1, there is a data structure for Gapped String Indexing with either Õ(n^{2-δ/3}) or Õ(n^{3-2δ}) space and Õ(|P₁| + |P₂| + n^{δ}⋅ (occ+1)) query time, where occ is the number of reported occurrences. As a new fundamental tool towards obtaining our main result, we introduce the Shifted Set Intersection problem: preprocess a collection of sets S₁, …, S_k of integers such that for any query consisting of three integers i,j,s, we can quickly output YES if and only if there exist a ∈ S_i and b ∈ S_j with a+s = b. We start by showing that the Shifted Set Intersection problem is equivalent to the indexing variant of 3SUM (3SUM Indexing) [Golovnev et al., STOC 2020]. We then give a data structure for Shifted Set Intersection with gaps, which entails a solution to the Gapped String Indexing problem. Furthermore, we enhance our data structure for deciding Shifted Set Intersection, so that we can support the reporting variant of the problem, i.e., outputting all certificates in the affirmative case. Via the obtained equivalence to 3SUM Indexing, we thus give new improved data structures for the reporting variant of 3SUM Indexing, and we show how this improves upon the state-of-the-art solution for Jumbled Indexing [Chan and Lewenstein, STOC 2015] for any alphabet of constant size σ > 5.
Cite as

Philip Bille, Inge Li Gørtz, Moshe Lewenstein, Solon P. Pissis, Eva Rotenberg, and Teresa Anna Steiner. Gapped String Indexing in Subquadratic Space and Sublinear Query Time. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 16:1-16:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bille_et_al:LIPIcs.STACS.2024.16,
  author =	{Bille, Philip and G{\o}rtz, Inge Li and Lewenstein, Moshe and Pissis, Solon P. and Rotenberg, Eva and Steiner, Teresa Anna},
  title =	{{Gapped String Indexing in Subquadratic Space and Sublinear Query Time}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{16:1--16:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.16},
  URN =		{urn:nbn:de:0030-drops-197262},
  doi =		{10.4230/LIPIcs.STACS.2024.16},
  annote =	{Keywords: data structures, string indexing, indexing with gaps, two patterns}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2024.103
Advanced Composition Theorems for Differential Obliviousness

Authors: Mingxun Zhou, Mengshi Zhao, T-H. Hubert Chan, and Elaine Shi

Published in: LIPIcs, Volume 287, 15th Innovations in Theoretical Computer Science Conference (ITCS 2024)

Abstract
Differential obliviousness (DO) is a privacy notion which mandates that the access patterns of a program satisfy differential privacy. Earlier works have shown that in numerous applications, differential obliviousness allows us to circumvent fundamental barriers pertaining to fully oblivious algorithms, resulting in asymptotical (and sometimes even polynomial) performance improvements. Although DO has been applied to various contexts, including the design of algorithms, data structures, and protocols, its compositional properties are not explored until the recent work of Zhou et al. (Eurocrypt'23). Specifically, Zhou et al. showed that the original DO notion is not composable. They then proposed a refinement of DO called neighbor-preserving differential obliviousness (NPDO), and proved a basic composition for NPDO. In Zhou et al.’s basic composition theorem for NPDO, the privacy loss is linear in k for k-fold composition. In comparison, for standard differential privacy, we can enjoy roughly √k loss for k-fold composition by applying the well-known advanced composition theorem given an appropriate parameter range. Therefore, a natural question left open by their work is whether we can also prove an analogous advanced composition for NPDO. In this paper, we answer this question affirmatively. As a key step in proving an advanced composition theorem for NPDO, we define a more operational notion called symmetric NPDO which we prove to be equivalent to NPDO. Using symmetric NPDO as a stepping stone, we also show how to generalize NPDO to more general notions of divergence, resulting in Rényi-NPDO, zero-concentrated-NPDO, Gassian-NPDO, and g-NPDO notions. We also prove composition theorems for these generalized notions of NPDO.
Cite as

Mingxun Zhou, Mengshi Zhao, T-H. Hubert Chan, and Elaine Shi. Advanced Composition Theorems for Differential Obliviousness. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 103:1-103:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{zhou_et_al:LIPIcs.ITCS.2024.103,
  author =	{Zhou, Mingxun and Zhao, Mengshi and Chan, T-H. Hubert and Shi, Elaine},
  title =	{{Advanced Composition Theorems for Differential Obliviousness}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{103:1--103:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-309-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{287},
  editor =	{Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.103},
  URN =		{urn:nbn:de:0030-drops-196315},
  doi =		{10.4230/LIPIcs.ITCS.2024.103},
  annote =	{Keywords: Differential Privacy, Oblivious Algorithms}
}
Document
DOI: 10.4230/LIPIcs.DISC.2023.28
Quorum Subsumption for Heterogeneous Quorum Systems

Authors: Xiao Li, Eric Chan, and Mohsen Lesani

Published in: LIPIcs, Volume 281, 37th International Symposium on Distributed Computing (DISC 2023)

Abstract
Byzantine quorum systems provide higher throughput than proof-of-work and incur modest energy consumption. Further, their modern incarnations incorporate personalized and heterogeneous trust. Thus, they are emerging as an appealing candidate for global financial infrastructure. However, since their quorums are not uniform across processes anymore, the properties that they should maintain to support abstractions such as reliable broadcast and consensus are not well-understood. It has been shown that the two properties quorum intersection and availability are necessary. In this paper, we prove that they are not sufficient. We then define the notion of quorum subsumption, and show that the three conditions together are sufficient: we present reliable broadcast and consensus protocols, and prove their correctness for quorum systems that provide the three properties.
Cite as

Xiao Li, Eric Chan, and Mohsen Lesani. Quorum Subsumption for Heterogeneous Quorum Systems. In 37th International Symposium on Distributed Computing (DISC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 281, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.DISC.2023.28,
  author =	{Li, Xiao and Chan, Eric and Lesani, Mohsen},
  title =	{{Quorum Subsumption for Heterogeneous Quorum Systems}},
  booktitle =	{37th International Symposium on Distributed Computing (DISC 2023)},
  pages =	{28:1--28:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-301-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{281},
  editor =	{Oshman, Rotem},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2023.28},
  URN =		{urn:nbn:de:0030-drops-191541},
  doi =		{10.4230/LIPIcs.DISC.2023.28},
  annote =	{Keywords: Distributed Systems, Impossibility Results, Byzantine fault tolerance}
}
Document
DOI: 10.4230/LIPIcs.CP.2023.32
Assembly Line Preliminary Design Optimization for an Aircraft

Authors: Stéphanie Roussel, Thomas Polacsek, and Anouck Chan

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract
In the aeronautics industry, each aircraft family has a dedicated manufacturing system. This system is classically designed once the aircraft design is completely finished, which might lead to poor performance. To mitigate this issue, a strategy is to take into account the production system as early as possible in the aircraft design process. In this work, we define the Assembly Line Preliminary Design Problem, which consists in defining, for a given aircraft design, the best assembly line layout and the type and number of machines equipping each workstation. We propose a Constraint Programming encoding for that problem, along with an algorithm based on epsilon constraint for exploring the set of Pareto solutions. We present experiments run on a set of real industrial data. The results show that the approach is promising and offers support to experts in order to compare aircraft designs with each other.
Cite as

Stéphanie Roussel, Thomas Polacsek, and Anouck Chan. Assembly Line Preliminary Design Optimization for an Aircraft. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{roussel_et_al:LIPIcs.CP.2023.32,
  author =	{Roussel, St\'{e}phanie and Polacsek, Thomas and Chan, Anouck},
  title =	{{Assembly Line Preliminary Design Optimization for an Aircraft}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{32:1--32:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.32},
  URN =		{urn:nbn:de:0030-drops-190690},
  doi =		{10.4230/LIPIcs.CP.2023.32},
  annote =	{Keywords: Assembly line design, Constraint Programming, Multi-objective, Industry 4.0}
}
Document
DOI: 10.4230/LIPIcs.SEA.2023.19
Exact and Approximate Range Mode Query Data Structures in Practice

Authors: Meng He and Zhen Liu

Published in: LIPIcs, Volume 265, 21st International Symposium on Experimental Algorithms (SEA 2023)

Abstract
We conduct an experimental study on the range mode problem. In the exact version of the problem, we preprocess an array A, such that given a query range [a, b], the most frequent element in A[a, b] can be found efficiently. For this problem, our most important finding is that the strategy of using succinct data structures to encode more precomputed information not only helped Chan et al. (Linear-space data structures for range mode query in arrays, Theory of Computing Systems, 2013) improve previous results in theory but also helps us achieve the best time/space tradeoff in practice; we even go a step further to replace more components in their solution with succinct data structures and improve the performance further. In the approximate version of this problem, a (1+ε)-approximate range mode query looks for an element whose occurrences in A[a,b] is at least F_{a,b}/(1+ε), where F_{a,b} is the frequency of the mode in A[a,b]. We implement all previous solutions to this problems and find that, even when ε = 1/2, the average approximation ratio of these solutions is close to 1 in practice, and they provide much faster query time than the best exact solution. These solutions achieve different useful time-space tradeoffs, and among them, El-Zein et al. (On Approximate Range Mode and Range Selection, 30th International Symposium on Algorithms and Computation, 2019) provide us with one solution whose space usage is only 35.6% to 93.8% of the cost of storing the input array of 32-bit integers (in most cases, the space cost is closer to the lower end, and the average space cost is 20.2 bits per symbol among all datasets). Its non-succinct version also stands out with query support at least several times faster than other O(n/ε)-word structures while using only slightly more space in practice.
Cite as

Meng He and Zhen Liu. Exact and Approximate Range Mode Query Data Structures in Practice. In 21st International Symposium on Experimental Algorithms (SEA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 265, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{he_et_al:LIPIcs.SEA.2023.19,
  author =	{He, Meng and Liu, Zhen},
  title =	{{Exact and Approximate Range Mode Query Data Structures in Practice}},
  booktitle =	{21st International Symposium on Experimental Algorithms (SEA 2023)},
  pages =	{19:1--19:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-279-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{265},
  editor =	{Georgiadis, Loukas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2023.19},
  URN =		{urn:nbn:de:0030-drops-183693},
  doi =		{10.4230/LIPIcs.SEA.2023.19},
  annote =	{Keywords: range mode query, exact range mode query, approximate range mode query}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2023.34
On the Fine-Grained Complexity of Small-Size Geometric Set Cover and Discrete k-Center for Small k

Authors: Timothy M. Chan, Qizheng He, and Yuancheng Yu

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
We study the time complexity of the discrete k-center problem and related (exact) geometric set cover problems when k or the size of the cover is small. We obtain a plethora of new results: - We give the first subquadratic algorithm for rectilinear discrete 3-center in 2D, running in Õ(n^{3/2}) time. - We prove a lower bound of Ω(n^{4/3-δ}) for rectilinear discrete 3-center in 4D, for any constant δ > 0, under a standard hypothesis about triangle detection in sparse graphs. - Given n points and n weighted axis-aligned unit squares in 2D, we give the first subquadratic algorithm for finding a minimum-weight cover of the points by 3 unit squares, running in Õ(n^{8/5}) time. We also prove a lower bound of Ω(n^{3/2-δ}) for the same problem in 2D, under the well-known APSP Hypothesis. For arbitrary axis-aligned rectangles in 2D, our upper bound is Õ(n^{7/4}). - We prove a lower bound of Ω(n^{2-δ}) for Euclidean discrete 2-center in 13D, under the Hyperclique Hypothesis. This lower bound nearly matches the straightforward upper bound of Õ(n^ω), if the matrix multiplication exponent ω is equal to 2. - We similarly prove an Ω(n^{k-δ}) lower bound for Euclidean discrete k-center in O(k) dimensions for any constant k ≥ 3, under the Hyperclique Hypothesis. This lower bound again nearly matches known upper bounds if ω = 2. - We also prove an Ω(n^{2-δ}) lower bound for the problem of finding 2 boxes to cover the largest number of points, given n points and n boxes in 12D . This matches the straightforward near-quadratic upper bound.
Cite as

Timothy M. Chan, Qizheng He, and Yuancheng Yu. On the Fine-Grained Complexity of Small-Size Geometric Set Cover and Discrete k-Center for Small k. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 34:1-34:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chan_et_al:LIPIcs.ICALP.2023.34,
  author =	{Chan, Timothy M. and He, Qizheng and Yu, Yuancheng},
  title =	{{On the Fine-Grained Complexity of Small-Size Geometric Set Cover and Discrete k-Center for Small k}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{34:1--34:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel 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.2023.34},
  URN =		{urn:nbn:de:0030-drops-180868},
  doi =		{10.4230/LIPIcs.ICALP.2023.34},
  annote =	{Keywords: Geometric set cover, discrete k-center, conditional lower bounds}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2023.23
Constant-Hop Spanners for More Geometric Intersection Graphs, with Even Smaller Size

Authors: Timothy M. Chan and Zhengcheng Huang

Published in: LIPIcs, Volume 258, 39th International Symposium on Computational Geometry (SoCG 2023)

Abstract
In SoCG 2022, Conroy and Tóth presented several constructions of sparse, low-hop spanners in geometric intersection graphs, including an O(nlog n)-size 3-hop spanner for n disks (or fat convex objects) in the plane, and an O(nlog² n)-size 3-hop spanner for n axis-aligned rectangles in the plane. Their work left open two major questions: (i) can the size be made closer to linear by allowing larger constant stretch? and (ii) can near-linear size be achieved for more general classes of intersection graphs? We address both questions simultaneously, by presenting new constructions of constant-hop spanners that have almost linear size and that hold for a much larger class of intersection graphs. More precisely, we prove the existence of an O(1)-hop spanner for arbitrary string graphs with O(nα_k(n)) size for any constant k, where α_k(n) denotes the k-th function in the inverse Ackermann hierarchy. We similarly prove the existence of an O(1)-hop spanner for intersection graphs of d-dimensional fat objects with O(nα_k(n)) size for any constant k and d. We also improve on some of Conroy and Tóth’s specific previous results, in either the number of hops or the size: we describe an O(nlog n)-size 2-hop spanner for disks (or more generally objects with linear union complexity) in the plane, and an O(nlog n)-size 3-hop spanner for axis-aligned rectangles in the plane. Our proofs are all simple, using separator theorems, recursion, shifted quadtrees, and shallow cuttings.
Cite as

Timothy M. Chan and Zhengcheng Huang. Constant-Hop Spanners for More Geometric Intersection Graphs, with Even Smaller Size. In 39th International Symposium on Computational Geometry (SoCG 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 258, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chan_et_al:LIPIcs.SoCG.2023.23,
  author =	{Chan, Timothy M. and Huang, Zhengcheng},
  title =	{{Constant-Hop Spanners for More Geometric Intersection Graphs, with Even Smaller Size}},
  booktitle =	{39th International Symposium on Computational Geometry (SoCG 2023)},
  pages =	{23:1--23:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-273-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{258},
  editor =	{Chambers, Erin W. and Gudmundsson, Joachim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2023.23},
  URN =		{urn:nbn:de:0030-drops-178738},
  doi =		{10.4230/LIPIcs.SoCG.2023.23},
  annote =	{Keywords: Hop spanners, geometric intersection graphs, string graphs, fat objects, separators, shallow cuttings}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2023.33
Labeled Nearest Neighbor Search and Metric Spanners via Locality Sensitive Orderings

Authors: Arnold Filtser

Published in: LIPIcs, Volume 258, 39th International Symposium on Computational Geometry (SoCG 2023)

Abstract
Chan, Har-Peled, and Jones [SICOMP 2020] developed locality-sensitive orderings (LSO) for Euclidean space. A (τ,ρ)-LSO is a collection Σ of orderings such that for every x,y ∈ ℝ^d there is an ordering σ ∈ Σ, where all the points between x and y w.r.t. σ are in the ρ-neighborhood of either x or y. In essence, LSO allow one to reduce problems to the 1-dimensional line. Later, Filtser and Le [STOC 2022] developed LSO’s for doubling metrics, general metric spaces, and minor free graphs. For Euclidean and doubling spaces, the number of orderings in the LSO is exponential in the dimension, which made them mainly useful for the low dimensional regime. In this paper, we develop new LSO’s for Euclidean, 𝓁_p, and doubling spaces that allow us to trade larger stretch for a much smaller number of orderings. We then use our new LSO’s (as well as the previous ones) to construct path reporting low hop spanners, fault tolerant spanners, reliable spanners, and light spanners for different metric spaces. While many nearest neighbor search (NNS) data structures were constructed for metric spaces with implicit distance representations (where the distance between two metric points can be computed using their names, e.g. Euclidean space), for other spaces almost nothing is known. In this paper we initiate the study of the labeled NNS problem, where one is allowed to artificially assign labels (short names) to metric points. We use LSO’s to construct efficient labeled NNS data structures in this model.
Cite as

Arnold Filtser. Labeled Nearest Neighbor Search and Metric Spanners via Locality Sensitive Orderings. In 39th International Symposium on Computational Geometry (SoCG 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 258, pp. 33:1-33:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{filtser:LIPIcs.SoCG.2023.33,
  author =	{Filtser, Arnold},
  title =	{{Labeled Nearest Neighbor Search and Metric Spanners via Locality Sensitive Orderings}},
  booktitle =	{39th International Symposium on Computational Geometry (SoCG 2023)},
  pages =	{33:1--33:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-273-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{258},
  editor =	{Chambers, Erin W. and Gudmundsson, Joachim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2023.33},
  URN =		{urn:nbn:de:0030-drops-178839},
  doi =		{10.4230/LIPIcs.SoCG.2023.33},
  annote =	{Keywords: Locality sensitive ordering, nearest neighbor search, high dimensional Euclidean space, doubling dimension, planar and minor free graphs, path reporting low hop spanner, fault tolerant spanner, reliable spanner, light spanner}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2023.46
Online and Dynamic Algorithms for Geometric Set Cover and Hitting Set

Authors: Arindam Khan, Aditya Lonkar, Saladi Rahul, Aditya Subramanian, and Andreas Wiese

Published in: LIPIcs, Volume 258, 39th International Symposium on Computational Geometry (SoCG 2023)

Abstract
Set cover and hitting set are fundamental problems in combinatorial optimization which are well-studied in the offline, online, and dynamic settings. We study the geometric versions of these problems and present new online and dynamic algorithms for them. In the online version of set cover (resp. hitting set), m sets (resp. n points) are given and n points (resp. m sets) arrive online, one-by-one. In the dynamic versions, points (resp. sets) can arrive as well as depart. Our goal is to maintain a set cover (resp. hitting set), minimizing the size of the computed solution. For online set cover for (axis-parallel) squares of arbitrary sizes, we present a tight O(log n)-competitive algorithm. In the same setting for hitting set, we provide a tight O(log N)-competitive algorithm, assuming that all points have integral coordinates in [0,N)². No online algorithm had been known for either of these settings, not even for unit squares (apart from the known online algorithms for arbitrary set systems). For both dynamic set cover and hitting set with d-dimensional hyperrectangles, we obtain (log m)^O(d)-approximation algorithms with (log m)^O(d) worst-case update time. This partially answers an open question posed by Chan et al. [SODA'22]. Previously, no dynamic algorithms with polylogarithmic update time were known even in the setting of squares (for either of these problems). Our main technical contributions are an extended quad-tree approach and a frequency reduction technique that reduces geometric set cover instances to instances of general set cover with bounded frequency.
Cite as

Arindam Khan, Aditya Lonkar, Saladi Rahul, Aditya Subramanian, and Andreas Wiese. Online and Dynamic Algorithms for Geometric Set Cover and Hitting Set. In 39th International Symposium on Computational Geometry (SoCG 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 258, pp. 46:1-46:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{khan_et_al:LIPIcs.SoCG.2023.46,
  author =	{Khan, Arindam and Lonkar, Aditya and Rahul, Saladi and Subramanian, Aditya and Wiese, Andreas},
  title =	{{Online and Dynamic Algorithms for Geometric Set Cover and Hitting Set}},
  booktitle =	{39th International Symposium on Computational Geometry (SoCG 2023)},
  pages =	{46:1--46:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-273-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{258},
  editor =	{Chambers, Erin W. and Gudmundsson, Joachim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2023.46},
  URN =		{urn:nbn:de:0030-drops-178967},
  doi =		{10.4230/LIPIcs.SoCG.2023.46},
  annote =	{Keywords: Geometric Set Cover, Hitting Set, Rectangles, Squares, Hyperrectangles, Online Algorithms, Dynamic Data Structures}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2023.47
Sparse Euclidean Spanners with Optimal Diameter: A General and Robust Lower Bound via a Concave Inverse-Ackermann Function

Authors: Hung Le, Lazar Milenković, and Shay Solomon

Published in: LIPIcs, Volume 258, 39th International Symposium on Computational Geometry (SoCG 2023)

Abstract
In STOC'95 [S. Arya et al., 1995] Arya et al. showed that any set of n points in ℝ^d admits a (1+ε)-spanner with hop-diameter at most 2 (respectively, 3) and O(n log n) edges (resp., O(n log log n) edges). They also gave a general upper bound tradeoff of hop-diameter k with O(n α_k(n)) edges, for any k ≥ 2. The function α_k is the inverse of a certain Ackermann-style function, where α₀(n) = ⌈n/2⌉, α₁(n) = ⌈√n⌉, α₂(n) = ⌈log n⌉, α₃(n) = ⌈log log n⌉, α₄(n) = log^* n, α₅(n) = ⌊ 1/2 log^*n ⌋, …. Roughly speaking, for k ≥ 2 the function α_{k} is close to ⌊(k-2)/2⌋-iterated log-star function, i.e., log with ⌊(k-2)/2⌋ stars. Despite a large body of work on spanners of bounded hop-diameter, the fundamental question of whether this tradeoff between size and hop-diameter of Euclidean (1+ε)-spanners is optimal has remained open, even in one-dimensional spaces. Three lower bound tradeoffs are known: - An optimal k versus Ω(n α_k(n)) by Alon and Schieber [N. Alon and B. Schieber, 1987], but it applies to stretch 1 (not 1+ε). - A suboptimal k versus Ω(nα_{2k+6}(n)) by Chan and Gupta [H. T.-H. Chan and A. Gupta, 2006]. - A suboptimal k versus Ω(n/(2^{6⌊k/2⌋}) α_k(n)) by Le et al. [Le et al., 2022]. This paper establishes the optimal k versus Ω(n α_k(n)) lower bound tradeoff for stretch 1+ε, for any ε > 0, and for any k. An important conceptual contribution of this work is in achieving optimality by shaving off an extremely slowly growing term, namely 2^{6⌊k/2⌋} for k ≤ O(α(n)); such a fine-grained optimization (that achieves optimality) is very rare in the literature. To shave off the 2^{6⌊k/2⌋} term from the previous bound of Le et al., our argument has to drill much deeper. In particular, we propose a new way of analyzing recurrences that involve inverse-Ackermann style functions, and our key technical contribution is in presenting the first explicit construction of concave versions of these functions. An important advantage of our approach over previous ones is its robustness: While all previous lower bounds are applicable only to restricted 1-dimensional point sets, ours applies even to random point sets in constant-dimensional spaces.
Cite as

Hung Le, Lazar Milenković, and Shay Solomon. Sparse Euclidean Spanners with Optimal Diameter: A General and Robust Lower Bound via a Concave Inverse-Ackermann Function. In 39th International Symposium on Computational Geometry (SoCG 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 258, pp. 47:1-47:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{le_et_al:LIPIcs.SoCG.2023.47,
  author =	{Le, Hung and Milenkovi\'{c}, Lazar and Solomon, Shay},
  title =	{{Sparse Euclidean Spanners with Optimal Diameter: A General and Robust Lower Bound via a Concave Inverse-Ackermann Function}},
  booktitle =	{39th International Symposium on Computational Geometry (SoCG 2023)},
  pages =	{47:1--47:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-273-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{258},
  editor =	{Chambers, Erin W. and Gudmundsson, Joachim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2023.47},
  URN =		{urn:nbn:de:0030-drops-178976},
  doi =		{10.4230/LIPIcs.SoCG.2023.47},
  annote =	{Keywords: Euclidean spanners, Ackermann functions, convex functions, hop-diameter}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2022.13
Inscribing or Circumscribing a Histogon to a Convex Polygon

Authors: Jaehoon Chung, Sang Won Bae, Chan-Su Shin, Sang Duk Yoon, and Hee-Kap Ahn

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

Abstract
We consider two optimization problems of approximating a convex polygon, one by a largest inscribed histogon and the other by a smallest circumscribed histogon. An axis-aligned histogon is an axis-aligned rectilinear polygon such that every horizontal edge has an integer length. A histogon of orientation θ is a copy of an axis-aligned histogon rotated by θ in counterclockwise direction. The goal is to find a largest inscribed histogon and a smallest circumscribed histogon over all orientations in [0,π). Depending on whether the horizontal width of a histogon is predetermined or not, we consider several different versions of the problem and present exact algorithms. These optimization problems belong to shape analysis, classification, and simplification, and they have applications in various cost-optimization problems.
Cite as

Jaehoon Chung, Sang Won Bae, Chan-Su Shin, Sang Duk Yoon, and Hee-Kap Ahn. Inscribing or Circumscribing a Histogon to a Convex Polygon. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{chung_et_al:LIPIcs.FSTTCS.2022.13,
  author =	{Chung, Jaehoon and Bae, Sang Won and Shin, Chan-Su and Yoon, Sang Duk and Ahn, Hee-Kap},
  title =	{{Inscribing or Circumscribing a Histogon to a Convex Polygon}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{13:1--13:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.13},
  URN =		{urn:nbn:de:0030-drops-174054},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.13},
  annote =	{Keywords: Shape simplification, Shape analysis, Histogon, Convex polygon}
}
Document
DOI: 10.4230/LIPIcs.ESA.2022.35
Approximate Circular Pattern Matching

Authors: Panagiotis Charalampopoulos, Tomasz Kociumaka, Jakub Radoszewski, Solon P. Pissis, Wojciech Rytter, Tomasz Waleń, and Wiktor Zuba

Published in: LIPIcs, Volume 244, 30th Annual European Symposium on Algorithms (ESA 2022)

Abstract
We investigate the complexity of approximate circular pattern matching (CPM, in short) under the Hamming and edit distance. Under each of these two basic metrics, we are given a length-n text T, a length-m pattern P, and a positive integer threshold k, and we are to report all starting positions (called occurrences) of fragments of T that are at distance at most k from some cyclic rotation of P. In the decision version of the problem, we are to check if there is any such occurrence. All previous results for approximate CPM were either average-case upper bounds or heuristics, with the exception of the work of Charalampopoulos et al. [CKP^+, JCSS'21], who considered only the Hamming distance. For the reporting version of the approximate CPM problem, under the Hamming distance we improve upon the main algorithm of [CKP^+, JCSS'21] from 𝒪(n+(n/m) ⋅ k⁴) to 𝒪(n+(n/m) ⋅ k³ log log k) time; for the edit distance, we give an 𝒪(nk²)-time algorithm. Notably, for the decision versions and wide parameter-ranges, we give algorithms whose complexities are almost identical to the state-of-the-art for standard (i.e., non-circular) approximate pattern matching: - For the decision version of the approximate CPM problem under the Hamming distance, we obtain an 𝒪(n+(n/m) ⋅ k² log k / log log k)-time algorithm, which works in 𝒪(n) time whenever k = 𝒪(√{m log log m / log m}). In comparison, the fastest algorithm for the standard counterpart of the problem, by Chan et al. [CGKKP, STOC’20], runs in 𝒪(n) time only for k = 𝒪(√m). We achieve this result via a reduction to a geometric problem by building on ideas from [CKP^+, JCSS'21] and Charalampopoulos et al. [CKW, FOCS'20]. - For the decision version of the approximate CPM problem under the edit distance, the 𝒪(nklog³ k) runtime of our algorithm near matches the 𝒪(nk) runtime of the Landau-Vishkin algorithm [LV, J. Algorithms'89] for approximate pattern matching under edit distance; the latter algorithm remains the fastest known for k = Ω(m^{2/5}). As a stepping stone, we propose an 𝒪(nklog³ k)-time algorithm for solving the Longest Prefix k'-Approximate Match problem, proposed by Landau et al. [LMS, SICOMP'98], for all k' ∈ {1,…,k}. Our algorithm is based on Tiskin’s theory of seaweeds [Tiskin, Math. Comput. Sci.'08], with recent advancements (see Charalampopoulos et al. [CKW, FOCS'22]), and on exploiting the seaweeds' relation to Monge matrices. In contrast, we obtain a conditional lower bound that suggests a polynomial separation between approximate CPM under the Hamming distance over the binary alphabet and its non-circular counterpart. We also show that a strongly subquadratic-time algorithm for the decision version of approximate CPM under edit distance would refute the Strong Exponential Time Hypothesis.
Cite as

Panagiotis Charalampopoulos, Tomasz Kociumaka, Jakub Radoszewski, Solon P. Pissis, Wojciech Rytter, Tomasz Waleń, and Wiktor Zuba. Approximate Circular Pattern Matching. In 30th Annual European Symposium on Algorithms (ESA 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 244, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{charalampopoulos_et_al:LIPIcs.ESA.2022.35,
  author =	{Charalampopoulos, Panagiotis and Kociumaka, Tomasz and Radoszewski, Jakub and Pissis, Solon P. and Rytter, Wojciech and Wale\'{n}, Tomasz and Zuba, Wiktor},
  title =	{{Approximate Circular Pattern Matching}},
  booktitle =	{30th Annual European Symposium on Algorithms (ESA 2022)},
  pages =	{35:1--35:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-247-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{244},
  editor =	{Chechik, Shiri and Navarro, Gonzalo and Rotenberg, Eva and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2022.35},
  URN =		{urn:nbn:de:0030-drops-169738},
  doi =		{10.4230/LIPIcs.ESA.2022.35},
  annote =	{Keywords: approximate circular pattern matching, Hamming distance, edit distance}
}
Document
DOI: 10.4230/LIPIcs.ESA.2022.39
Conditional Lower Bounds for Dynamic Geometric Measure Problems

Authors: Justin Dallant and John Iacono

Published in: LIPIcs, Volume 244, 30th Annual European Symposium on Algorithms (ESA 2022)

Abstract
We give new polynomial lower bounds for a number of dynamic measure problems in computational geometry. These lower bounds hold in the Word-RAM model, conditioned on the hardness of either 3SUM, APSP, or the Online Matrix-Vector Multiplication problem [Henzinger et al., STOC 2015]. In particular we get lower bounds in the incremental and fully-dynamic settings for counting maximal or extremal points in ℝ³, different variants of Klee’s Measure Problem, problems related to finding the largest empty disk in a set of points, and querying the size of the i'th convex layer in a planar set of points. We also answer a question of Chan et al. [SODA 2022] by giving a conditional lower bound for dynamic approximate square set cover. While many conditional lower bounds for dynamic data structures have been proven since the seminal work of Pătraşcu [STOC 2010], few of them relate to computational geometry problems. This is the first paper focusing on this topic. Most problems we consider can be solved in O(nlog n) time in the static case and their dynamic versions have only been approached from the perspective of improving known upper bounds. One exception to this is Klee’s measure problem in ℝ², for which Chan [CGTA 2010] gave an unconditional Ω(√n) lower bound on the worst-case update time. By a similar approach, we show that such a lower bound also holds for an important special case of Klee’s measure problem in ℝ³ known as the Hypervolume Indicator problem, even for amortized runtime in the incremental setting.
Cite as

Justin Dallant and John Iacono. Conditional Lower Bounds for Dynamic Geometric Measure Problems. In 30th Annual European Symposium on Algorithms (ESA 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 244, pp. 39:1-39:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dallant_et_al:LIPIcs.ESA.2022.39,
  author =	{Dallant, Justin and Iacono, John},
  title =	{{Conditional Lower Bounds for Dynamic Geometric Measure Problems}},
  booktitle =	{30th Annual European Symposium on Algorithms (ESA 2022)},
  pages =	{39:1--39:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-247-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{244},
  editor =	{Chechik, Shiri and Navarro, Gonzalo and Rotenberg, Eva and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2022.39},
  URN =		{urn:nbn:de:0030-drops-169777},
  doi =		{10.4230/LIPIcs.ESA.2022.39},
  annote =	{Keywords: Computational geometry, Fine-grained complexity, Dynamic data structures}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2022.31
Faster Knapsack Algorithms via Bounded Monotone Min-Plus-Convolution

Authors: Karl Bringmann and Alejandro Cassis

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We present new exact and approximation algorithms for 0-1-Knapsack and Unbounded Knapsack: - Exact Algorithm for 0-1-Knapsack: 0-1-Knapsack has known algorithms running in time Õ(n + min{n ⋅ OPT, n ⋅ W, OPT², W²}) [Bellman '57], where n is the number of items, W is the weight budget, and OPT is the optimal profit. We present an algorithm running in time Õ(n + (W + OPT)^{1.5}). This improves the running time in case n,W,OPT are roughly equal. - Exact Algorithm for Unbounded Knapsack: Unbounded Knapsack has known algorithms running in time Õ(n + min{n ⋅ p_max, n ⋅ w_max, p_max², w_max²}) [Axiotis, Tzamos '19, Jansen, Rohwedder '19, Chan, He '22], where n is the number of items, w_{max} is the largest weight of any item, and p_max is the largest profit of any item. We present an algorithm running in time Õ(n + (p_max + w_max)^{1.5}), giving a similar improvement as for 0-1-Knapsack. - Approximating Unbounded Knapsack with Resource Augmentation: Unbounded Knapsack has a known FPTAS with running time Õ(min{n/ε, n + 1/ε²}) [Jansen, Kraft '18]. We study weak approximation algorithms, which approximate the optimal profit but are allowed to overshoot the weight constraint (i.e. resource augmentation). We present the first approximation scheme for Unbounded Knapsack in this setting, achieving running time Õ(n + 1/ε^{1.5}). Along the way, we also give a simpler FPTAS with lower order improvement in the standard setting. For all of these problem settings the previously known results had matching conditional lower bounds. We avoid these lower bounds in the approximation setting by allowing resource augmentation, and in the exact setting by analyzing the time complexity in terms of weight and profit parameters (instead of only weight or only profit parameters). Our algorithms can be seen as reductions to Min-Plus-Convolution on monotone sequences with bounded entries. These structured instances of Min-Plus-Convolution can be solved in time O(n^1.5) [Chi, Duan, Xie, Zhang '22] (in contrast to the conjectured n^{2-o(1)} lower bound for the general case). We complement our results by showing reductions in the opposite direction, that is, we show that achieving our results with the constant 1.5 replaced by any constant < 2 implies subquadratic algorithms for Min-Plus-Convolution on monotone sequences with bounded entries.
Cite as

Karl Bringmann and Alejandro Cassis. Faster Knapsack Algorithms via Bounded Monotone Min-Plus-Convolution. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bringmann_et_al:LIPIcs.ICALP.2022.31,
  author =	{Bringmann, Karl and Cassis, Alejandro},
  title =	{{Faster Knapsack Algorithms via Bounded Monotone Min-Plus-Convolution}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{31:1--31:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.31},
  URN =		{urn:nbn:de:0030-drops-163727},
  doi =		{10.4230/LIPIcs.ICALP.2022.31},
  annote =	{Keywords: Knapsack, Approximation Schemes, Fine-Grained Complexity, Min-Plus Convolution}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.13
REST: Integrating Term Rewriting with Program Verification

Authors: Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables flexible but terminating term rewriting for theorem proving by: (1) exploiting newly-introduced term orderings that are more permissive than standard rewrite simplification orderings; (2) dynamically and iteratively selecting orderings based on the path of rewrites taken so far; and (3) integrating external oracles that allow steps that cannot be justified with rewrite rules. Our REST approach is designed around an easily implementable core algorithm, parameterizable by choices of term orderings and their implementations; in this way our approach can be easily integrated into existing tools. We implemented REST as a Haskell library and incorporated it into Liquid Haskell’s evaluation strategy, extending Liquid Haskell with rewriting rules. We evaluated our REST implementation by comparing it against both existing rewriting techniques and E-matching (as used in most SMT solvers) and by showing that it can be used to supplant manual lemma application in many existing Liquid Haskell proofs.
Cite as

Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers. REST: Integrating Term Rewriting with Program Verification. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 13:1-13:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{grannan_et_al:LIPIcs.ECOOP.2022.13,
  author =	{Grannan, Zachary and Vazou, Niki and Darulova, Eva and Summers, Alexander J.},
  title =	{{REST: Integrating Term Rewriting with Program Verification}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{13:1--13:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.13},
  URN =		{urn:nbn:de:0030-drops-162416},
  doi =		{10.4230/LIPIcs.ECOOP.2022.13},
  annote =	{Keywords: term rewriting, program verification, theorem proving}
}
  • Refine by Author
  • 23 Chan, Timothy M.
  • 5 Shi, Elaine
  • 4 Chan, T-H. Hubert
  • 4 Iacono, John
  • 3 Cardinal, Jean
  • Show More...

  • Refine by Classification
  • 22 Theory of computation → Computational geometry
  • 9 Theory of computation → Design and analysis of algorithms
  • 6 Theory of computation → Data structures design and analysis
  • 4 Theory of computation → Pattern matching
  • 3 Theory of computation → Approximation algorithms analysis
  • Show More...

  • Refine by Keyword
  • 5 approximation algorithms
  • 5 dynamic data structures
  • 4 computational geometry
  • 4 geometric data structures
  • 3 approximation
  • Show More...

  • Refine by Type
  • 79 document

  • Refine by Publication Year
  • 15 2021
  • 10 2017
  • 10 2020
  • 9 2019
  • 8 2023
  • Show More...

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