Document

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

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.

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

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

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.

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

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

LIPIcs, Volume 271, SAT 2023, Complete Volume

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

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

Front Matter, Table of Contents, Preface, Conference Organization

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

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

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).

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

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.

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

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

LIPIcs, Volume 8, FSTTCS'10, Complete Volume

Kamal Lodaya and Meena Mahajan. LIPIcs, Volume 8, FSTTCS'10, Complete Volume. In 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

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

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.

Kamal Lodaya and Meena Mahajan. Frontmatter, Table of Contents, Preface, Conference Organization, Author Index. In 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

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

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.

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} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail