59 Search Results for "Nguyen, Hoai-An"


Document
Infinitary Cut-Elimination via Finite Approximations

Authors: Matteo Acclavio, Gianluca Curzi, and Giulio Guerrieri

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Furthermore, we show that cut-elimination preserves the progressing criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model.

Cite as

Matteo Acclavio, Gianluca Curzi, and Giulio Guerrieri. Infinitary Cut-Elimination via Finite Approximations. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{acclavio_et_al:LIPIcs.CSL.2024.8,
  author =	{Acclavio, Matteo and Curzi, Gianluca and Guerrieri, Giulio},
  title =	{{Infinitary Cut-Elimination via Finite Approximations}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.8},
  URN =		{urn:nbn:de:0030-drops-196510},
  doi =		{10.4230/LIPIcs.CSL.2024.8},
  annote =	{Keywords: cut-elimination, non-wellfounded proofs, parsimonious logic, linear logic, proof theory, approximation, sequent calculus, non-uniform proofs}
}
Document
Syntactically and Semantically Regular Languages of λ-Terms Coincide Through Logical Relations

Authors: Vincent Moreau and Lê Thành Dũng (Tito) Nguyễn

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
A fundamental theme in automata theory is regular languages of words and trees, and their many equivalent definitions. Salvati has proposed a generalization to regular languages of simply typed λ-terms, defined using denotational semantics in finite sets. We provide here some evidence for its robustness. First, we give an equivalent syntactic characterization that naturally extends the seminal work of Hillebrand and Kanellakis connecting regular languages of words and syntactic λ-definability. Second, we show that any finitary extensional model of the simply typed λ-calculus, when used in Salvati’s definition, recognizes exactly the same class of languages of λ-terms as the category of finite sets does. The proofs of these two results rely on logical relations and can be seen as instances of a more general construction of a categorical nature, inspired by previous categorical accounts of logical relations using the gluing construction.

Cite as

Vincent Moreau and Lê Thành Dũng (Tito) Nguyễn. Syntactically and Semantically Regular Languages of λ-Terms Coincide Through Logical Relations. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 40:1-40:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{moreau_et_al:LIPIcs.CSL.2024.40,
  author =	{Moreau, Vincent and Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng (Tito)},
  title =	{{Syntactically and Semantically Regular Languages of \lambda-Terms Coincide Through Logical Relations}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{40:1--40:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.40},
  URN =		{urn:nbn:de:0030-drops-196831},
  doi =		{10.4230/LIPIcs.CSL.2024.40},
  annote =	{Keywords: regular languages, simple types, denotational semantics, logical relations}
}
Document
Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics

Authors: Jonathan Sterling, Daniel Gratzer, and Lars Birkedal

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voevodsky’s univalent foundations. We observe for the first time the profound impact of univalence on the denotational semantics of mutable state. Univalence automatically ensures that all computations are invariant under symmetries of the heap - a bountiful source of program equivalences. In particular, even the most simplistic univalent model enjoys many new equations that do not hold when the same constructions are carried out in the universes of traditional set-level (extensional) type theory.

Cite as

Jonathan Sterling, Daniel Gratzer, and Lars Birkedal. Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 47:1-47:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{sterling_et_al:LIPIcs.CSL.2024.47,
  author =	{Sterling, Jonathan and Gratzer, Daniel and Birkedal, Lars},
  title =	{{Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{47:1--47:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.47},
  URN =		{urn:nbn:de:0030-drops-196901},
  doi =		{10.4230/LIPIcs.CSL.2024.47},
  annote =	{Keywords: univalent foundations, homotopy type theory, impredicative encodings, synthetic guarded domain theory, guarded recursion, higher-order store, reference types}
}
Document
Quantum Pseudoentanglement

Authors: Scott Aaronson, Adam Bouland, Bill Fefferman, Soumik Ghosh, Umesh Vazirani, Chenyi Zhang, and Zixin Zhou

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


Abstract
Entanglement is a quantum resource, in some ways analogous to randomness in classical computation. Inspired by recent work of Gheorghiu and Hoban, we define the notion of "pseudoentanglement", a property exhibited by ensembles of efficiently constructible quantum states which are indistinguishable from quantum states with maximal entanglement. Our construction relies on the notion of quantum pseudorandom states - first defined by Ji, Liu and Song - which are efficiently constructible states indistinguishable from (maximally entangled) Haar-random states. Specifically, we give a construction of pseudoentangled states with entanglement entropy arbitrarily close to log n across every cut, a tight bound providing an exponential separation between computational vs information theoretic quantum pseudorandomness. We discuss applications of this result to Matrix Product State testing, entanglement distillation, and the complexity of the AdS/CFT correspondence. As compared with a previous version of this manuscript (arXiv:2211.00747v1) this version introduces a new pseudorandom state construction, has a simpler proof of correctness, and achieves a technically stronger result of low entanglement across all cuts simultaneously.

Cite as

Scott Aaronson, Adam Bouland, Bill Fefferman, Soumik Ghosh, Umesh Vazirani, Chenyi Zhang, and Zixin Zhou. Quantum Pseudoentanglement. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{aaronson_et_al:LIPIcs.ITCS.2024.2,
  author =	{Aaronson, Scott and Bouland, Adam and Fefferman, Bill and Ghosh, Soumik and Vazirani, Umesh and Zhang, Chenyi and Zhou, Zixin},
  title =	{{Quantum Pseudoentanglement}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{2:1--2:21},
  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.2},
  URN =		{urn:nbn:de:0030-drops-195300},
  doi =		{10.4230/LIPIcs.ITCS.2024.2},
  annote =	{Keywords: Quantum computing, Quantum complexity theory, entanglement}
}
Document
On Parallel Repetition of PCPs

Authors: Alessandro Chiesa, Ziyi Guan, and Burcu Yıldız

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


Abstract
Parallel repetition refers to a set of valuable techniques used to reduce soundness error of probabilistic proofs while saving on certain efficiency measures. Parallel repetition has been studied for interactive proofs (IPs) and multi-prover interactive proofs (MIPs). In this paper we initiate the study of parallel repetition for probabilistically checkable proofs (PCPs). We show that, perhaps surprisingly, parallel repetition of a PCP can increase soundness error, in fact bringing the soundness error to one as the number of repetitions tends to infinity. This "failure" of parallel repetition is common: we find that it occurs for a wide class of natural PCPs for NP-complete languages. We explain this unexpected phenomenon by providing a characterization result: the parallel repetition of a PCP brings the soundness error to zero if and only if a certain "MIP projection" of the PCP has soundness error strictly less than one. We show that our characterization is tight via a suitable example. Moreover, for those cases where parallel repetition of a PCP does bring the soundness error to zero, the aforementioned connection to MIPs offers preliminary results on the rate of decay of the soundness error. Finally, we propose a simple variant of parallel repetition, called consistent parallel repetition (CPR), which has the same randomness complexity and query complexity as the plain variant of parallel repetition. We show that CPR brings the soundness error to zero for every PCP (with non-trivial soundness error). In fact, we show that CPR decreases the soundness error at an exponential rate in the repetition parameter.

Cite as

Alessandro Chiesa, Ziyi Guan, and Burcu Yıldız. On Parallel Repetition of PCPs. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 34:1-34:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{chiesa_et_al:LIPIcs.ITCS.2024.34,
  author =	{Chiesa, Alessandro and Guan, Ziyi and Y{\i}ld{\i}z, Burcu},
  title =	{{On Parallel Repetition of PCPs}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{34:1--34:14},
  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.34},
  URN =		{urn:nbn:de:0030-drops-195629},
  doi =		{10.4230/LIPIcs.ITCS.2024.34},
  annote =	{Keywords: probabilistically checkable proofs, parallel repetition}
}
Document
Revisiting the Nova Proof System on a Cycle of Curves

Authors: Wilson D. Nguyen, Dan Boneh, and Srinath Setty

Published in: LIPIcs, Volume 282, 5th Conference on Advances in Financial Technologies (AFT 2023)


Abstract
Nova is an efficient recursive proof system built from an elegant folding scheme for (relaxed) R1CS statements. The original Nova paper (CRYPTO'22) presented Nova using a single elliptic curve group of order p. However, for improved efficiency, the implementation of Nova alters the scheme to use a 2-cycle of elliptic curves. This altered scheme is only described in the code and has not been proven secure. In this work, we point out a soundness vulnerability in the original implementation of the 2-cycle Nova system. To demonstrate this vulnerability, we construct a convincing Nova proof for the correct evaluation of 2^{75} rounds of the Minroot VDF in only 116 milliseconds. We then present a modification of the 2-cycle Nova system and formally prove its security. The modified system also happens to be more efficient than the original implementation. In particular, the modification eliminates an R1CS instance-witness pair from the recursive proof. The implementation of Nova has now been updated to use our optimized and secure system. In addition, we show that the folding mechanism at the core of Nova is malleable: given a proof for some statement z, an adversary can construct a proof for a related statement z', at the same depth as z, without knowledge of the witness for z'.

Cite as

Wilson D. Nguyen, Dan Boneh, and Srinath Setty. Revisiting the Nova Proof System on a Cycle of Curves. In 5th Conference on Advances in Financial Technologies (AFT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 282, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{nguyen_et_al:LIPIcs.AFT.2023.18,
  author =	{Nguyen, Wilson D. and Boneh, Dan and Setty, Srinath},
  title =	{{Revisiting the Nova Proof System on a Cycle of Curves}},
  booktitle =	{5th Conference on Advances in Financial Technologies (AFT 2023)},
  pages =	{18:1--18:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-303-4},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{282},
  editor =	{Bonneau, Joseph and Weinberg, S. Matthew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2023.18},
  URN =		{urn:nbn:de:0030-drops-192076},
  doi =		{10.4230/LIPIcs.AFT.2023.18},
  annote =	{Keywords: Cryptographic Protocols, Recursive Proof Systems, Folding, Vulnerability}
}
Document
Short Paper
Status Poles and Status Zoning to Model Residential Land Prices: Status-Quality Trade off Theory (Short Paper)

Authors: Thuy Phuong Le, Alexis Comber, Binh Quoc Tran, Phe Huu Hoang, Huy Quang Man, Linh Xuan Nguyen, Tuan Le Pham, and Tu Ngoc Bui

Published in: LIPIcs, Volume 277, 12th International Conference on Geographic Information Science (GIScience 2023)


Abstract
This study describes an approach for augmenting urban residential preference and hedonic house price models by incorporating Status-Quality Trade Off theory (SQTO). SQTO seeks explain the dynamic of urban structure using a multipolar, in which the location and strength of poles is driven by notions of residential status and dwelling quality. This paper presents in outline an approach for identifying status poles and for quantifying their effect on land and residential property prices. The results show how the incorporation of SQTO results in an enhanced understanding of variations in land / property process with increased spatial nuance. A number of future research areas are identified related to the status pole weights and the development of status pole index.

Cite as

Thuy Phuong Le, Alexis Comber, Binh Quoc Tran, Phe Huu Hoang, Huy Quang Man, Linh Xuan Nguyen, Tuan Le Pham, and Tu Ngoc Bui. Status Poles and Status Zoning to Model Residential Land Prices: Status-Quality Trade off Theory (Short Paper). In 12th International Conference on Geographic Information Science (GIScience 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 277, pp. 46:1-46:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{le_et_al:LIPIcs.GIScience.2023.46,
  author =	{Le, Thuy Phuong and Comber, Alexis and Tran, Binh Quoc and Hoang, Phe Huu and Man, Huy Quang and Nguyen, Linh Xuan and Le Pham, Tuan and Bui, Tu Ngoc},
  title =	{{Status Poles and Status Zoning to Model Residential Land Prices: Status-Quality Trade off Theory}},
  booktitle =	{12th International Conference on Geographic Information Science (GIScience 2023)},
  pages =	{46:1--46:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-288-4},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{277},
  editor =	{Beecham, Roger and Long, Jed A. and Smith, Dianna and Zhao, Qunshan and Wise, Sarah},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.GIScience.2023.46},
  URN =		{urn:nbn:de:0030-drops-189415},
  doi =		{10.4230/LIPIcs.GIScience.2023.46},
  annote =	{Keywords: spatial theory, house prices}
}
Document
APPROX
On Complexity of 1-Center in Various Metrics

Authors: Amir Abboud, MohammadHossein Bateni, Vincent Cohen-Addad, Karthik C. S., and Saeed Seddighin

Published in: LIPIcs, Volume 275, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)


Abstract
We consider the classic 1-center problem: Given a set P of n points in a metric space find the point in P that minimizes the maximum distance to the other points of P. We study the complexity of this problem in d-dimensional 𝓁_p-metrics and in edit and Ulam metrics over strings of length d. Our results for the 1-center problem may be classified based on d as follows. - Small d. Assuming the hitting set conjecture (HSC), we show that when d = ω(log n), no subquadratic algorithm can solve the 1-center problem in any of the 𝓁_p-metrics, or in the edit or Ulam metrics. - Large d. When d = Ω(n), we extend our conditional lower bound to rule out subquartic algorithms for the 1-center problem in edit metric (assuming Quantified SETH). On the other hand, we give a (1+ε)-approximation for 1-center in the Ulam metric with running time O_{ε}̃(nd+n²√d). We also strengthen some of the above lower bounds by allowing approximation algorithms or by reducing the dimension d, but only against a weaker class of algorithms which list all requisite solutions. Moreover, we extend one of our hardness results to rule out subquartic algorithms for the well-studied 1-median problem in the edit metric, where given a set of n strings each of length n, the goal is to find a string in the set that minimizes the sum of the edit distances to the rest of the strings in the set.

Cite as

Amir Abboud, MohammadHossein Bateni, Vincent Cohen-Addad, Karthik C. S., and Saeed Seddighin. On Complexity of 1-Center in Various Metrics. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 275, pp. 1:1-1:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{abboud_et_al:LIPIcs.APPROX/RANDOM.2023.1,
  author =	{Abboud, Amir and Bateni, MohammadHossein and Cohen-Addad, Vincent and Karthik C. S. and Seddighin, Saeed},
  title =	{{On Complexity of 1-Center in Various Metrics}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)},
  pages =	{1:1--1:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-296-9},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{275},
  editor =	{Megow, Nicole and Smith, Adam},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2023.1},
  URN =		{urn:nbn:de:0030-drops-188260},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2023.1},
  annote =	{Keywords: Center, Clustering, Edit metric, Ulam metric, Hamming metric, Fine-grained Complexity, Approximation}
}
Document
Early Ideas
Amortized Analysis via Coinduction (Early Ideas)

Authors: Harrison Grodin and Robert Harper

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)


Abstract
Amortized analysis is a program cost analysis technique for data structures in which the cost of operations is specified in aggregate, under the assumption of continued sequential use. Typically, amortized analyses are presented inductively, in terms of finite sequences of operations. We give an alternative coinductive formulation and prove that it is equivalent to the standard inductive definition. We describe a classic amortized data structure, the batched queue, and outline a coinductive proof of its amortized efficiency in calf, a dependent type theory for cost analysis.

Cite as

Harrison Grodin and Robert Harper. Amortized Analysis via Coinduction (Early Ideas). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, pp. 23:1-23:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{grodin_et_al:LIPIcs.CALCO.2023.23,
  author =	{Grodin, Harrison and Harper, Robert},
  title =	{{Amortized Analysis via Coinduction}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{23:1--23:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.23},
  URN =		{urn:nbn:de:0030-drops-188201},
  doi =		{10.4230/LIPIcs.CALCO.2023.23},
  annote =	{Keywords: amortized analysis, coinduction, data structure, mechanized proof}
}
Document
Can You Solve Closest String Faster Than Exhaustive Search?

Authors: Amir Abboud, Nick Fischer, Elazar Goldenberg, Karthik C. S., and Ron Safier

Published in: LIPIcs, Volume 274, 31st Annual European Symposium on Algorithms (ESA 2023)


Abstract
We study the fundamental problem of finding the best string to represent a given set, in the form of the Closest String problem: Given a set X ⊆ Σ^d of n strings, find the string x^* minimizing the radius of the smallest Hamming ball around x^* that encloses all the strings in X. In this paper, we investigate whether the Closest String problem admits algorithms that are faster than the trivial exhaustive search algorithm. We obtain the following results for the two natural versions of the problem: - In the continuous Closest String problem, the goal is to find the solution string x^* anywhere in Σ^d. For binary strings, the exhaustive search algorithm runs in time O(2^d poly(nd)) and we prove that it cannot be improved to time O(2^{(1-ε) d} poly(nd)), for any ε > 0, unless the Strong Exponential Time Hypothesis fails. - In the discrete Closest String problem, x^* is required to be in the input set X. While this problem is clearly in polynomial time, its fine-grained complexity has been pinpointed to be quadratic time n^{2 ± o(1)} whenever the dimension is ω(log n) < d < n^o(1). We complement this known hardness result with new algorithms, proving essentially that whenever d falls out of this hard range, the discrete Closest String problem can be solved faster than exhaustive search. In the small-d regime, our algorithm is based on a novel application of the inclusion-exclusion principle. Interestingly, all of our results apply (and some are even stronger) to the natural dual of the Closest String problem, called the Remotest String problem, where the task is to find a string maximizing the Hamming distance to all the strings in X.

Cite as

Amir Abboud, Nick Fischer, Elazar Goldenberg, Karthik C. S., and Ron Safier. Can You Solve Closest String Faster Than Exhaustive Search?. In 31st Annual European Symposium on Algorithms (ESA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 274, pp. 3:1-3:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{abboud_et_al:LIPIcs.ESA.2023.3,
  author =	{Abboud, Amir and Fischer, Nick and Goldenberg, Elazar and Karthik C. S. and Safier, Ron},
  title =	{{Can You Solve Closest String Faster Than Exhaustive Search?}},
  booktitle =	{31st Annual European Symposium on Algorithms (ESA 2023)},
  pages =	{3:1--3:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-295-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{274},
  editor =	{G{\o}rtz, Inge Li and Farach-Colton, Martin and Puglisi, Simon J. 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.2023.3},
  URN =		{urn:nbn:de:0030-drops-186566},
  doi =		{10.4230/LIPIcs.ESA.2023.3},
  annote =	{Keywords: Closest string, fine-grained complexity, SETH, inclusion-exclusion}
}
Document
Abstract
EMMA: Adding Sequences into a Constraint Alignment with High Accuracy and Scalability (Abstract)

Authors: Chengze Shen, Baqiao Liu, Kelly P. Williams, and Tandy Warnow

Published in: LIPIcs, Volume 273, 23rd International Workshop on Algorithms in Bioinformatics (WABI 2023)


Abstract
Multiple sequence alignment (MSA) is a crucial precursor to many downstream biological analyses, such as phylogeny estimation [Morrison, 2006], RNA structure prediction [Shapiro et al., 2007], protein structure prediction [Jumper et al., 2021], etc. Obtaining an accurate MSA can be challenging, especially when the dataset is large (i.e., more than 1000 sequences). A key technique for large-scale MSA estimation is to add sequences into an existing alignment. For example, biological knowledge can be used to form a reference alignment on a subset of the sequences, and then the remaining sequences can be added to the reference alignment. Another case where adding sequences into an existing alignment occurs is when new sequences or genomes are added to databases, leading to the opportunity to add the new sequences for each gene in the genome into a growing alignment. A third case is for de novo multiple sequence alignment, where a subset of the sequences is selected and aligned, and then the remaining sequences are added into this "backbone alignment" [Nguyen et al., 2015; Park et al., 2023; Shen et al., 2022; Liu and Warnow, 2023; Park and Warnow, 2023; Yamada et al., 2016]. Thus, adding sequences into existing alignments is a natural problem with multiple applications to biological sequence analysis. A few methods have been developed to add sequences into an existing alignment, with MAFFT--add [Katoh and Frith, 2012] perhaps the most well-known. However, several multiple sequence alignment methods that operate in two steps (first extract and align the backbone sequences and then add the remaining sequences into this backbone alignment) also provide utilities for adding sequences into a user-provided alignment. We present EMMA, a new approach for adding "query" sequences into an existing "constraint" alignment. By construction, EMMA never changes the constraint alignment, except through the introduction of additional sites to represent homologies between the query sequences. EMMA uses a divide-and-conquer technique combined with MAFFT--add (using the most accurate setting, MAFFT-linsi--add) to add sequences into a user-provided alignment. We evaluate EMMA by comparing it to MAFFT-linsi--add, MAFFT--add (the default setting), and WITCH-ng-add. We include a range of biological and simulated datasets (nucleotides and proteins) ranging in size from 1000 to almost 200,000 sequences and evaluate alignment accuracy and scalability. MAFFT-linsi--add was the slowest and least scalable method, only able to run on datasets with at most 1000 sequences in this study, but had excellent accuracy (often the best) on those datasets. We also see that EMMA has better recall than WITCH-ng-add and MAFFT--add on large datasets, especially when the backbone alignment is small or clade-based.

Cite as

Chengze Shen, Baqiao Liu, Kelly P. Williams, and Tandy Warnow. EMMA: Adding Sequences into a Constraint Alignment with High Accuracy and Scalability (Abstract). In 23rd International Workshop on Algorithms in Bioinformatics (WABI 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 273, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{shen_et_al:LIPIcs.WABI.2023.2,
  author =	{Shen, Chengze and Liu, Baqiao and Williams, Kelly P. and Warnow, Tandy},
  title =	{{EMMA: Adding Sequences into a Constraint Alignment with High Accuracy and Scalability}},
  booktitle =	{23rd International Workshop on Algorithms in Bioinformatics (WABI 2023)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-294-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{273},
  editor =	{Belazzougui, Djamal and Ouangraoua, A\"{i}da},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.WABI.2023.2},
  URN =		{urn:nbn:de:0030-drops-186285},
  doi =		{10.4230/LIPIcs.WABI.2023.2},
  annote =	{Keywords: Multiple sequence alignment, constraint alignment, MAFFT}
}
Document
On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract)

Authors: Christoph Haase, Alessio Mansutti, and Amaury Pouly

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)


Abstract
This paper introduces a generic framework that provides sufficient conditions for guaranteeing polynomial-time decidability of fixed-negation fragments of first-order theories that adhere to certain fixed-parameter tractability requirements. It enables deciding sentences of such theories with arbitrary existential quantification, conjunction and a fixed number of negation symbols in polynomial time. It was recently shown by Nguyen and Pak [SIAM J. Comput. 51(2): 1-31 (2022)] that an even more restricted such fragment of Presburger arithmetic (the first-order theory of the integers with addition and order) is NP-hard. In contrast, by application of our framework, we show that the fixed negation fragment of weak Presburger arithmetic, which drops the order relation from Presburger arithmetic in favour of equality, is decidable in polynomial time.

Cite as

Christoph Haase, Alessio Mansutti, and Amaury Pouly. On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract). In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 52:1-52:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{haase_et_al:LIPIcs.MFCS.2023.52,
  author =	{Haase, Christoph and Mansutti, Alessio and Pouly, Amaury},
  title =	{{On Polynomial-Time Decidability of k-Negations Fragments of FO Theories (Extended Abstract)}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{52:1--52:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.52},
  URN =		{urn:nbn:de:0030-drops-185869},
  doi =		{10.4230/LIPIcs.MFCS.2023.52},
  annote =	{Keywords: first-order theories, arithmetic theories, fixed-parameter tractability}
}
Document
Track A: Algorithms, Complexity and Games
Faster Submodular Maximization for Several Classes of Matroids

Authors: Monika Henzinger, Paul Liu, Jan Vondrák, and Da Wei Zheng

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


Abstract
The maximization of submodular functions have found widespread application in areas such as machine learning, combinatorial optimization, and economics, where practitioners often wish to enforce various constraints; the matroid constraint has been investigated extensively due to its algorithmic properties and expressive power. Though tight approximation algorithms for general matroid constraints exist in theory, the running times of such algorithms typically scale quadratically, and are not practical for truly large scale settings. Recent progress has focused on fast algorithms for important classes of matroids given in explicit form. Currently, nearly-linear time algorithms only exist for graphic and partition matroids [Alina Ene and Huy L. Nguyen, 2019]. In this work, we develop algorithms for monotone submodular maximization constrained by graphic, transversal matroids, or laminar matroids in time near-linear in the size of their representation. Our algorithms achieve an optimal approximation of 1-1/e-ε and both generalize and accelerate the results of Ene and Nguyen [Alina Ene and Huy L. Nguyen, 2019]. In fact, the running time of our algorithm cannot be improved within the fast continuous greedy framework of Badanidiyuru and Vondrák [Ashwinkumar Badanidiyuru and Jan Vondrák, 2014]. To achieve near-linear running time, we make use of dynamic data structures that maintain bases with approximate maximum cardinality and weight under certain element updates. These data structures need to support a weight decrease operation and a novel Freeze operation that allows the algorithm to freeze elements (i.e. force to be contained) in its basis regardless of future data structure operations. For the laminar matroid, we present a new dynamic data structure using the top tree interface of Alstrup, Holm, de Lichtenberg, and Thorup [Stephen Alstrup et al., 2005] that maintains the maximum weight basis under insertions and deletions of elements in O(log n) time. This data structure needs to support certain subtree query and path update operations that are performed every insertion and deletion that are non-trivial to handle in conjunction. For the transversal matroid the Freeze operation corresponds to requiring the data structure to keep a certain set S of vertices matched, a property that we call S-stability. While there is a large body of work on dynamic matching algorithms, none are S-stable and maintain an approximate maximum weight matching under vertex updates. We give the first such algorithm for bipartite graphs with total running time linear (up to log factors) in the number of edges.

Cite as

Monika Henzinger, Paul Liu, Jan Vondrák, and Da Wei Zheng. Faster Submodular Maximization for Several Classes of Matroids. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 74:1-74:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.ICALP.2023.74,
  author =	{Henzinger, Monika and Liu, Paul and Vondr\'{a}k, Jan and Zheng, Da Wei},
  title =	{{Faster Submodular Maximization for Several Classes of Matroids}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{74:1--74:18},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.74},
  URN =		{urn:nbn:de:0030-drops-181267},
  doi =		{10.4230/LIPIcs.ICALP.2023.74},
  annote =	{Keywords: submodular optimization, dynamic data structures, matching algorithms}
}
Document
Track A: Algorithms, Complexity and Games
Faster Matroid Partition Algorithms

Authors: Tatsuya Terao

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


Abstract
In the matroid partitioning problem, we are given k matroids ℳ₁ = (V, ℐ_1), … , ℳ_k = (V, ℐ_k) defined over a common ground set V of n elements, and we need to find a partitionable set S ⊆ V of largest possible cardinality, denoted by p. Here, a set S ⊆ V is called partitionable if there exists a partition (S_1, … , S_k) of S with S_i ∈ ℐ_i for i = 1, …, k. In 1986, Cunningham [Cunningham, 1986] presented a matroid partition algorithm that uses O(n p^{3/2} + k n) independence oracle queries, which was the previously known best algorithm. This query complexity is O(n^{5/2}) when k ≤ n. Our main result is to present a matroid partition algorithm that uses Õ(k^{1/3} n p + k n) independence oracle queries, which is Õ(n^{7/3}) when k ≤ n. This improves upon previous Cunningham’s algorithm. To obtain this, we present a new approach edge recycling augmentation, which can be attained through new ideas: an efficient utilization of the binary search technique by Nguyễn [Nguyen, 2019] and Chakrabarty-Lee-Sidford-Singla-Wong [Chakrabarty et al., 2019] and a careful analysis of the number of independence oracle queries. Our analysis differs significantly from the one for matroid intersection algorithms, because of the parameter k. We also present a matroid partition algorithm that uses Õ((n + k) √p) rank oracle queries.

Cite as

Tatsuya Terao. Faster Matroid Partition Algorithms. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 104:1-104:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{terao:LIPIcs.ICALP.2023.104,
  author =	{Terao, Tatsuya},
  title =	{{Faster Matroid Partition Algorithms}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{104:1--104:20},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.104},
  URN =		{urn:nbn:de:0030-drops-181566},
  doi =		{10.4230/LIPIcs.ICALP.2023.104},
  annote =	{Keywords: Matroid Partition, Matroid Union, Combinatorial Optimization}
}
Document
Enumerating Regular Languages with Bounded Delay

Authors: Antoine Amarilli and Mikaël Monet

Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)


Abstract
We study the task, for a given language L, of enumerating the (generally infinite) sequence of its words, without repetitions, while bounding the delay between two consecutive words. To allow for delay bounds that do not depend on the current word length, we assume a model where we produce each word by editing the preceding word with a small edit script, rather than writing out the word from scratch. In particular, this witnesses that the language is orderable, i.e., we can write its words as an infinite sequence such that the Levenshtein edit distance between any two consecutive words is bounded by a value that depends only on the language. For instance, (a+b)^* is orderable (with a variant of the Gray code), but a^* + b^* is not. We characterize which regular languages are enumerable in this sense, and show that this can be decided in PTIME in an input deterministic finite automaton (DFA) for the language. In fact, we show that, given a DFA A, we can compute in PTIME automata A₁, …, A_t such that L(A) is partitioned as L(A₁) ⊔ … ⊔ L(A_t) and every L(A_i) is orderable in this sense. Further, we show that the value of t obtained is optimal, i.e., we cannot partition L(A) into less than t orderable languages. In the case where L(A) is orderable (i.e., t = 1), we show that the ordering can be produced by a bounded-delay algorithm: specifically, the algorithm runs in a suitable pointer machine model, and produces a sequence of bounded-length edit scripts to visit the words of L(A) without repetitions, with bounded delay - exponential in |A| - between each script. In fact, we show that we can achieve this while only allowing the edit operations push and pop at the beginning and end of the word, which implies that the word can in fact be maintained in a double-ended queue. By contrast, when fixing the distance bound d between consecutive words and the number of classes of the partition, it is NP-hard in the input DFA A to decide if L(A) is orderable in this sense, already for finite languages. Last, we study the model where push-pop edits are only allowed at the end of the word, corresponding to a case where the word is maintained on a stack. We show that these operations are strictly weaker and that the slender languages are precisely those that can be partitioned into finitely many languages that are orderable in this sense. For the slender languages, we can again characterize the minimal number of languages in the partition, and achieve bounded-delay enumeration.

Cite as

Antoine Amarilli and Mikaël Monet. Enumerating Regular Languages with Bounded Delay. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{amarilli_et_al:LIPIcs.STACS.2023.8,
  author =	{Amarilli, Antoine and Monet, Mika\"{e}l},
  title =	{{Enumerating Regular Languages with Bounded Delay}},
  booktitle =	{40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-266-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{254},
  editor =	{Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.8},
  URN =		{urn:nbn:de:0030-drops-176609},
  doi =		{10.4230/LIPIcs.STACS.2023.8},
  annote =	{Keywords: Regular language, constant-delay enumeration, edit distance}
}
  • Refine by Author
  • 4 Kim Thang, Nguyen
  • 3 Ene, Alina
  • 3 Karthik C. S.
  • 3 Li, Yi
  • 3 Nguyen, Huy L.
  • Show More...

  • Refine by Classification
  • 6 Theory of computation → Approximation algorithms analysis
  • 3 Theory of computation → Categorical semantics
  • 3 Theory of computation → Denotational semantics
  • 3 Theory of computation → Problems, reductions and completeness
  • 3 Theory of computation → Streaming, sublinear and near linear time algorithms
  • Show More...

  • Refine by Keyword
  • 3 Approximation Algorithms
  • 3 Scheduling
  • 2 Combinatorial Optimization
  • 2 Lagrangian Duality
  • 2 data streams
  • Show More...

  • Refine by Type
  • 59 document

  • Refine by Publication Year
  • 10 2023
  • 9 2020
  • 9 2022
  • 7 2016
  • 5 2021
  • 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