7 Search Results for "Sofronova, Anastasia"

Document
RANDOM
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2023.36
Sampling and Certifying Symmetric Functions

Authors: Yuval Filmus, Itai Leigh, Artur Riazanov, and Dmitry Sokolov

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

Abstract
A circuit 𝒞 samples a distribution X with an error ε if the statistical distance between the output of 𝒞 on the uniform input and X is ε. We study the hardness of sampling a uniform distribution over the set of n-bit strings of Hamming weight k denoted by Uⁿ_k for decision forests, i.e. every output bit is computed as a decision tree of the inputs. For every k there is an O(log n)-depth decision forest sampling Uⁿ_k with an inverse-polynomial error [Emanuele Viola, 2012; Czumaj, 2015]. We show that for every ε > 0 there exists τ such that for decision depth τ log (n/k) / log log (n/k), the error for sampling U_kⁿ is at least 1-ε. Our result is based on the recent robust sunflower lemma [Ryan Alweiss et al., 2021; Rao, 2019]. Our second result is about matching a set of n-bit strings with the image of a d-local circuit, i.e. such that each output bit depends on at most d input bits. We study the set of all n-bit strings whose Hamming weight is at least n/2. We improve the previously known locality lower bound from Ω(log^* n) [Beyersdorff et al., 2013] to Ω(√log n), leaving only a quartic gap from the best upper bound of O(log² n).
Cite as

Yuval Filmus, Itai Leigh, Artur Riazanov, and Dmitry Sokolov. Sampling and Certifying Symmetric Functions. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 275, pp. 36:1-36:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{filmus_et_al:LIPIcs.APPROX/RANDOM.2023.36,
  author =	{Filmus, Yuval and Leigh, Itai and Riazanov, Artur and Sokolov, Dmitry},
  title =	{{Sampling and Certifying Symmetric Functions}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)},
  pages =	{36:1--36:21},
  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.36},
  URN =		{urn:nbn:de:0030-drops-188611},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2023.36},
  annote =	{Keywords: sampling, lower bounds, robust sunflowers, decision trees, switching networks}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.59
Automating OBDD proofs is NP-hard

Authors: Dmitry Itsykson and Artur Riazanov

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
We prove that the proof system OBDD(∧, weakening) is not automatable unless P = NP. The proof is based upon the celebrated result of [Albert Atserias and Moritz Müller, 2019] about the hardness of automatability for resolution. The heart of the proof is lifting with multi-output indexing gadget from resolution block-width to dag-like multiparty number-in-hand communication protocol size with o(n) parties, where n is the number of variables in the non-lifted formula. A similar lifting theorem for protocols with n+1 participants was proved by [Göös et al., 2020] to establish the hardness of automatability result for Cutting Planes.
Cite as

Dmitry Itsykson and Artur Riazanov. Automating OBDD proofs is NP-hard. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 59:1-59:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.MFCS.2022.59,
  author =	{Itsykson, Dmitry and Riazanov, Artur},
  title =	{{Automating OBDD proofs is NP-hard}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{59:1--59:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert 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.MFCS.2022.59},
  URN =		{urn:nbn:de:0030-drops-168575},
  doi =		{10.4230/LIPIcs.MFCS.2022.59},
  annote =	{Keywords: proof complexity, OBDD, automatability, lifting, dag-like communication}
}
Document
DOI: 10.4230/LIPIcs.CCC.2022.13
A Better-Than-3log(n) Depth Lower Bound for De Morgan Formulas with Restrictions on Top Gates

Authors: Ivan Mihajlin and Anastasia Sofronova

Published in: LIPIcs, Volume 234, 37th Computational Complexity Conference (CCC 2022)

Abstract
We prove that a modification of Andreev’s function is not computable by (3 + α - ε) log(n) depth De Morgan formula with (2α - ε)log{n} layers of AND gates at the top for any 0 < α < 1/5 and any constant ε > 0. In order to do this, we prove a weak variant of Karchmer-Raz-Wigderson conjecture. To be more precise, we prove the existence of two functions f : {0,1}ⁿ → {0,1} and g : {0,1}ⁿ → {0,1}ⁿ such that f(g(x) ⊕ y) is not computable by depth (1 + α - ε) n formulas with (2 α - ε) n layers of AND gates at the top. We do this by a top-down approach, which was only used before for depth-3 model. Our technical contribution includes combinatorial insights into structure of composition with random boolean function, which led us to introducing a notion of well-mixed sets. A set of functions is well-mixed if, when composed with a random function, it does not have subsets that agree on large fractions of inputs. We use probabilistic method to prove the existence of well-mixed sets.
Cite as

Ivan Mihajlin and Anastasia Sofronova. A Better-Than-3log(n) Depth Lower Bound for De Morgan Formulas with Restrictions on Top Gates. In 37th Computational Complexity Conference (CCC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 234, pp. 13:1-13:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{mihajlin_et_al:LIPIcs.CCC.2022.13,
  author =	{Mihajlin, Ivan and Sofronova, Anastasia},
  title =	{{A Better-Than-3log(n) Depth Lower Bound for De Morgan Formulas with Restrictions on Top Gates}},
  booktitle =	{37th Computational Complexity Conference (CCC 2022)},
  pages =	{13:1--13:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-241-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{234},
  editor =	{Lovett, Shachar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2022.13},
  URN =		{urn:nbn:de:0030-drops-165755},
  doi =		{10.4230/LIPIcs.CCC.2022.13},
  annote =	{Keywords: formula complexity, communication complexity, Karchmer-Raz-Wigderson conjecture, De Morgan formulas}
}
Document
DOI: 10.4230/LIPIcs.CCC.2022.15
Pseudorandom Generators, Resolution and Heavy Width

Authors: Dmitry Sokolov

Published in: LIPIcs, Volume 234, 37th Computational Complexity Conference (CCC 2022)

Abstract
Following the paper of Alekhnovich, Ben-Sasson, Razborov, Wigderson [Michael Alekhnovich et al., 2004] we call a pseudorandom generator ℱ:{0, 1}ⁿ → {0, 1}^m hard for a propositional proof system P if P cannot efficiently prove the (properly encoded) statement b ∉ Im(ℱ) for any string b ∈ {0, 1}^m. In [Michael Alekhnovich et al., 2004] the authors suggested the "functional encoding" of the considered statement for Nisan-Wigderson generator that allows the introduction of "local" extension variables. These extension variables may potentially significantly increase the power of the proof system. In [Michael Alekhnovich et al., 2004] authors gave a lower bound of exp[Ω(n²/{m⋅2^{2^Δ}})] on the length of Resolution proofs where Δ is the degree of the dependency graph of the generator. This lower bound meets the barrier for the restriction technique. In this paper, we introduce a "heavy width" measure for Resolution that allows us to show a lower bound of exp[n²/{m 2^𝒪(εΔ)}] on the length of Resolution proofs of the considered statement for the Nisan-Wigderson generator. This gives an exponential lower bound up to Δ := log^{2 - δ} n (the bigger degree the more extension variables we can use). In [Michael Alekhnovich et al., 2004] authors left an open problem to get rid of scaling factor 2^{2^Δ}, it is a solution to this open problem.
Cite as

Dmitry Sokolov. Pseudorandom Generators, Resolution and Heavy Width. In 37th Computational Complexity Conference (CCC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 234, pp. 15:1-15:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{sokolov:LIPIcs.CCC.2022.15,
  author =	{Sokolov, Dmitry},
  title =	{{Pseudorandom Generators, Resolution and Heavy Width}},
  booktitle =	{37th Computational Complexity Conference (CCC 2022)},
  pages =	{15:1--15:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-241-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{234},
  editor =	{Lovett, Shachar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2022.15},
  URN =		{urn:nbn:de:0030-drops-165770},
  doi =		{10.4230/LIPIcs.CCC.2022.15},
  annote =	{Keywords: proof complexity, pseudorandom generators, resolution, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.CCC.2021.3
Proof Complexity of Natural Formulas via Communication Arguments

Authors: Dmitry Itsykson and Artur Riazanov

Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)

Abstract
A canonical communication problem Search(φ) is defined for every unsatisfiable CNF φ: an assignment to the variables of φ is partitioned among the communicating parties, they are to find a clause of φ falsified by this assignment. Lower bounds on the randomized k-party communication complexity of Search(φ) in the number-on-forehead (NOF) model imply tree-size lower bounds, rank lower bounds, and size-space tradeoffs for the formula φ in the semantic proof system T^{cc}(k,c) that operates with proof lines that can be computed by k-party randomized communication protocol using at most c bits of communication [Göös and Pitassi, 2014]. All known lower bounds on Search(φ) (e.g. [Beame et al., 2007; Göös and Pitassi, 2014; Russell Impagliazzo et al., 1994]) are realized on ad-hoc formulas φ (i.e. they were introduced specifically for these lower bounds). We introduce a new communication complexity approach that allows establishing proof complexity lower bounds for natural formulas. First, we demonstrate our approach for two-party communication and apply it to the proof system Res(⊕) that operates with disjunctions of linear equalities over 𝔽₂ [Dmitry Itsykson and Dmitry Sokolov, 2014]. Let a formula PM_G encode that a graph G has a perfect matching. If G has an odd number of vertices, then PM_G has a tree-like Res(⊕)-refutation of a polynomial-size [Dmitry Itsykson and Dmitry Sokolov, 2014]. It was unknown whether this is the case for graphs with an even number of vertices. Using our approach we resolve this question and show a lower bound 2^{Ω(n)} on size of tree-like Res(⊕)-refutations of PM_{K_{n+2,n}}. Then we apply our approach for k-party communication complexity in the NOF model and obtain a Ω(1/k 2^{n/2k - 3k/2}) lower bound on the randomized k-party communication complexity of Search(BPHP^{M}_{2ⁿ}) w.r.t. to some natural partition of the variables, where BPHP^{M}_{2ⁿ} is the bit pigeonhole principle and M = 2ⁿ+2^{n(1-1/k)}. In particular, our result implies that the bit pigeonhole requires exponential tree-like Th(k) proofs, where Th(k) is the semantic proof system operating with polynomial inequalities of degree at most k and k = 𝒪(log^{1-ε} n) for some ε > 0. We also show that BPHP^{2ⁿ+1}_{2ⁿ} superpolynomially separates tree-like Th(log^{1-ε} m) from tree-like Th(log m), where m is the number of variables in the refuted formula.
Cite as

Dmitry Itsykson and Artur Riazanov. Proof Complexity of Natural Formulas via Communication Arguments. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 3:1-3:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{itsykson_et_al:LIPIcs.CCC.2021.3,
  author =	{Itsykson, Dmitry and Riazanov, Artur},
  title =	{{Proof Complexity of Natural Formulas via Communication Arguments}},
  booktitle =	{36th Computational Complexity Conference (CCC 2021)},
  pages =	{3:1--3:34},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-193-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{200},
  editor =	{Kabanets, Valentine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.3},
  URN =		{urn:nbn:de:0030-drops-142773},
  doi =		{10.4230/LIPIcs.CCC.2021.3},
  annote =	{Keywords: bit pigeonhole principle, disjointness, multiparty communication complexity, perfect matching, proof complexity, randomized communication complexity, Resolution over linear equations, tree-like proofs}
}
Document
DOI: 10.4230/LIPIcs.CCC.2021.17
Branching Programs with Bounded Repetitions and Flow Formulas

Authors: Anastasia Sofronova and Dmitry Sokolov

Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)

Abstract
Restricted branching programs capture various complexity measures like space in Turing machines or length of proofs in proof systems. In this paper, we focus on the application in the proof complexity that was discovered by Lovasz et al. [László Lovász et al., 1995] who showed the equivalence between regular Resolution and read-once branching programs for "unsatisfied clause search problem" (Search_φ). This connection is widely used, in particular, in the recent breakthrough result about the Clique problem in regular Resolution by Atserias et al. [Albert Atserias et al., 2018]. We study the branching programs with bounded repetitions, so-called (1,+k)-BPs (Sieling [Detlef Sieling, 1996]) in application to the Search_φ problem. On the one hand, it is a natural generalization of read-once branching programs. On the other hand, this model gives a powerful proof system that can efficiently certify the unsatisfiability of a wide class of formulas that is hard for Resolution (Knop [Alexander Knop, 2017]). We deal with Search_φ that is "relatively easy" compared to all known hard examples for the (1,+k)-BPs. We introduce the first technique for proving exponential lower bounds for the (1,+k)-BPs on Search_φ. To do it we combine a well-known technique for proving lower bounds on the size of branching programs [Detlef Sieling, 1996; Detlef Sieling and Ingo Wegener, 1994; Stasys Jukna and Alexander A. Razborov, 1998] with the modification of the "closure" technique [Michael Alekhnovich et al., 2004; Michael Alekhnovich and Alexander A. Razborov, 2003]. In contrast with most Resolution lower bounds, our technique uses not only "local" properties of the formula, but also a "global" structure. Our hard examples are based on the Flow formulas introduced in [Michael Alekhnovich and Alexander A. Razborov, 2003].
Cite as

Anastasia Sofronova and Dmitry Sokolov. Branching Programs with Bounded Repetitions and Flow Formulas. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 17:1-17:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{sofronova_et_al:LIPIcs.CCC.2021.17,
  author =	{Sofronova, Anastasia and Sokolov, Dmitry},
  title =	{{Branching Programs with Bounded Repetitions and Flow Formulas}},
  booktitle =	{36th Computational Complexity Conference (CCC 2021)},
  pages =	{17:1--17:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-193-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{200},
  editor =	{Kabanets, Valentine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.17},
  URN =		{urn:nbn:de:0030-drops-142915},
  doi =		{10.4230/LIPIcs.CCC.2021.17},
  annote =	{Keywords: proof complexity, branching programs, bounded repetitions, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.49
Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs

Authors: Nicola Galesi, Dmitry Itsykson, Artur Riazanov, and Anastasia Sofronova

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
We prove that there is a constant K such that Tseitin formulas for an undirected graph G requires proofs of size 2^{tw(G)^{Omega(1/d)}} in depth-d Frege systems for d<(K log n)/(log log n), where tw(G) is the treewidth of G. This extends Håstad recent lower bound for the grid graph to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent. Namely, we show that if a Tseitin formula for a graph G has size s, then for all large enough d, it has a depth-d Frege proof of size 2^{tw(G)^{O(1/d)}} poly(s). Through this result we settle the question posed by M. Alekhnovich and A. Razborov of showing that the class of Tseitin formulas is quasi-automatizable for resolution.
Cite as

Nicola Galesi, Dmitry Itsykson, Artur Riazanov, and Anastasia Sofronova. Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 49:1-49:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{galesi_et_al:LIPIcs.MFCS.2019.49,
  author =	{Galesi, Nicola and Itsykson, Dmitry and Riazanov, Artur and Sofronova, Anastasia},
  title =	{{Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{49:1--49:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.49},
  URN =		{urn:nbn:de:0030-drops-109932},
  doi =		{10.4230/LIPIcs.MFCS.2019.49},
  annote =	{Keywords: Tseitin formula, treewidth, AC0-Frege}
}
  • Refine by Author
  • 4 Riazanov, Artur
  • 3 Itsykson, Dmitry
  • 3 Sofronova, Anastasia
  • 3 Sokolov, Dmitry
  • 1 Filmus, Yuval
  • Show More...

  • Refine by Classification
  • 4 Theory of computation → Proof complexity
  • 2 Theory of computation → Circuit complexity
  • 1 Theory of computation → Communication complexity
  • 1 Theory of computation → Computational complexity and cryptography
  • 1 Theory of computation → Generating random combinatorial structures

  • Refine by Keyword
  • 4 proof complexity
  • 3 lower bounds
  • 1 AC0-Frege
  • 1 De Morgan formulas
  • 1 Karchmer-Raz-Wigderson conjecture
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 3 2022
  • 2 2021
  • 1 2019
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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