Search Results

Documents authored by Sofronova, Anastasia


Document
RANDOM
Searching for Falsified Clause in Random (log{n})-CNFs Is Hard for Randomized Communication

Authors: Artur Riazanov, Anastasia Sofronova, Dmitry Sokolov, and Weiqiang Yuan

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


Abstract
We show that for a randomly sampled unsatisfiable O(log n)-CNF over n variables the randomized two-party communication cost of finding a clause falsified by the given variable assignment is linear in n.

Cite as

Artur Riazanov, Anastasia Sofronova, Dmitry Sokolov, and Weiqiang Yuan. Searching for Falsified Clause in Random (log{n})-CNFs Is Hard for Randomized Communication. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 353, pp. 64:1-64:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{riazanov_et_al:LIPIcs.APPROX/RANDOM.2025.64,
  author =	{Riazanov, Artur and Sofronova, Anastasia and Sokolov, Dmitry and Yuan, Weiqiang},
  title =	{{Searching for Falsified Clause in Random (log\{n\})-CNFs Is Hard for Randomized Communication}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)},
  pages =	{64:1--64:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-397-3},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{353},
  editor =	{Ene, Alina and Chattopadhyay, Eshan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2025.64},
  URN =		{urn:nbn:de:0030-drops-244306},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2025.64},
  annote =	{Keywords: communication complexity, proof complexity, random CNF}
}
Document
A Lower Bound for k-DNF Resolution on Random CNF Formulas via Expansion

Authors: Anastasia Sofronova and Dmitry Sokolov

Published in: LIPIcs, Volume 339, 40th Computational Complexity Conference (CCC 2025)


Abstract
Random Δ-CNF formulas are one of the few candidates that are expected to be hard for proof systems and SAT algotirhms. Assume we sample m clauses over n variables. Here, the main complexity parameter is clause density, χ := m/n. For a fixed Δ, there exists a satisfiability threshold c_Δ such that for χ > c_Δ a formula is unsatisfiable with high probability. and for χ < c_Δ it is satisfiable with high probability. Near satisfiability threshold, there are various lower bounds for algorithms and proof systems [Eli Ben-Sasson, 2001; Eli Ben-Sasson and Russell Impagliazzo, 1999; Michael Alekhnovich and Alexander A. Razborov, 2003; Dima Grigoriev, 2001; Grant Schoenebeck, 2008; Pavel Hrubes and Pavel Pudlák, 2017; Noah Fleming et al., 2017; Dmitry Sokolov, 2024], and for high-density regimes, there exist upper bounds [Uriel Feige et al., 2006; Sebastian Müller and Iddo Tzameret, 2014; Jackson Abascal et al., 2021; Venkatesan Guruswami et al., 2022]. One of the frontiers in the direction of proving lower bounds on these formulas is the k-DNF Resolution proof system (aka Res(k)). There are several known results for k = 𝒪(√{log n}/{log log n}}) [Nathan Segerlind et al., 2004; Michael Alekhnovich, 2011], that are applicable only for density regime near the threshold. In this paper, we show the first Res(k) lower bound that is applicable in higher-density regimes. Our results work for slightly larger k = 𝒪(√{log n}).

Cite as

Anastasia Sofronova and Dmitry Sokolov. A Lower Bound for k-DNF Resolution on Random CNF Formulas via Expansion. In 40th Computational Complexity Conference (CCC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 339, pp. 32:1-32:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{sofronova_et_al:LIPIcs.CCC.2025.32,
  author =	{Sofronova, Anastasia and Sokolov, Dmitry},
  title =	{{A Lower Bound for k-DNF Resolution on Random CNF Formulas via Expansion}},
  booktitle =	{40th Computational Complexity Conference (CCC 2025)},
  pages =	{32:1--32:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-379-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{339},
  editor =	{Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.32},
  URN =		{urn:nbn:de:0030-drops-237269},
  doi =		{10.4230/LIPIcs.CCC.2025.32},
  annote =	{Keywords: proof complexity, random CNFs}
}
Document
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.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
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.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
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.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}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail