6 Search Results for "Smal, Alexander"


Document
Proving Unsatisfiability with Hitting Formulas

Authors: Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals

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


Abstract
A hitting formula is a set of Boolean clauses such that any two of the clauses cannot be simultaneously falsified. Hitting formulas have been studied in many different contexts at least since [Iwama, 1989] and, based on experimental evidence, Peitl and Szeider [Tomás Peitl and Stefan Szeider, 2022] conjectured that unsatisfiable hitting formulas are among the hardest for resolution. Using the fact that hitting formulas are easy to check for satisfiability we make them the foundation of a new static proof system {{rmHitting}}: a refutation of a CNF in {{rmHitting}} is an unsatisfiable hitting formula such that each of its clauses is a weakening of a clause of the refuted CNF. Comparing this system to resolution and other proof systems is equivalent to studying the hardness of hitting formulas. Our first result is that {{rmHitting}} is quasi-polynomially simulated by tree-like resolution, which means that hitting formulas cannot be exponentially hard for resolution and partially refutes the conjecture of Peitl and Szeider. We show that tree-like resolution and {{rmHitting}} are quasi-polynomially separated, while for resolution, this question remains open. For a system that is only quasi-polynomially stronger than tree-like resolution, {{rmHitting}} is surprisingly difficult to polynomially simulate in another proof system. Using the ideas of Raz-Shpilka’s polynomial identity testing for noncommutative circuits [Raz and Shpilka, 2005] we show that {{rmHitting}} is p-simulated by {{rmExtended {{rmFrege}}}}, but we conjecture that much more efficient simulations exist. As a byproduct, we show that a number of static (semi)algebraic systems are verifiable in deterministic polynomial time. We consider multiple extensions of {{rmHitting}}, and in particular a proof system {{{rmHitting}}(⊕)} related to the {{{rmRes}}(⊕)} proof system for which no superpolynomial-size lower bounds are known. {{{rmHitting}}(⊕)} p-simulates the tree-like version of {{{rmRes}}(⊕)} and is at least quasi-polynomially stronger. We show that formulas expressing the non-existence of perfect matchings in the graphs K_{n,n+2} are exponentially hard for {{{rmHitting}}(⊕)} via a reduction to the partition bound for communication complexity. See the full version of the paper for the proofs. They are omitted in this Extended Abstract.

Cite as

Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals. Proving Unsatisfiability with Hitting Formulas. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 48:1-48:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{filmus_et_al:LIPIcs.ITCS.2024.48,
  author =	{Filmus, Yuval and Hirsch, Edward A. and Riazanov, Artur and Smal, Alexander and Vinyals, Marc},
  title =	{{Proving Unsatisfiability with Hitting Formulas}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{48:1--48:20},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.48},
  URN =		{urn:nbn:de:0030-drops-195762},
  doi =		{10.4230/LIPIcs.ITCS.2024.48},
  annote =	{Keywords: hitting formulas, polynomial identity testing, query complexity}
}
Document
Super-Cubic Lower Bound for Generalized Karchmer-Wigderson Games

Authors: Artur Ignatiev, Ivan Mihajlin, and Alexander Smal

Published in: LIPIcs, Volume 248, 33rd International Symposium on Algorithms and Computation (ISAAC 2022)


Abstract
In this paper, we prove a super-cubic lower bound on the size of a communication protocol for generalized Karchmer-Wigderson game for an explicit function f: {0,1}ⁿ → {0,1}^{log n}. Lower bounds for original Karchmer-Wigderson games correspond to De Morgan formula lower bounds, thus the best known size lower bound is cubic. The generalized Karchmer-Wigderson games are similar to the original ones, so we hope that our approach can provide an insight for proving better lower bounds on the original Karchmer-Wigderson games, and hence for proving new lower bounds on De Morgan formula size. To achieve super-cubic lower bound we adapt several techniques used in formula complexity to communication protocols, prove communication complexity lower bound for a composition of several functions with a multiplexer relation, and use a technique from [Ivan Mihajlin and Alexander Smal, 2021] to extract the "hardest" function from it. As a result, in this setting we are able to show that there is a relatively small set of functions such that at least one of them does not have a small protocol. The resulting lower bound of Ω̃(n^3.156) is significantly better than the bound obtained from the counting argument.

Cite as

Artur Ignatiev, Ivan Mihajlin, and Alexander Smal. Super-Cubic Lower Bound for Generalized Karchmer-Wigderson Games. In 33rd International Symposium on Algorithms and Computation (ISAAC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 248, pp. 66:1-66:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{ignatiev_et_al:LIPIcs.ISAAC.2022.66,
  author =	{Ignatiev, Artur and Mihajlin, Ivan and Smal, Alexander},
  title =	{{Super-Cubic Lower Bound for Generalized Karchmer-Wigderson Games}},
  booktitle =	{33rd International Symposium on Algorithms and Computation (ISAAC 2022)},
  pages =	{66:1--66:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-258-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{248},
  editor =	{Bae, Sang Won and Park, Heejin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2022.66},
  URN =		{urn:nbn:de:0030-drops-173510},
  doi =		{10.4230/LIPIcs.ISAAC.2022.66},
  annote =	{Keywords: communication complexity, circuit complexity, Karchmer-Wigderson games}
}
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-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
Toward Better Depth Lower Bounds: The XOR-KRW Conjecture

Authors: Ivan Mihajlin and Alexander Smal

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


Abstract
In this paper, we propose a new conjecture, the XOR-KRW conjecture, which is a relaxation of the Karchmer-Raz-Wigderson conjecture [Mauricio Karchmer et al., 1995]. This relaxation is still strong enough to imply 𝐏 ̸ ⊆ NC¹ if proven. We also present a weaker version of this conjecture that might be used for breaking n³ lower bound for De Morgan formulas. Our study of this conjecture allows us to partially answer an open question stated in [Dmitry Gavinsky et al., 2017] regarding the composition of the universal relation with a function. To be more precise, we prove that there exists a function g such that the composition of the universal relation with g is significantly harder than just a universal relation. The fact that we can only prove the existence of g is an inherent feature of our approach. The paper’s main technical contribution is a new approach to lower bounds for multiplexer-type relations based on the non-deterministic hardness of non-equality and a new method of converting lower bounds for multiplexer-type relations into lower bounds against some function. In order to do this, we develop techniques to lower bound communication complexity in half-duplex and partially half-duplex communication models.

Cite as

Ivan Mihajlin and Alexander Smal. Toward Better Depth Lower Bounds: The XOR-KRW Conjecture. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 38:1-38:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{mihajlin_et_al:LIPIcs.CCC.2021.38,
  author =	{Mihajlin, Ivan and Smal, Alexander},
  title =	{{Toward Better Depth Lower Bounds: The XOR-KRW Conjecture}},
  booktitle =	{36th Computational Complexity Conference (CCC 2021)},
  pages =	{38:1--38:24},
  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.38},
  URN =		{urn:nbn:de:0030-drops-143121},
  doi =		{10.4230/LIPIcs.CCC.2021.38},
  annote =	{Keywords: communication complexity, KRW conjecture, circuit complexity, half-duplex communication complexity, Karchmer-Wigderson games, multiplexer relation, universal relation}
}
Document
Half-Duplex Communication Complexity

Authors: Kenneth Hoover, Russell Impagliazzo, Ivan Mihajlin, and Alexander V. Smal

Published in: LIPIcs, Volume 123, 29th International Symposium on Algorithms and Computation (ISAAC 2018)


Abstract
Suppose Alice and Bob are communicating in order to compute some function f, but instead of a classical communication channel they have a pair of walkie-talkie devices. They can use some classical communication protocol for f where in each round one player sends a bit and the other one receives it. The question is whether talking via walkie-talkie gives them more power? Using walkie-talkies instead of a classical communication channel allows players two extra possibilities: to speak simultaneously (but in this case they do not hear each other) and to listen at the same time (but in this case they do not transfer any bits). The motivation for this kind of a communication model comes from the study of the KRW conjecture. We show that for some definitions this non-classical communication model is, in fact, more powerful than the classical one as it allows to compute some functions in a smaller number of rounds. We also prove lower bounds for these models using both combinatorial and information theoretic methods.

Cite as

Kenneth Hoover, Russell Impagliazzo, Ivan Mihajlin, and Alexander V. Smal. Half-Duplex Communication Complexity. In 29th International Symposium on Algorithms and Computation (ISAAC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 123, pp. 10:1-10:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{hoover_et_al:LIPIcs.ISAAC.2018.10,
  author =	{Hoover, Kenneth and Impagliazzo, Russell and Mihajlin, Ivan and Smal, Alexander V.},
  title =	{{Half-Duplex Communication Complexity}},
  booktitle =	{29th International Symposium on Algorithms and Computation (ISAAC 2018)},
  pages =	{10:1--10:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-094-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{123},
  editor =	{Hsu, Wen-Lian and Lee, Der-Tsai and Liao, Chung-Shou},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2018.10},
  URN =		{urn:nbn:de:0030-drops-99583},
  doi =		{10.4230/LIPIcs.ISAAC.2018.10},
  annote =	{Keywords: communication complexity, half-duplex channel, information theory}
}
Document
Circuit Size Lower Bounds and #SAT Upper Bounds Through a General Framework

Authors: Alexander Golovnev, Alexander S. Kulikov, Alexander V. Smal, and Suguru Tamaki

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)


Abstract
Most of the known lower bounds for binary Boolean circuits with unrestricted depth are proved by the gate elimination method. The most efficient known algorithms for the #SAT problem on binary Boolean circuits use similar case analyses to the ones in gate elimination. Chen and Kabanets recently showed that the known case analyses can also be used to prove average case circuit lower bounds, that is, lower bounds on the size of approximations of an explicit function. In this paper, we provide a general framework for proving worst/average case lower bounds for circuits and upper bounds for #SAT that is built on ideas of Chen and Kabanets. A proof in such a framework goes as follows. One starts by fixing three parameters: a class of circuits, a circuit complexity measure, and a set of allowed substitutions. The main ingredient of a proof goes as follows: by going through a number of cases, one shows that for any circuit from the given class, one can find an allowed substitution such that the given measure of the circuit reduces by a sufficient amount. This case analysis immediately implies an upper bound for #SAT. To~obtain worst/average case circuit complexity lower bounds one needs to present an explicit construction of a function that is a disperser/extractor for the class of sources defined by the set of substitutions under consideration. We show that many known proofs (of circuit size lower bounds and upper bounds for #SAT) fall into this framework. Using this framework, we prove the following new bounds: average case lower bounds of 3.24n and 2.59n for circuits over U_2 and B_2, respectively (though the lower bound for the basis B_2 is given for a quadratic disperser whose explicit construction is not currently known), and faster than 2^n #SAT-algorithms for circuits over U_2 and B_2 of size at most 3.24n and 2.99n, respectively. Here by B_2 we mean the set of all bivariate Boolean functions, and by U_2 the set of all bivariate Boolean functions except for parity and its complement.

Cite as

Alexander Golovnev, Alexander S. Kulikov, Alexander V. Smal, and Suguru Tamaki. Circuit Size Lower Bounds and #SAT Upper Bounds Through a General Framework. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 45:1-45:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{golovnev_et_al:LIPIcs.MFCS.2016.45,
  author =	{Golovnev, Alexander and Kulikov, Alexander S. and Smal, Alexander V. and Tamaki, Suguru},
  title =	{{Circuit Size Lower Bounds and #SAT Upper Bounds Through a General Framework}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{45:1--45:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.45},
  URN =		{urn:nbn:de:0030-drops-64588},
  doi =		{10.4230/LIPIcs.MFCS.2016.45},
  annote =	{Keywords: circuit complexity, lower bounds, exponential time algorithms, satisfiability}
}
  • Refine by Author
  • 4 Mihajlin, Ivan
  • 3 Smal, Alexander
  • 2 Smal, Alexander V.
  • 1 Filmus, Yuval
  • 1 Golovnev, Alexander
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Circuit complexity
  • 1 Theory of computation → Communication complexity
  • 1 Theory of computation → Proof complexity

  • Refine by Keyword
  • 4 communication complexity
  • 3 circuit complexity
  • 2 Karchmer-Wigderson games
  • 1 De Morgan formulas
  • 1 KRW conjecture
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 2 2022
  • 1 2016
  • 1 2018
  • 1 2021
  • 1 2024

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