Search Results

Documents authored by Mahajan, Meena

Document
DOI: 10.4230/LIPIcs.SAT.2024.10
New Lower Bounds for Polynomial Calculus over Non-Boolean Bases

Authors: Yogesh Dahiya, Meena Mahajan, and Sasank Mouli

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
In this paper, we obtain new size lower bounds for proofs in the Polynomial Calculus (PC) proof system, in two different settings. - When the Boolean variables are encoded using ±1 (as opposed to 0,1): We establish a lifting theorem using an asymmetric gadget G, showing that for an unsatisfiable formula F, the lifted formula F∘G requires PC size 2^{Ω(d)}, where d is the degree required to refute F. Our lower bound does not depend on the number of variables n, and holds over every field. The only previously known size lower bounds in this setting were established quite recently in [Sokolov, STOC 2020] using lifting with another (symmetric) gadget. The size lower bound there is 2^{Ω((d-d₀)²/n)} (where d₀ is the degree of the initial equations arising from the formula), and is shown to hold only over the reals. - When the PC refutation proceeds over a finite field 𝔽_p and is allowed to use extension variables: We show that there is an unsatisfiable AC⁰[p] formula with N variables for which any PC refutation using N^{1+ε(1-δ)} extension variables, each of arity at most N^{1-ε} and size at most N^c, must have size exp(Ω(N^{εδ}/polylog N)). Our proof achieves these bounds by an XOR-ification of the generalised PHP^{m,r}_n formulas from [Razborov, CC 1998]. The only previously known lower bounds for PC in this setting are those obtained in [Impagliazzo-Mouli-Pitassi, CCC 2023]; in those bounds the number of extension variables is required to be sub-quadratic, and their arity is restricted to logarithmic in the number of original variables. Our result generalises these, and demonstrates a tradeoff between the number and the arity of extension variables. Since our tautology is represented by a small AC⁰[p] formula, our results imply lower bounds for a reasonably strong fragment of AC⁰[p]-Frege.
Cite as

Yogesh Dahiya, Meena Mahajan, and Sasank Mouli. New Lower Bounds for Polynomial Calculus over Non-Boolean Bases. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dahiya_et_al:LIPIcs.SAT.2024.10,
  author =	{Dahiya, Yogesh and Mahajan, Meena and Mouli, Sasank},
  title =	{{New Lower Bounds for Polynomial Calculus over Non-Boolean Bases}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{10:1--10:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.10},
  URN =		{urn:nbn:de:0030-drops-205327},
  doi =		{10.4230/LIPIcs.SAT.2024.10},
  annote =	{Keywords: Proof Complexity, Polynomial Calculus, degree, Fourier basis, extension variables}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.38
Dependency Schemes in CDCL-Based QBF Solving: A Proof-Theoretic Study

Authors: Abhimanyu Choudhury and Meena Mahajan

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
In Quantified Boolean Formulas QBFs, dependency schemes help to detect spurious or superfluous dependencies that are implied by the variable ordering in the quantifier prefix but are not essential for constructing countermodels. This detection can provably shorten refutations in specific proof systems, and is expected to speed up runs of QBF solvers. The proof system QCDCL recently defined by Beyersdorff and Böhm (LMCS 2023) abstracts the reasoning employed by QBF solvers based on conflict-driven clause-learning (CDCL) techniques. We show how to incorporate the use of dependency schemes into this proof system, either in a preprocessing phase, or in the propagations and clause learning, or both. We then show that when the reflexive resolution path dependency scheme 𝙳^rrs is used, a mixed picture emerges: the proof systems that add 𝙳^rrs to QCDCL in these three ways are not only incomparable with each other, but are also incomparable with the basic QCDCL proof system that does not use 𝙳^rrs at all, as well as with several other resolution-based QBF proof systems. A notable fact is that all our separations are achieved through QBFs with bounded quantifier alternation.
Cite as

Abhimanyu Choudhury and Meena Mahajan. Dependency Schemes in CDCL-Based QBF Solving: A Proof-Theoretic Study. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{choudhury_et_al:LIPIcs.FSTTCS.2023.38,
  author =	{Choudhury, Abhimanyu and Mahajan, Meena},
  title =	{{Dependency Schemes in CDCL-Based QBF Solving: A Proof-Theoretic Study}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{38:1--38:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.38},
  URN =		{urn:nbn:de:0030-drops-194116},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.38},
  annote =	{Keywords: QBF, CDCL, Resolution, Dependency schemes}
}
Document
DOI: 10.4230/DagRep.13.3.17
Computational Complexity of Discrete Problems (Dagstuhl Seminar 23111)

Authors: Anna Gál, Meena Mahajan, Rahul Santhanam, Till Tantau, and Manaswi Paraashar

Published in: Dagstuhl Reports, Volume 13, Issue 3 (2023)

Abstract
This report documents the program and activities of Dagstuhl Seminar 23111 "Computational Complexity of Discrete Problems", which was held in-person in March 2023 (the previous instance of the seminar series had been held online in March 2021). Following a description of the seminar’s objectives and its overall organization, this report lists the different major talks given during the seminar in alphabetical order of speakers, followed by the abstracts of the talks, including the main references and relevant sources where applicable. The return to an in-person setting allowed an intense atmosphere of active research and interaction throughout the five day seminar.
Cite as

Anna Gál, Meena Mahajan, Rahul Santhanam, Till Tantau, and Manaswi Paraashar. Computational Complexity of Discrete Problems (Dagstuhl Seminar 23111). In Dagstuhl Reports, Volume 13, Issue 3, pp. 17-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{gal_et_al:DagRep.13.3.17,
  author =	{G\'{a}l, Anna and Mahajan, Meena and Santhanam, Rahul and Tantau, Till and Paraashar, Manaswi},
  title =	{{Computational Complexity of Discrete Problems (Dagstuhl Seminar 23111)}},
  pages =	{17--31},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{13},
  number =	{3},
  editor =	{G\'{a}l, Anna and Mahajan, Meena and Santhanam, Rahul and Tantau, Till and Paraashar, Manaswi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.3.17},
  URN =		{urn:nbn:de:0030-drops-192261},
  doi =		{10.4230/DagRep.13.3.17},
  annote =	{Keywords: circuit complexity, communication complexity, computational complexity, lower bounds, randomness}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.34
Query Complexity of Search Problems

Authors: Arkadev Chattopadhyay, Yogesh Dahiya, and Meena Mahajan

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

Abstract
We relate various complexity measures like sensitivity, block sensitivity, certificate complexity for multi-output functions to the query complexities of such functions. Using these relations, we provide the following improvements upon the known relationship between pseudo-deterministic and deterministic query complexity for total search problems: - We show that deterministic query complexity is at most the third power of its pseudo-deterministic query complexity. Previously, a fourth-power relation was shown by Goldreich, Goldwasser and Ron (ITCS'13). - We improve the known separation between pseudo-deterministic and randomized decision tree size for total search problems in two ways: (1) we exhibit an exp(Ω̃(n^{1/4})) separation for the SearchCNF relation for random k-CNFs. This seems to be the first exponential lower bound on the pseudo-deterministic size complexity of SearchCNF associated with random k-CNFs. (2) we exhibit an exp(Ω(n)) separation for the ApproxHamWt relation. The previous best known separation for any relation was exp(Ω(n^{1/2})). We also separate pseudo-determinism from randomness in And and (And,Or) decision trees, and determinism from pseudo-determinism in Parity decision trees. For a hypercube colouring problem, that was introduced by Goldwasswer, Impagliazzo, Pitassi and Santhanam (CCC'21) to analyze the pseudo-deterministic complexity of a complete problem in TFNP^{dt}, we prove that either the monotone block-sensitivity or the anti-monotone block sensitivity is Ω(n^{1/3}); Goldwasser et al. showed an Ω(n^{1/2}) bound for general block-sensitivity.
Cite as

Arkadev Chattopadhyay, Yogesh Dahiya, and Meena Mahajan. Query Complexity of Search Problems. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 34:1-34:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chattopadhyay_et_al:LIPIcs.MFCS.2023.34,
  author =	{Chattopadhyay, Arkadev and Dahiya, Yogesh and Mahajan, Meena},
  title =	{{Query Complexity of Search Problems}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{34:1--34:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.34},
  URN =		{urn:nbn:de:0030-drops-185689},
  doi =		{10.4230/LIPIcs.MFCS.2023.34},
  annote =	{Keywords: Decision trees, Search problems, Pseudo-determinism, Randomness}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.SAT.2023
LIPIcs, Volume 271, SAT 2023, Complete Volume

Authors: Meena Mahajan and Friedrich Slivovsky

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
LIPIcs, Volume 271, SAT 2023, Complete Volume
Cite as

26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 1-522, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Proceedings{mahajan_et_al:LIPIcs.SAT.2023,
  title =	{{LIPIcs, Volume 271, SAT 2023, Complete Volume}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{1--522},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023},
  URN =		{urn:nbn:de:0030-drops-184615},
  doi =		{10.4230/LIPIcs.SAT.2023},
  annote =	{Keywords: LIPIcs, Volume 271, SAT 2023, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.SAT.2023.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Meena Mahajan and Friedrich Slivovsky

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{mahajan_et_al:LIPIcs.SAT.2023.0,
  author =	{Mahajan, Meena and Slivovsky, Friedrich},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{0:i--0:xviii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.0},
  URN =		{urn:nbn:de:0030-drops-184625},
  doi =		{10.4230/LIPIcs.SAT.2023.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.22
QBF Merge Resolution Is Powerful but Unnatural

Authors: Meena Mahajan and Gaurav Sood

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
The Merge Resolution proof system (M-Res) for QBFs, proposed by Beyersdorff et al. in 2019, explicitly builds partial strategies inside refutations. The original motivation for this approach was to overcome the limitations encountered in long-distance Q-Resolution proof system (LD-Q-Res), where the syntactic side-conditions, while prohibiting all unsound resolutions, also end up prohibiting some sound resolutions. However, while the advantage of M-Res over many other resolution-based QBF proof systems was already demonstrated, a comparison with LD-Q-Res itself had remained open. In this paper, we settle this question. We show that M-Res has an exponential advantage over not only LD-Q-Res, but even over LQU^+-Res and IRM, the most powerful among currently known resolution-based QBF proof systems. Combining this with results from Beyersdorff et al. 2020, we conclude that M-Res is incomparable with LQU-Res and LQU^+-Res. Our proof method reveals two additional and curious features about MRes: (i) M-Res is not closed under restrictions, and is hence not a natural proof system, and (ii) weakening axiom clauses with existential variables provably yields an exponential advantage over MRes without weakening. We further show that in the context of regular derivations, weakening axiom clauses with universal variables provably yields an exponential advantage over M-Res without weakening. These results suggest that M-Res is better used with weakening, though whether M-Res with weakening is closed under restrictions remains open. We note that even with weakening, M-Res continues to be simulated by eFrege+∀red (the simulation of ordinary M-Res was shown recently by Chew and Slivovsky).
Cite as

Meena Mahajan and Gaurav Sood. QBF Merge Resolution Is Powerful but Unnatural. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{mahajan_et_al:LIPIcs.SAT.2022.22,
  author =	{Mahajan, Meena and Sood, Gaurav},
  title =	{{QBF Merge Resolution Is Powerful but Unnatural}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{22:1--22:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.22},
  URN =		{urn:nbn:de:0030-drops-166969},
  doi =		{10.4230/LIPIcs.SAT.2022.22},
  annote =	{Keywords: QBF, proof complexity, resolution, weakening, restrictions}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2021.15
On (Simple) Decision Tree Rank

Authors: Yogesh Dahiya and Meena Mahajan

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
In the decision tree computation model for Boolean functions, the depth corresponds to query complexity, and size corresponds to storage space. The depth measure is the most well-studied one, and is known to be polynomially related to several non-computational complexity measures of functions such as certificate complexity. The size measure is also studied, but to a lesser extent. Another decision tree measure that has received very little attention is the minimal rank of the decision tree, first introduced by Ehrenfeucht and Haussler in 1989. This measure is not polynomially related to depth, and hence it can reveal additional information about the complexity of a function. It is characterised by the value of a Prover-Delayer game first proposed by Pudlák and Impagliazzo in the context of tree-like resolution proofs. In this paper we study this measure further. We obtain upper and lower bounds on rank in terms of (variants of) certificate complexity. We also obtain upper and lower bounds on the rank for composed functions in terms of the depth of the outer function and the rank of the inner function. We compute the rank exactly for several natural functions and use them to show that all the bounds we have obtained are tight. We also observe that the size-rank relationship for decision trees, obtained by Ehrenfeucht and Haussler, is tight upto constant factors.
Cite as

Yogesh Dahiya and Meena Mahajan. On (Simple) Decision Tree Rank. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dahiya_et_al:LIPIcs.FSTTCS.2021.15,
  author =	{Dahiya, Yogesh and Mahajan, Meena},
  title =	{{On (Simple) Decision Tree Rank}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.15},
  URN =		{urn:nbn:de:0030-drops-155263},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.15},
  annote =	{Keywords: Boolean functions, Decision trees, certificate complexity, rank}
}
Document
DOI: 10.4230/DagRep.11.2.1
Computational Complexity of Discrete Problems (Dagstuhl Seminar 21121)

Authors: Anna Gál, Meena Mahajan, Rahul Santhanam, and Till Tantau

Published in: Dagstuhl Reports, Volume 11, Issue 2 (2021)

Abstract
This report documents the program and activities of Dagstuhl Seminar 21121 "Computational Complexity of Discrete Problems," which was held online in March 2021. Starting with a description of the organization of the online meeting and the topics covered, we then list the different talks given during the seminar in alphabetical order of speakers, followed by the abstracts of the talks, including the main references and relevant sources where applicable. Despite the fact that only a compressed daily time slot was available for the seminar with participants from time zones spanning the whole globe and despite the fact that informal discussions were harder to hold than in a typical on-site seminar, the rate of participation throughout the seminar was very high and many lively scientific debates were held.
Cite as

Anna Gál, Meena Mahajan, Rahul Santhanam, and Till Tantau. Computational Complexity of Discrete Problems (Dagstuhl Seminar 21121). In Dagstuhl Reports, Volume 11, Issue 2, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{gal_et_al:DagRep.11.2.1,
  author =	{G\'{a}l, Anna and Mahajan, Meena and Santhanam, Rahul and Tantau, Till},
  title =	{{Computational Complexity of Discrete Problems (Dagstuhl Seminar 21121)}},
  pages =	{1--16},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2021},
  volume =	{11},
  number =	{2},
  editor =	{G\'{a}l, Anna and Mahajan, Meena and Santhanam, Rahul and Tantau, Till},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.2.1},
  URN =		{urn:nbn:de:0030-drops-146836},
  doi =		{10.4230/DagRep.11.2.1},
  annote =	{Keywords: circuit complexity, communication complexity, computational complexity, lower bounds, randomness}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.12
Hard QBFs for Merge Resolution

Authors: Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, and Gaurav Sood

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract
We prove the first proof size lower bounds for the proof system Merge Resolution (MRes [Olaf Beyersdorff et al., 2020]), a refutational proof system for prenex quantified Boolean formulas (QBF) with a CNF matrix. Unlike most QBF resolution systems in the literature, proofs in MRes consist of resolution steps together with information on countermodels, which are syntactically stored in the proofs as merge maps. As demonstrated in [Olaf Beyersdorff et al., 2020], this makes MRes quite powerful: it has strategy extraction by design and allows short proofs for formulas which are hard for classical QBF resolution systems. Here we show the first exponential lower bounds for MRes, thereby uncovering limitations of MRes. Technically, the results are either transferred from bounds from circuit complexity (for restricted versions of MRes) or directly obtained by combinatorial arguments (for full MRes). Our results imply that the MRes approach is largely orthogonal to other QBF resolution models such as the QCDCL resolution systems QRes and QURes and the expansion systems ∀Exp+Res and IR.
Cite as

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, and Gaurav Sood. Hard QBFs for Merge Resolution. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.FSTTCS.2020.12,
  author =	{Beyersdorff, Olaf and Blinkhorn, Joshua and Mahajan, Meena and Peitl, Tom\'{a}\v{s} and Sood, Gaurav},
  title =	{{Hard QBFs for Merge Resolution}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{12:1--12:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.12},
  URN =		{urn:nbn:de:0030-drops-132530},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.12},
  annote =	{Keywords: QBF, resolution, proof complexity, lower bounds}
}
Document
DOI: 10.4230/DagRep.10.2.1
SAT and Interactions (Dagstuhl Seminar 20061)

Authors: Olaf Beyersdorff, Uwe Egly, Meena Mahajan, and Cláudia Nalon

Published in: Dagstuhl Reports, Volume 10, Issue 2 (2020)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 20061 "SAT and Interactions". The seminar brought together theoreticians and practitioners from the areas of proof complexity and proof theory, SAT and QBF solving, MaxSAT, and modal logics, who discussed recent developments in their fields and embarked on an interdisciplinary exchange of ideas and techniques between these neighbouring subfields of SAT.
Cite as

Olaf Beyersdorff, Uwe Egly, Meena Mahajan, and Cláudia Nalon. SAT and Interactions (Dagstuhl Seminar 20061). In Dagstuhl Reports, Volume 10, Issue 2, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{beyersdorff_et_al:DagRep.10.2.1,
  author =	{Beyersdorff, Olaf and Egly, Uwe and Mahajan, Meena and Nalon, Cl\'{a}udia},
  title =	{{SAT and Interactions (Dagstuhl Seminar 20061)}},
  pages =	{1--18},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2020},
  volume =	{10},
  number =	{2},
  editor =	{Beyersdorff, Olaf and Egly, Uwe and Mahajan, Meena and Nalon, Cl\'{a}udia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.10.2.1},
  URN =		{urn:nbn:de:0030-drops-130576},
  doi =		{10.4230/DagRep.10.2.1},
  annote =	{Keywords: SAT, MaxSAT, QBF, proof complexity, deep inference, modal logic, solving}
}
Document
DOI: 10.4230/LIPIcs.CCC.2020.21
Algebraic Branching Programs, Border Complexity, and Tangent Spaces

Authors: Markus Bläser, Christian Ikenmeyer, Meena Mahajan, Anurag Pandey, and Nitin Saurabh

Published in: LIPIcs, Volume 169, 35th Computational Complexity Conference (CCC 2020)

Abstract
Nisan showed in 1991 that the width of a smallest noncommutative single-(source,sink) algebraic branching program (ABP) to compute a noncommutative polynomial is given by the ranks of specific matrices. This means that the set of noncommutative polynomials with ABP width complexity at most k is Zariski-closed, an important property in geometric complexity theory. It follows that approximations cannot help to reduce the required ABP width. It was mentioned by Forbes that this result would probably break when going from single-(source,sink) ABPs to trace ABPs. We prove that this is correct. Moreover, we study the commutative monotone setting and prove a result similar to Nisan, but concerning the analytic closure. We observe the same behavior here: The set of polynomials with ABP width complexity at most k is closed for single-(source,sink) ABPs and not closed for trace ABPs. The proofs reveal an intriguing connection between tangent spaces and the vector space of flows on the ABP. We close with additional observations on VQP and the closure of VNP which allows us to establish a separation between the two classes.
Cite as

Markus Bläser, Christian Ikenmeyer, Meena Mahajan, Anurag Pandey, and Nitin Saurabh. Algebraic Branching Programs, Border Complexity, and Tangent Spaces. In 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 169, pp. 21:1-21:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{blaser_et_al:LIPIcs.CCC.2020.21,
  author =	{Bl\"{a}ser, Markus and Ikenmeyer, Christian and Mahajan, Meena and Pandey, Anurag and Saurabh, Nitin},
  title =	{{Algebraic Branching Programs, Border Complexity, and Tangent Spaces}},
  booktitle =	{35th Computational Complexity Conference (CCC 2020)},
  pages =	{21:1--21:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-156-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{169},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2020.21},
  URN =		{urn:nbn:de:0030-drops-125733},
  doi =		{10.4230/LIPIcs.CCC.2020.21},
  annote =	{Keywords: Algebraic Branching Programs, Border Complexity, Tangent Spaces, Lower Bounds, Geometric Complexity Theory, Flows, VQP, VNP}
}
Document
DOI: 10.4230/LIPIcs.STACS.2019.14
Building Strategies into QBF Proofs

Authors: Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan

Published in: LIPIcs, Volume 126, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)

Abstract
Strategy extraction is of paramount importance for quantified Boolean formulas (QBF), both in solving and proof complexity. It extracts (counter)models for a QBF from a run of the solver resp. the proof of the QBF, thereby allowing to certify the solver’s answer resp. establish soundness of the system. So far in the QBF literature, strategy extraction has been algorithmically performed from proofs. Here we devise the first QBF system where (partial) strategies are built into the proof and are piecewise constructed by simple operations along with the derivation. This has several advantages: (1) lines of our calculus have a clear semantic meaning as they are accompanied by semantic objects; (2) partial strategies are represented succinctly (in contrast to some previous approaches); (3) our calculus has strategy extraction by design; and (4) the partial strategies allow new sound inference steps which are disallowed in previous central QBF calculi such as Q-Resolution and long-distance Q-Resolution. The last item (4) allows us to show an exponential separation between our new system and the previously studied reductionless long-distance resolution calculus, introduced to model QCDCL solving. Our approach also naturally lifts to dependency QBFs (DQBF), where it yields the first sound and complete CDCL-type calculus for DQBF, thus opening future avenues into DQBF CDCL solving.
Cite as

Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan. Building Strategies into QBF Proofs. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.STACS.2019.14,
  author =	{Beyersdorff, Olaf and Blinkhorn, Joshua and Mahajan, Meena},
  title =	{{Building Strategies into QBF Proofs}},
  booktitle =	{36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-100-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{126},
  editor =	{Niedermeier, Rolf and Paul, Christophe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2019.14},
  URN =		{urn:nbn:de:0030-drops-102538},
  doi =		{10.4230/LIPIcs.STACS.2019.14},
  annote =	{Keywords: QBF, DQBF, resolution, proof complexity}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.2
Lower Bound Techniques for QBF Proof Systems

Authors: Meena Mahajan

Published in: LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)

Abstract
How do we prove that a false QBF is inded false? How big a proof is needed? The special case when all quantifiers are existential is the well-studied setting of propositional proof complexity. Expectedly, universal quantifiers change the game significantly. Several proof systems have been designed in the last couple of decades to handle QBFs. Lower bound paradigms from propositional proof complexity cannot always be extended - in most cases feasible interpolation and consequent transfer of circuit lower bounds works, but obtaining lower bounds on size by providing lower bounds on width fails dramatically. A new paradigm with no analogue in the propositional world has emerged in the form of strategy extraction, allowing for transfer of circuit lower bounds, as well as obtaining independent genuine QBF lower bounds based on a semantic cost measure. This talk will provide a broad overview of some of these developments.
Cite as

Meena Mahajan. Lower Bound Techniques for QBF Proof Systems. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 2:1-2:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{mahajan:LIPIcs.STACS.2018.2,
  author =	{Mahajan, Meena},
  title =	{{Lower Bound Techniques for QBF Proof Systems}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{2:1--2:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Niedermeier, Rolf and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.2},
  URN =		{urn:nbn:de:0030-drops-85362},
  doi =		{10.4230/LIPIcs.STACS.2018.2},
  annote =	{Keywords: Proof Complexity, Quantified Boolean formulas, Resolution, Lower Bound Techniques}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.74
Computing the Maximum using (min, +) Formulas

Authors: Meena Mahajan, Prajakta Nimbhorkar, and Anuj Tawari

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
We study computation by formulas over (min,+). We consider the computation of max{x_1,...,x_n} over N as a difference of (min,+) formulas, and show that size n + n \log n is sufficient and necessary. Our proof also shows that any (min,+) formula computing the minimum of all sums of n-1 out of n variables must have n \log n leaves; this too is tight. Our proofs use a complexity measure for (min,+) functions based on minterm-like behaviour and on the entropy of an associated graph.
Cite as

Meena Mahajan, Prajakta Nimbhorkar, and Anuj Tawari. Computing the Maximum using (min, +) Formulas. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 74:1-74:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{mahajan_et_al:LIPIcs.MFCS.2017.74,
  author =	{Mahajan, Meena and Nimbhorkar, Prajakta and Tawari, Anuj},
  title =	{{Computing the Maximum using (min, +) Formulas}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{74:1--74:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.74},
  URN =		{urn:nbn:de:0030-drops-80706},
  doi =		{10.4230/LIPIcs.MFCS.2017.74},
  annote =	{Keywords: Formulas, Circuits, Lower bounds, Tropical semiring}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2017.5
Arithmetic Circuits: An Overview (Invited Talk)

Authors: Meena Mahajan

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
This talk reviews recent developments in algebraic complexity theory. It outlines some major results concerning structure, completeness, closure, and lower bounds. It describes some techniques that have been central to obtaining these results, including extreme depth reduction, partial derivatives, and padding.
Cite as

Meena Mahajan. Arithmetic Circuits: An Overview (Invited Talk). In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{mahajan:LIPIcs.CSL.2017.5,
  author =	{Mahajan, Meena},
  title =	{{Arithmetic Circuits: An Overview}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{5:1--5:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.5},
  URN =		{urn:nbn:de:0030-drops-76858},
  doi =		{10.4230/LIPIcs.CSL.2017.5},
  annote =	{Keywords: algebraic complexity, circuits, formulas, branching programs, determinant, permanent}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.40
Understanding Cutting Planes for QBFs

Authors: Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
We define a cutting planes system CP+ForallRed for quantified Boolean formulas (QBF) and analyse the proof-theoretic strength of this new calculus. While in the propositional case, Cutting Planes is of intermediate strength between resolution and Frege, our findings here show that the situation in QBF is slightly more complex: while CP+ForallRed is again weaker than QBF Frege and stronger than the CDCL-based QBF resolution systems Q-Res and QU-Res, it turns out to be incomparable to even the weakest expansion-based QBF resolution system ForallExp+Res. Technically, our results establish the effectiveness of two lower bound techniques for CP+ForallRed: via strategy extraction and via monotone feasible interpolation.
Cite as

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding Cutting Planes for QBFs. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 40:1-40:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.FSTTCS.2016.40,
  author =	{Beyersdorff, Olaf and Chew, Leroy and Mahajan, Meena and Shukla, Anil},
  title =	{{Understanding Cutting Planes for QBFs}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{40:1--40:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.40},
  URN =		{urn:nbn:de:0030-drops-68758},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.40},
  annote =	{Keywords: proof complexity, QBF, cutting planes, resolution, simulations}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.15
Are Short Proofs Narrow? QBF Resolution is not Simple

Authors: Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
The groundbreaking paper 'Short proofs are narrow - resolution made simple' by Ben-Sasson and Wigderson (J. ACM 2001) introduces what is today arguably the main technique to obtain resolution lower bounds: to show a lower bound for the width of proofs. Another important measure for resolution is space, and in their fundamental work, Atserias and Dalmau (J. Comput. Syst. Sci. 2008) show that space lower bounds again can be obtained via width lower bounds. Here we assess whether similar techniques are effective for resolution calculi for quantified Boolean formulas (QBF). A mixed picture emerges. Our main results show that both the relations between size and width as well as between space and width drastically fail in Q-resolution, even in its weaker tree-like version. On the other hand, we obtain positive results for the expansion-based resolution systems Forall-Exp+Res and IR-calc, however only in the weak tree-like models. Technically, our negative results rely on showing width lower bounds together with simultaneous upper bounds for size and space. For our positive results we exhibit space and width-preserving simulations between QBF resolution calculi.
Cite as

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Are Short Proofs Narrow? QBF Resolution is not Simple. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.STACS.2016.15,
  author =	{Beyersdorff, Olaf and Chew, Leroy and Mahajan, Meena and Shukla, Anil},
  title =	{{Are Short Proofs Narrow? QBF Resolution is not Simple}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{15:1--15:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.15},
  URN =		{urn:nbn:de:0030-drops-57164},
  doi =		{10.4230/LIPIcs.STACS.2016.15},
  annote =	{Keywords: proof complexity, QBF, resolution, lower bound techniques, simulations}
}
Document
DOI: 10.4230/DagRep.5.9.105
Circuits, Logic and Games (Dagstuhl Seminar 15401)

Authors: Mikolaj Bojanczyk, Meena Mahajan, Thomas Schwentick, and Heribert Vollmer

Published in: Dagstuhl Reports, Volume 5, Issue 9 (2016)

Abstract
Over the years, there has been a lot of interplay between circuit complexity and logic. There are tight connections between small-depth circuit classes and fragments and extensions of firstorder logic, and ideas from games and finite model theory have provided powerful lower bound techniques for circuits. In recent years, there has been an impressive and sustained growth of interest and activity in the intersection of finite model theory and Boolean circuit complexity. The central aim of the seminar was to bring together researchers from these two areas to further strengthen the mutual fertilisation. The seminar focussed on the following specific topics: -The algebraic approach to circuit complexity with its applications to finite model theory -The logic-circuit connection, with a particular emphasis on circuit lower bounds that trigger results in finite model theory like separations between logics - New connections between uniformity conditions on circuit families and logical predicates - Structural complexity and circuit lower bounds inherently using methods from logic and algebra Proof systems with low circuit complexity - Dynamic complexity: understanding the dynamic expressive power of small depth circuit classes The seminar had 43 participants from 11 countries and was very successful with respect to the exchange of recent results, ideas and methodological approaches.
Cite as

Mikolaj Bojanczyk, Meena Mahajan, Thomas Schwentick, and Heribert Vollmer. Circuits, Logic and Games (Dagstuhl Seminar 15401). In Dagstuhl Reports, Volume 5, Issue 9, pp. 105-124, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{bojanczyk_et_al:DagRep.5.9.105,
  author =	{Bojanczyk, Mikolaj and Mahajan, Meena and Schwentick, Thomas and Vollmer, Heribert},
  title =	{{Circuits, Logic and Games (Dagstuhl Seminar 15401)}},
  pages =	{105--124},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{9},
  editor =	{Bojanczyk, Mikolaj and Mahajan, Meena and Schwentick, Thomas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.9.105},
  URN =		{urn:nbn:de:0030-drops-56872},
  doi =		{10.4230/DagRep.5.9.105},
  annote =	{Keywords: computational complexity theory, finite model theory, Boolean circuits, regular languages, finite monoids, Ehrenfeucht-Fraiss\'{e}-games}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.493
Homomorphism Polynomials Complete for VP

Authors: Arnaud Durand, Meena Mahajan, Guillaume Malod, Nicolas de Rugy-Altherre, and Nitin Saurabh

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
The VP versus VNP question, introduced by Valiant, is probably the most important open question in algebraic complexity theory. Thanks to completeness results, a variant of this question, VBP versus VNP, can be succinctly restated as asking whether the permanent of a generic matrix can be written as a determinant of a matrix of polynomially bounded size. Strikingly, this restatement does not mention any notion of computational model. To get a similar restatement for the original and more fundamental question, and also to better understand the class itself, we need a complete polynomial for VP. Ad hoc constructions yielding complete polynomials were known, but not natural examples in the vein of the determinant. We give here several variants of natural complete polynomials for VP, based on the notion of graph homomorphism polynomials.
Cite as

Arnaud Durand, Meena Mahajan, Guillaume Malod, Nicolas de Rugy-Altherre, and Nitin Saurabh. Homomorphism Polynomials Complete for VP. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 493-504, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{durand_et_al:LIPIcs.FSTTCS.2014.493,
  author =	{Durand, Arnaud and Mahajan, Meena and Malod, Guillaume and de Rugy-Altherre, Nicolas and Saurabh, Nitin},
  title =	{{Homomorphism Polynomials Complete for VP}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{493--504},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.493},
  URN =		{urn:nbn:de:0030-drops-48665},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.493},
  annote =	{Keywords: algebraic complexity, graph homomorphism, polynomials, VP, VNP, completeness}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.FSTTCS.2010
LIPIcs, Volume 8, FSTTCS'10, Complete Volume

Authors: Kamal Lodaya and Meena Mahajan

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
LIPIcs, Volume 8, FSTTCS'10, Complete Volume
Cite as

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Proceedings{lodaya_et_al:LIPIcs.FSTTCS.2010,
  title =	{{LIPIcs, Volume 8, FSTTCS'10, Complete Volume}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010},
  URN =		{urn:nbn:de:0030-drops-41027},
  doi =		{10.4230/LIPIcs.FSTTCS.2010},
  annote =	{Keywords: Software/Program Verification, Models of Computation, Modes of Computation, Complexity Measures and Classes, Nonnumerical Algorithms and Problems pecifying and Verifying and Reasoning about Program}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.FSTTCS.2010.i
Frontmatter, Table of Contents, Preface, Conference Organization, Author Index

Authors: Kamal Lodaya and Meena Mahajan

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
This proceedings volume has the papers presented at the 30th annual conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), held at the Institute of Mathematical Sciences (IMSc), Chennai, during 15–18 December 2010. The conference attracted 128 submissions from 35 countries in 6 continents, most of them of very high quality. We thank the authors who submitted for making this such a competitive conference. The PC succeeded in obtaining the help of 216 external reviewers, in all producing 400 referee reports which were of immeasurable help in deciding the 38 contributed papers which have made it to this publication.
Cite as

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. i-xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{lodaya_et_al:LIPIcs.FSTTCS.2010.i,
  author =	{Lodaya, Kamal and Mahajan, Meena},
  title =	{{Frontmatter, Table of Contents, Preface, Conference Organization, Author Index}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{i--xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.i},
  URN =		{urn:nbn:de:0030-drops-28475},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Conference Organization, Author Index}
}
Document
DOI: 10.4230/DagSemProc.09421.7
Small space analogues of Valiant's classes and the limitations of skew formula

Authors: Meena Mahajan and Raghavendra Rao B. V.

Published in: Dagstuhl Seminar Proceedings, Volume 9421, Algebraic Methods in Computational Complexity (2010)

Abstract
In the uniform circuit model of computation, the width of a boolean circuit exactly characterises the ``space'' complexity of the computed function. Looking for a similar relationship in Valiant's algebraic model of computation, we propose width of an arithmetic circuit as a possible measure of space. We introduce the class VL as an algebraic variant of deterministic log-space L. In the uniform setting, we show that our definition coincides with that of VPSPACE at polynomial width. Further, to define algebraic variants of non-deterministic space-bounded classes, we introduce the notion of ``read-once'' certificates for arithmetic circuits. We show that polynomial-size algebraic branching programs can be expressed as a read-once exponential sum over polynomials in VL, ie $mbox{VBP}inSigma^R cdotmbox{VL}$. We also show that $Sigma^R cdot mbox{VBP} =mbox{VBP}$, ie VBPs are stable under read-once exponential sums. Further, we show that read-once exponential sums over a restricted class of constant-width arithmetic circuits are within VQP, and this is the largest known such subclass of poly-log-width circuits with this property. We also study the power of skew formulas and show that exponential sums of a skew formula cannot represent the determinant polynomial.
Cite as

Meena Mahajan and Raghavendra Rao B. V.. Small space analogues of Valiant's classes and the limitations of skew formula. In Algebraic Methods in Computational Complexity. Dagstuhl Seminar Proceedings, Volume 9421, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{mahajan_et_al:DagSemProc.09421.7,
  author =	{Mahajan, Meena and Rao B. V., Raghavendra},
  title =	{{Small space analogues of Valiant's classes and the limitations of   skew formula}},
  booktitle =	{Algebraic Methods in Computational Complexity},
  pages =	{1--23},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9421},
  editor =	{Manindra Agrawal and Lance Fortnow and Thomas Thierauf and Christopher Umans},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09421.7},
  URN =		{urn:nbn:de:0030-drops-24126},
  doi =		{10.4230/DagSemProc.09421.7},
  annote =	{Keywords: Algebraic circuits, space bounds, circuit width, nondeterministic circuits, skew formulas}
}
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