46 Search Results for "Göös, Mika"


Document
Fully Local Succinct Distributed Arguments

Authors: Eden Aldema Tshuva and Rotem Oshman

Published in: LIPIcs, Volume 319, 38th International Symposium on Distributed Computing (DISC 2024)


Abstract
Distributed certification is a proof system for detecting illegal network states or improper execution of distributed algorithms. A certification scheme consists of a proving algorithm, which assigns a certificate to each node, and a verification algorithm where nodes use these certificates to decide whether to accept or reject. The system must ensure that all nodes accept if and only if the network is in a legal state, adhering to the principles of completeness and soundness. The main goal is to design a scheme where the verification process is local and the certificates are succinct, while using as efficient as possible proving algorithm. In cryptographic proof systems, the soundness requirement is often relaxed to computational soundness, where soundness is guaranteed only against computationally bounded adversaries. Computationally sound proof systems are called arguments. Recently, Aldema Tshuva, Boyle, Cohen, Moran, and Oshman (TCC 2023) showed that succinct distributed arguments can be used to enable any polynomially bounded distributed algorithm to certify its execution with polylogarithmic-length certificates. However, their approach required a global communication phase, adding O(D) communication rounds in networks of diameter D, which limits its applicability to local algorithms. In this work, we give the first construction of a fully local succinct distributed argument system, where the prover and the verifier are both local. We show that a distributed algorithm that runs in R rounds, has polynomial local computation, and messages of B bits each can be compiled into a self-certifying algorithm that runs in R + polylog(n) rounds and sends messages of size B + polylog(n), with certificates of length polylog(n). This construction has several applications, including self-certification for local algorithms, ongoing certification of long-lived algorithms, and efficient local mending of the certificates when the network changes.

Cite as

Eden Aldema Tshuva and Rotem Oshman. Fully Local Succinct Distributed Arguments. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{aldematshuva_et_al:LIPIcs.DISC.2024.1,
  author =	{Aldema Tshuva, Eden and Oshman, Rotem},
  title =	{{Fully Local Succinct Distributed Arguments}},
  booktitle =	{38th International Symposium on Distributed Computing (DISC 2024)},
  pages =	{1:1--1:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-352-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{319},
  editor =	{Alistarh, Dan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2024.1},
  URN =		{urn:nbn:de:0030-drops-212662},
  doi =		{10.4230/LIPIcs.DISC.2024.1},
  annote =	{Keywords: distributed certification, proof labeling schemes, SNARG}
}
Document
Distributed Model Checking on Graphs of Bounded Treedepth

Authors: Fedor V. Fomin, Pierre Fraigniaud, Pedro Montealegre, Ivan Rapaport, and Ioan Todinca

Published in: LIPIcs, Volume 319, 38th International Symposium on Distributed Computing (DISC 2024)


Abstract
We establish that every monadic second-order logic (MSO) formula on graphs with bounded treedepth is decidable in a constant number of rounds within the CONGEST model. To our knowledge, this marks the first meta-theorem regarding distributed model-checking. Various optimization problems on graphs are expressible in MSO. Examples include determining whether a graph G has a clique of size k, whether it admits a coloring with k colors, whether it contains a graph H as a subgraph or minor, or whether terminal vertices in G could be connected via vertex-disjoint paths. Our meta-theorem significantly enhances the work of Bousquet et al. [PODC 2022], which was focused on distributed certification of MSO on graphs with bounded treedepth. Moreover, our results can be extended to solving optimization and counting problems expressible in MSO, in graphs of bounded treedepth.

Cite as

Fedor V. Fomin, Pierre Fraigniaud, Pedro Montealegre, Ivan Rapaport, and Ioan Todinca. Distributed Model Checking on Graphs of Bounded Treedepth. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{fomin_et_al:LIPIcs.DISC.2024.25,
  author =	{Fomin, Fedor V. and Fraigniaud, Pierre and Montealegre, Pedro and Rapaport, Ivan and Todinca, Ioan},
  title =	{{Distributed Model Checking on Graphs of Bounded Treedepth}},
  booktitle =	{38th International Symposium on Distributed Computing (DISC 2024)},
  pages =	{25:1--25:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-352-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{319},
  editor =	{Alistarh, Dan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2024.25},
  URN =		{urn:nbn:de:0030-drops-212513},
  doi =		{10.4230/LIPIcs.DISC.2024.25},
  annote =	{Keywords: proof-labeling schemes, local computing, CONGEST model}
}
Document
Brief Announcement
Brief Announcement: Decreasing Verification Radius in Local Certification

Authors: Jan Matyáš Křišťan and Josef Erik Sedláček

Published in: LIPIcs, Volume 319, 38th International Symposium on Distributed Computing (DISC 2024)


Abstract
This paper deals with local certification, specifically locally checkable proofs: given a graph property, the task is to certify whether a graph satisfies the property. The verification of this certification needs to be done locally without the knowledge of the whole graph. We examine the trade-off between the visibility radius and the size of certificates. We describe a procedure that decreases the radius by encoding the neighbourhood of each vertex into its certificate. We also provide a corresponding lower bound on the required certificate size increase, showing that such an approach is close to optimal.

Cite as

Jan Matyáš Křišťan and Josef Erik Sedláček. Brief Announcement: Decreasing Verification Radius in Local Certification. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 49:1-49:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{kristan_et_al:LIPIcs.DISC.2024.49,
  author =	{K\v{r}i\v{s}\v{t}an, Jan Maty\'{a}\v{s} and Sedl\'{a}\v{c}ek, Josef Erik},
  title =	{{Brief Announcement: Decreasing Verification Radius in Local Certification}},
  booktitle =	{38th International Symposium on Distributed Computing (DISC 2024)},
  pages =	{49:1--49:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-352-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{319},
  editor =	{Alistarh, Dan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2024.49},
  URN =		{urn:nbn:de:0030-drops-212773},
  doi =		{10.4230/LIPIcs.DISC.2024.49},
  annote =	{Keywords: Local certification, locally checkable proofs, proof-labeling schemes, graphs, distributed computing}
}
Document
Locally Computing Edge Orientations

Authors: Slobodan Mitrović, Ronitt Rubinfeld, and Mihir Singhal

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


Abstract
We consider the question of orienting the edges in a graph G such that every vertex has bounded out-degree. For graphs of arboricity α, there is an orientation in which every vertex has out-degree at most α and, moreover, the best possible maximum out-degree of an orientation is at least α - 1. We are thus interested in algorithms that can achieve a maximum out-degree of close to α. A widely studied approach for this problem in the distributed algorithms setting is a "peeling algorithm" that provides an orientation with maximum out-degree α(2+ε) in a logarithmic number of iterations. We consider this problem in the local computation algorithm (LCA) model, which quickly answers queries of the form "What is the orientation of edge (u,v)?" by probing the input graph. When the peeling algorithm is executed in the LCA setting by applying standard techniques, e.g., the Parnas-Ron paradigm, it requires Ω(n) probes per query on an n-vertex graph. In the case where G has unbounded degree, we show that any LCA that orients its edges to yield maximum out-degree r must use Ω(√ n/r) probes to G per query in the worst case, even if G is known to be a forest (that is, α = 1). We also show several algorithms with sublinear probe complexity when G has unbounded degree. When G is a tree such that the maximum degree Δ of G is bounded, we demonstrate an algorithm that uses Δ n^{1-log_Δ r + o(1)} probes to G per query. To obtain this result, we develop an edge-coloring approach that ultimately yields a graph-shattering-like result. We also use this shattering-like approach to demonstrate an LCA which 4-colors any tree using sublinear probes per query.

Cite as

Slobodan Mitrović, Ronitt Rubinfeld, and Mihir Singhal. Locally Computing Edge Orientations. In 32nd Annual European Symposium on Algorithms (ESA 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 308, pp. 89:1-89:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{mitrovic_et_al:LIPIcs.ESA.2024.89,
  author =	{Mitrovi\'{c}, Slobodan and Rubinfeld, Ronitt and Singhal, Mihir},
  title =	{{Locally Computing Edge Orientations}},
  booktitle =	{32nd Annual European Symposium on Algorithms (ESA 2024)},
  pages =	{89:1--89:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-338-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{308},
  editor =	{Chan, Timothy and Fischer, Johannes and Iacono, John and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2024.89},
  URN =		{urn:nbn:de:0030-drops-211603},
  doi =		{10.4230/LIPIcs.ESA.2024.89},
  annote =	{Keywords: local computation algorithms, edge orientation, tree coloring}
}
Document
RANDOM
On the Communication Complexity of Finding a King in a Tournament

Authors: Nikhil S. Mande, Manaswi Paraashar, Swagato Sanyal, and Nitin Saurabh

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


Abstract
A tournament is a complete directed graph. A source in a tournament is a vertex that has no in-neighbours (every other vertex is reachable from it via a path of length 1), and a king in a tournament is a vertex v such that every other vertex is reachable from v via a path of length at most 2. It is well known that every tournament has at least one king. In particular, a maximum out-degree vertex is a king. The tasks of finding a king and a maximum out-degree vertex in a tournament has been relatively well studied in the context of query complexity. We study the communication complexity of finding a king, of finding a maximum out-degree vertex, and of finding a source (if it exists) in a tournament, where the edges are partitioned between two players. The following are our main results for n-vertex tournaments: - We show that the communication task of finding a source in a tournament is equivalent to the well-studied Clique vs. Independent Set (CIS) problem on undirected graphs. As a result, known bounds on the communication complexity of CIS [Yannakakis, JCSS'91, Göös, Pitassi, Watson, SICOMP'18] imply a bound of Θ̃(log² n) for finding a source (if it exists, or outputting that there is no source) in a tournament. - The deterministic and randomized communication complexities of finding a king are Θ(n). The quantum communication complexity of finding a king is Θ̃(√n). - The deterministic, randomized, and quantum communication complexities of finding a maximum out-degree vertex are Θ(n log n), Θ̃(n) and Θ̃(√n), respectively. Our upper bounds above hold for all partitions of edges, and the lower bounds for a specific partition of the edges. One of our lower bounds uses a fooling-set based argument, and all our other lower bounds follow from carefully-constructed reductions from Set-Disjointness. An interesting point to note here is that while the deterministic query complexity of finding a king has been open for over two decades [Shen, Sheng, Wu, SICOMP'03], we are able to essentially resolve the complexity of this problem in a model (communication complexity) that is usually harder to analyze than query complexity.

Cite as

Nikhil S. Mande, Manaswi Paraashar, Swagato Sanyal, and Nitin Saurabh. On the Communication Complexity of Finding a King in a Tournament. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 317, pp. 64:1-64:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{mande_et_al:LIPIcs.APPROX/RANDOM.2024.64,
  author =	{Mande, Nikhil S. and Paraashar, Manaswi and Sanyal, Swagato and Saurabh, Nitin},
  title =	{{On the Communication Complexity of Finding a King in a Tournament}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2024)},
  pages =	{64:1--64:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-348-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{317},
  editor =	{Kumar, Amit and Ron-Zewi, Noga},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2024.64},
  URN =		{urn:nbn:de:0030-drops-210571},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2024.64},
  annote =	{Keywords: Communication complexity, tournaments, query complexity}
}
Document
Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree

Authors: Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche, and Luc Nicolas Spachmann

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


Abstract
We initiate an in-depth proof-complexity analysis of polynomial calculus (𝒬-PC) for Quantified Boolean Formulas (QBF). In the course of this we establish a tight proof-size characterisation of 𝒬-PC in terms of a suitable circuit model (polynomial decision lists). Using this correspondence we show a size-degree relation for 𝒬-PC, similar in spirit, yet different from the classic size-degree formula for propositional PC by Impagliazzo, Pudlák and Sgall (1999). We use the circuit characterisation together with the size-degree relation to obtain various new lower bounds on proof size in 𝒬-PC. This leads to incomparability results for 𝒬-PC systems over different fields.

Cite as

Olaf Beyersdorff, Tim Hoffmann, Kaspar Kasche, and Luc Nicolas Spachmann. Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.MFCS.2024.27,
  author =	{Beyersdorff, Olaf and Hoffmann, Tim and Kasche, Kaspar and Spachmann, Luc Nicolas},
  title =	{{Polynomial Calculus for Quantified Boolean Logic: Lower Bounds Through Circuits and Degree}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{27:1--27:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.27},
  URN =		{urn:nbn:de:0030-drops-205834},
  doi =		{10.4230/LIPIcs.MFCS.2024.27},
  annote =	{Keywords: proof complexity, QBF, polynomial calculus, circuits, lower bounds}
}
Document
Local Certification of Geometric Graph Classes

Authors: Oscar Defrain, Louis Esperet, Aurélie Lagoutte, Pat Morin, and Jean-Florent Raymond

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


Abstract
The goal of local certification is to locally convince the vertices of a graph G that G satisfies a given property. A prover assigns short certificates to the vertices of the graph, then the vertices are allowed to check their certificates and the certificates of their neighbors, and based only on this local view and their own unique identifier, they must decide whether G satisfies the given property. If the graph indeed satisfies the property, all vertices must accept the instance, and otherwise at least one vertex must reject the instance (for any possible assignment of certificates). The goal is to minimize the size of the certificates. In this paper we study the local certification of geometric and topological graph classes. While it is known that in n-vertex graphs, planarity can be certified locally with certificates of size O(log n), we show that several closely related graph classes require certificates of size Ω(n). This includes penny graphs, unit-distance graphs, (induced) subgraphs of the square grid, 1-planar graphs, and unit-square graphs. These bounds are tight up to a constant factor and give the first known examples of hereditary (and even monotone) graph classes for which the certificates must have linear size. For unit-disk graphs we obtain a lower bound of Ω(n^{1-δ}) for any δ > 0 on the size of the certificates, and an upper bound of O(n log n). The lower bounds are obtained by proving rigidity properties of the considered graphs, which might be of independent interest.

Cite as

Oscar Defrain, Louis Esperet, Aurélie Lagoutte, Pat Morin, and Jean-Florent Raymond. Local Certification of Geometric Graph Classes. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 48:1-48:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{defrain_et_al:LIPIcs.MFCS.2024.48,
  author =	{Defrain, Oscar and Esperet, Louis and Lagoutte, Aur\'{e}lie and Morin, Pat and Raymond, Jean-Florent},
  title =	{{Local Certification of Geometric Graph Classes}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{48:1--48:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.48},
  URN =		{urn:nbn:de:0030-drops-206042},
  doi =		{10.4230/LIPIcs.MFCS.2024.48},
  annote =	{Keywords: Local certification, proof labeling schemes, geometric intersection graphs}
}
Document
Lifting Dichotomies

Authors: Yaroslav Alekseev, Yuval Filmus, and Alexander Smal

Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)


Abstract
Lifting theorems are used for transferring lower bounds between Boolean function complexity measures. Given a lower bound on a complexity measure A for some function f, we compose f with a carefully chosen gadget function g and get essentially the same lower bound on a complexity measure B for the lifted function f ⋄ g. Lifting theorems have a number of applications in many different areas such as circuit complexity, communication complexity, proof complexity, etc. One of the main question in the context of lifting is how to choose a suitable gadget g. Generally, to get better results, i.e., to minimize the losses when transferring lower bounds, we need the gadget to be of a constant size (number of inputs). Unfortunately, in many settings we know lifting results only for gadgets of size that grows with the size of f, and it is unclear whether it can be improved to a constant size gadget. This motivates us to identify the properties of gadgets that make lifting possible. In this paper, we systematically study the question "For which gadgets does the lifting result hold?" in the following four settings: lifting from decision tree depth to decision tree size, lifting from conjunction DAG width to conjunction DAG size, lifting from decision tree depth to parity decision tree depth and size, and lifting from block sensitivity to deterministic and randomized communication complexities. In all the cases, we prove the complete classification of gadgets by exposing the properties of gadgets that make lifting results hold. The structure of the results shows that there is no intermediate cases - for every gadget there is either a polynomial lifting or no lifting at all. As a byproduct of our studies, we prove the log-rank conjecture for the class of functions that can be represented as f ⋄ OR ⋄ XOR for some function f. In this extended abstract, the proofs are omitted. Full proofs are given in the full version [Yaroslav Alekseev et al., 2024].

Cite as

Yaroslav Alekseev, Yuval Filmus, and Alexander Smal. Lifting Dichotomies. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{alekseev_et_al:LIPIcs.CCC.2024.9,
  author =	{Alekseev, Yaroslav and Filmus, Yuval and Smal, Alexander},
  title =	{{Lifting Dichotomies}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-331-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{300},
  editor =	{Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.9},
  URN =		{urn:nbn:de:0030-drops-204051},
  doi =		{10.4230/LIPIcs.CCC.2024.9},
  annote =	{Keywords: decision trees, log-rank conjecture, lifting, parity decision trees}
}
Document
Quantum Automating TC⁰-Frege Is LWE-Hard

Authors: Noel Arteche, Gaia Carenini, and Matthew Gray

Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)


Abstract
We prove the first hardness results against efficient proof search by quantum algorithms. We show that under Learning with Errors (LWE), the standard lattice-based cryptographic assumption, no quantum algorithm can weakly automate TC⁰-Frege. This extends the line of results of Krajíček and Pudlák (Information and Computation, 1998), Bonet, Pitassi, and Raz (FOCS, 1997), and Bonet, Domingo, Gavaldà, Maciel, and Pitassi (Computational Complexity, 2004), who showed that Extended Frege, TC⁰-Frege and AC⁰-Frege, respectively, cannot be weakly automated by classical algorithms if either the RSA cryptosystem or the Diffie-Hellman key exchange protocol are secure. To the best of our knowledge, this is the first interaction between quantum computation and propositional proof search.

Cite as

Noel Arteche, Gaia Carenini, and Matthew Gray. Quantum Automating TC⁰-Frege Is LWE-Hard. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 15:1-15:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{arteche_et_al:LIPIcs.CCC.2024.15,
  author =	{Arteche, Noel and Carenini, Gaia and Gray, Matthew},
  title =	{{Quantum Automating TC⁰-Frege Is LWE-Hard}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{15:1--15:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-331-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{300},
  editor =	{Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.15},
  URN =		{urn:nbn:de:0030-drops-204117},
  doi =		{10.4230/LIPIcs.CCC.2024.15},
  annote =	{Keywords: automatability, post-quantum cryptography, feasible interpolation}
}
Document
Depth-d Frege Systems Are Not Automatable Unless 𝖯 = NP

Authors: Theodoros Papamakarios

Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)


Abstract
We show that for any integer d > 0, depth-d Frege systems are NP-hard to automate. Namely, given a set S of depth-d formulas, it is NP-hard to find a depth-d Frege refutation of S in time polynomial in the size of the shortest such refutation. This extends the result of Atserias and Müller [JACM, 2020] for the non-automatability of resolution - a depth-1 Frege system - to Frege systems of any depth d > 0.

Cite as

Theodoros Papamakarios. Depth-d Frege Systems Are Not Automatable Unless 𝖯 = NP. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{papamakarios:LIPIcs.CCC.2024.22,
  author =	{Papamakarios, Theodoros},
  title =	{{Depth-d Frege Systems Are Not Automatable Unless 𝖯 = NP}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-331-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{300},
  editor =	{Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.22},
  URN =		{urn:nbn:de:0030-drops-204187},
  doi =		{10.4230/LIPIcs.CCC.2024.22},
  annote =	{Keywords: Proof complexity, Automatability, Bounded-depth Frege}
}
Document
Exponential Separation Between Powers of Regular and General Resolution over Parities

Authors: Sreejata Kishor Bhattacharya, Arkadev Chattopadhyay, and Pavel Dvořák

Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)


Abstract
Proving super-polynomial lower bounds on the size of proofs of unsatisfiability of Boolean formulas using resolution over parities is an outstanding problem that has received a lot of attention after its introduction by Itsykson and Sokolov [Dmitry Itsykson and Dmitry Sokolov, 2014]. Very recently, Efremenko, Garlík and Itsykson [Klim Efremenko et al., 2023] proved the first exponential lower bounds on the size of ResLin proofs that were additionally restricted to be bottom-regular. We show that there are formulas for which such regular ResLin proofs of unsatisfiability continue to have exponential size even though there exist short proofs of their unsatisfiability in ordinary, non-regular resolution. This is the first super-polynomial separation between the power of general ResLin and that of regular ResLin for any natural notion of regularity. Our argument, while building upon the work of Efremenko et al. [Klim Efremenko et al., 2023], uses additional ideas from the literature on lifting theorems.

Cite as

Sreejata Kishor Bhattacharya, Arkadev Chattopadhyay, and Pavel Dvořák. Exponential Separation Between Powers of Regular and General Resolution over Parities. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 23:1-23:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{bhattacharya_et_al:LIPIcs.CCC.2024.23,
  author =	{Bhattacharya, Sreejata Kishor and Chattopadhyay, Arkadev and Dvo\v{r}\'{a}k, Pavel},
  title =	{{Exponential Separation Between Powers of Regular and General Resolution over Parities}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{23:1--23:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-331-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{300},
  editor =	{Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.23},
  URN =		{urn:nbn:de:0030-drops-204191},
  doi =		{10.4230/LIPIcs.CCC.2024.23},
  annote =	{Keywords: Proof Complexity, Regular Reslin, Branching Programs, Lifting}
}
Document
Track A: Algorithms, Complexity and Games
Oracle Separation of QMA and QCMA with Bounded Adaptivity

Authors: Shalev Ben-David and Srijita Kundu

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)


Abstract
We give an oracle separation between QMA and QCMA for quantum algorithms that have bounded adaptivity in their oracle queries; that is, the number of rounds of oracle calls is small, though each round may involve polynomially many queries in parallel. Our oracle construction is a simplified version of the construction used recently by Li, Liu, Pelecanos, and Yamakawa (2023), who showed an oracle separation between QMA and QCMA when the quantum algorithms are only allowed to access the oracle classically. To prove our results, we introduce a property of relations called slipperiness, which may be useful for getting a fully general classical oracle separation between QMA and QCMA.

Cite as

Shalev Ben-David and Srijita Kundu. Oracle Separation of QMA and QCMA with Bounded Adaptivity. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{bendavid_et_al:LIPIcs.ICALP.2024.21,
  author =	{Ben-David, Shalev and Kundu, Srijita},
  title =	{{Oracle Separation of QMA and QCMA with Bounded Adaptivity}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.21},
  URN =		{urn:nbn:de:0030-drops-201642},
  doi =		{10.4230/LIPIcs.ICALP.2024.21},
  annote =	{Keywords: Quantum computing, computational complexity}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Smoothed Analysis of Deterministic Discounted and Mean-Payoff Games

Authors: Bruno Loff and Mateusz Skomra

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)


Abstract
We devise a policy-iteration algorithm for deterministic two-player discounted and mean-payoff games, that runs in polynomial time with high probability, on any input where each payoff is chosen independently from a sufficiently random distribution and the underlying graph of the game is ergodic. This includes the case where an arbitrary set of payoffs has been perturbed by a Gaussian, showing for the first time that deterministic two-player games can be solved efficiently, in the sense of smoothed analysis. More generally, we devise a condition number for deterministic discounted and mean-payoff games played on ergodic graphs, and show that our algorithm runs in time polynomial in this condition number. Our result confirms a previous conjecture of Boros et al., which was claimed as a theorem [Boros et al., 2011] and later retracted [Boros et al., 2018]. It stands in contrast with a recent counter-example by Christ and Yannakakis [Christ and Yannakakis, 2023], showing that Howard’s policy-iteration algorithm does not run in smoothed polynomial time on stochastic single-player mean-payoff games. Our approach is inspired by the analysis of random optimal assignment instances by Frieze and Sorkin [Frieze and Sorkin, 2007], and the analysis of bias-induced policies for mean-payoff games by Akian, Gaubert and Hochart [Akian et al., 2018].

Cite as

Bruno Loff and Mateusz Skomra. Smoothed Analysis of Deterministic Discounted and Mean-Payoff Games. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 147:1-147:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{loff_et_al:LIPIcs.ICALP.2024.147,
  author =	{Loff, Bruno and Skomra, Mateusz},
  title =	{{Smoothed Analysis of Deterministic Discounted and Mean-Payoff Games}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{147:1--147:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.147},
  URN =		{urn:nbn:de:0030-drops-202908},
  doi =		{10.4230/LIPIcs.ICALP.2024.147},
  annote =	{Keywords: Mean-payoff games, discounted games, policy iteration, smoothed analysis}
}
Document
Track A: Algorithms, Complexity and Games
Two Choices Are Enough for P-LCPs, USOs, and Colorful Tangents

Authors: Michaela Borzechowski, John Fearnley, Spencer Gordon, Rahul Savani, Patrick Schnider, and Simon Weber

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)


Abstract
We provide polynomial-time reductions between three search problems from three distinct areas: the P-matrix linear complementarity problem (P-LCP), finding the sink of a unique sink orientation (USO), and a variant of the α-Ham Sandwich problem. For all three settings, we show that "two choices are enough", meaning that the general non-binary version of the problem can be reduced in polynomial time to the binary version. This specifically means that generalized P-LCPs are equivalent to P-LCPs, and grid USOs are equivalent to cube USOs. These results are obtained by showing that both the P-LCP and our α-Ham Sandwich variant are equivalent to a new problem we introduce, P-Lin-Bellman. This problem can be seen as a new tool for formulating problems as P-LCPs.

Cite as

Michaela Borzechowski, John Fearnley, Spencer Gordon, Rahul Savani, Patrick Schnider, and Simon Weber. Two Choices Are Enough for P-LCPs, USOs, and Colorful Tangents. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{borzechowski_et_al:LIPIcs.ICALP.2024.32,
  author =	{Borzechowski, Michaela and Fearnley, John and Gordon, Spencer and Savani, Rahul and Schnider, Patrick and Weber, Simon},
  title =	{{Two Choices Are Enough for P-LCPs, USOs, and Colorful Tangents}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{32:1--32:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.32},
  URN =		{urn:nbn:de:0030-drops-201751},
  doi =		{10.4230/LIPIcs.ICALP.2024.32},
  annote =	{Keywords: P-LCP, Unique Sink Orientation, \alpha-Ham Sandwich, search complexity, TFNP, UEOPL}
}
Document
Track A: Algorithms, Complexity and Games
From Proof Complexity to Circuit Complexity via Interactive Protocols

Authors: Noel Arteche, Erfan Khaniki, Ján Pich, and Rahul Santhanam

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)


Abstract
Folklore in complexity theory suspects that circuit lower bounds against NC¹ or P/poly, currently out of reach, are a necessary step towards proving strong proof complexity lower bounds for systems like Frege or Extended Frege. Establishing such a connection formally, however, is already daunting, as it would imply the breakthrough separation NEXP ⊈ P/poly, as recently observed by Pich and Santhanam [Pich and Santhanam, 2023]. We show such a connection conditionally for the Implicit Extended Frege proof system (iEF) introduced by Krajíček [Krajíček, 2004], capable of formalizing most of contemporary complexity theory. In particular, we show that if iEF proves efficiently the standard derandomization assumption that a concrete Boolean function is hard on average for subexponential-size circuits, then any superpolynomial lower bound on the length of iEF proofs implies #P ⊈ FP/poly (which would in turn imply, for example, PSPACE ⊈ P/poly). Our proof exploits the formalization inside iEF of the soundness of the sum-check protocol of Lund, Fortnow, Karloff, and Nisan [Lund et al., 1992]. This has consequences for the self-provability of circuit upper bounds in iEF. Interestingly, further improving our result seems to require progress in constructing interactive proof systems with more efficient provers.

Cite as

Noel Arteche, Erfan Khaniki, Ján Pich, and Rahul Santhanam. From Proof Complexity to Circuit Complexity via Interactive Protocols. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{arteche_et_al:LIPIcs.ICALP.2024.12,
  author =	{Arteche, Noel and Khaniki, Erfan and Pich, J\'{a}n and Santhanam, Rahul},
  title =	{{From Proof Complexity to Circuit Complexity via Interactive Protocols}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.12},
  URN =		{urn:nbn:de:0030-drops-201557},
  doi =		{10.4230/LIPIcs.ICALP.2024.12},
  annote =	{Keywords: proof complexity, circuit complexity, interactive protocols}
}
  • Refine by Author
  • 20 Göös, Mika
  • 7 Watson, Thomas
  • 6 Pitassi, Toniann
  • 5 Filmus, Yuval
  • 4 Ben-David, Shalev
  • Show More...

  • Refine by Classification
  • 11 Theory of computation → Proof complexity
  • 10 Theory of computation → Communication complexity
  • 6 Theory of computation → Circuit complexity
  • 5 Theory of computation → Oracles and decision trees
  • 5 Theory of computation → Quantum complexity theory
  • Show More...

  • Refine by Keyword
  • 6 communication complexity
  • 5 Proof Complexity
  • 5 TFNP
  • 4 Communication complexity
  • 4 query complexity
  • Show More...

  • Refine by Type
  • 46 document

  • Refine by Publication Year
  • 17 2024
  • 7 2019
  • 4 2020
  • 4 2021
  • 4 2022
  • 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