106 Search Results for "Mahajan, Meena"

Volume

LIPIcs, Volume 271

26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

SAT 2023, July 4-8, 2023, Alghero, Italy

Editors: Meena Mahajan and Friedrich Slivovsky

Volume

LIPIcs, Volume 8

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

FSTTCS 2010, December 15-18, 2010, Chennai, India

Editors: Kamal Lodaya and Meena Mahajan

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.SEA.2024.7
Local Search k-means++ with Foresight

Authors: Theo Conrads, Lukas Drexler, Joshua Könen, Daniel R. Schmidt, and Melanie Schmidt

Published in: LIPIcs, Volume 301, 22nd International Symposium on Experimental Algorithms (SEA 2024)

Abstract
Since its introduction in 1957, Lloyd’s algorithm for k-means clustering has been extensively studied and has undergone several improvements. While in its original form it does not guarantee any approximation factor at all, Arthur and Vassilvitskii (SODA 2007) proposed k-means++ which enhances Lloyd’s algorithm by a seeding method which guarantees a 𝒪(log k)-approximation in expectation. More recently, Lattanzi and Sohler (ICML 2019) proposed LS++ which further improves the solution quality of k-means++ by local search techniques to obtain a 𝒪(1)-approximation. On the practical side, the greedy variant of k-means++ is often used although its worst-case behaviour is provably worse than for the standard k-means++ variant. We investigate how to improve LS++ further in practice. We study two options for improving the practical performance: (a) Combining LS++ with greedy k-means++ instead of k-means++, and (b) Improving LS++ by better entangling it with Lloyd’s algorithm. Option (a) worsens the theoretical guarantees of k-means++ but improves the practical quality also in combination with LS++ as we confirm in our experiments. Option (b) is our new algorithm, Foresight LS++. We experimentally show that FLS++ improves upon the solution quality of LS++. It retains its asymptotic runtime and its worst-case approximation bounds.
Cite as

Theo Conrads, Lukas Drexler, Joshua Könen, Daniel R. Schmidt, and Melanie Schmidt. Local Search k-means++ with Foresight. In 22nd International Symposium on Experimental Algorithms (SEA 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 301, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{conrads_et_al:LIPIcs.SEA.2024.7,
  author =	{Conrads, Theo and Drexler, Lukas and K\"{o}nen, Joshua and Schmidt, Daniel R. and Schmidt, Melanie},
  title =	{{Local Search k-means++ with Foresight}},
  booktitle =	{22nd International Symposium on Experimental Algorithms (SEA 2024)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-325-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{301},
  editor =	{Liberti, Leo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2024.7},
  URN =		{urn:nbn:de:0030-drops-203727},
  doi =		{10.4230/LIPIcs.SEA.2024.7},
  annote =	{Keywords: k-means clustering, kmeans++, greedy, local search}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2024.27
Determinants vs. Algebraic Branching Programs

Authors: Abhranil Chatterjee, Mrinal Kumar, and Ben Lee Volk

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

Abstract
We show that for every homogeneous polynomial of degree d, if it has determinantal complexity at most s, then it can be computed by a homogeneous algebraic branching program (ABP) of size at most O(d⁵s). Moreover, we show that for most homogeneous polynomials, the width of the resulting homogeneous ABP is just s-1 and the size is at most O(ds). Thus, for constant degree homogeneous polynomials, their determinantal complexity and ABP complexity are within a constant factor of each other and hence, a super-linear lower bound for ABPs for any constant degree polynomial implies a super-linear lower bound on determinantal complexity; this relates two open problems of great interest in algebraic complexity. As of now, super-linear lower bounds for ABPs are known only for polynomials of growing degree [Mrinal Kumar, 2019; Prerona Chatterjee et al., 2022], and for determinantal complexity the best lower bounds are larger than the number of variables only by a constant factor [Mrinal Kumar and Ben Lee Volk, 2022]. While determinantal complexity and ABP complexity are classically known to be polynomially equivalent [Meena Mahajan and V. Vinay, 1997], the standard transformation from the former to the latter incurs a polynomial blow up in size in the process, and thus, it was unclear if a super-linear lower bound for ABPs implies a super-linear lower bound on determinantal complexity. In particular, a size preserving transformation from determinantal complexity to ABPs does not appear to have been known prior to this work, even for constant degree polynomials.
Cite as

Abhranil Chatterjee, Mrinal Kumar, and Ben Lee Volk. Determinants vs. Algebraic Branching Programs. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 27:1-27:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.ITCS.2024.27,
  author =	{Chatterjee, Abhranil and Kumar, Mrinal and Volk, Ben Lee},
  title =	{{Determinants vs. Algebraic Branching Programs}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{27:1--27:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-309-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{287},
  editor =	{Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.27},
  URN =		{urn:nbn:de:0030-drops-195550},
  doi =		{10.4230/LIPIcs.ITCS.2024.27},
  annote =	{Keywords: Determinant, Algebraic Branching Program, Lower Bounds, Singular Variety}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2024.91
Lower Bounds for Planar Arithmetic Circuits

Authors: C. Ramya and Pratik Shastri

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

Abstract
Arithmetic circuits are a natural well-studied model for computing multivariate polynomials over a field. In this paper, we study planar arithmetic circuits. These are circuits whose underlying graph is planar. In particular, we prove an Ω(nlog n) lower bound on the size of planar arithmetic circuits computing explicit bilinear forms on 2n variables. As a consequence, we get an Ω(nlog n) lower bound on the size of arithmetic formulas and planar algebraic branching programs computing explicit bilinear forms. This is the first such lower bound on the formula complexity of an explicit bilinear form. In the case of read-once planar circuits, we show Ω(n²) size lower bounds for computing explicit bilinear forms. Furthermore, we prove fine separations between the various planar models of computations mentioned above. In addition to this, we look at multi-output planar circuits and show Ω(n^{4/3}) size lower bound for computing an explicit linear transformation on n-variables. For a suitable definition of multi-output formulas, we extend the above result to get an Ω(n²/log n) size lower bound. As a consequence, we demonstrate that there exists an n-variate polynomial computable by n^{1 + o(1)}-sized formulas such that any multi-output planar circuit (resp., multi-output formula) simultaneously computing all its first-order partial derivatives requires size Ω(n^{4/3}) (resp., Ω(n²/log n)). This shows that a statement analogous to that of Baur, Strassen[Walter Baur and Volker Strassen, 1983] does not hold in the case of planar circuits and formulas.
Cite as

C. Ramya and Pratik Shastri. Lower Bounds for Planar Arithmetic Circuits. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 91:1-91:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ramya_et_al:LIPIcs.ITCS.2024.91,
  author =	{Ramya, C. and Shastri, Pratik},
  title =	{{Lower Bounds for Planar Arithmetic Circuits}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{91:1--91:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-309-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{287},
  editor =	{Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.91},
  URN =		{urn:nbn:de:0030-drops-196199},
  doi =		{10.4230/LIPIcs.ITCS.2024.91},
  annote =	{Keywords: Arithmetic circuit complexity, Planar circuits, Bilinear forms}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.11
Monotone Classes Beyond VNP

Authors: Prerona Chatterjee, Kshitij Gajjar, and Anamay Tengse

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

Abstract
In this work, we study the natural monotone analogues of various equivalent definitions of VPSPACE: a well studied class (Poizat 2008, Koiran & Perifel 2009, Malod 2011, Mahajan & Rao 2013) that is believed to be larger than VNP. We observe that these monotone analogues are not equivalent unlike their non-monotone counterparts, and propose monotone VPSPACE (mVPSPACE) to be defined as the monotone analogue of Poizat’s definition. With this definition, mVPSPACE turns out to be exponentially stronger than mVNP and also satisfies several desirable closure properties that the other analogues may not. Our initial goal was to understand the monotone complexity of transparent polynomials, a concept that was recently introduced by Hrubeš & Yehudayoff (2021). In that context, we show that transparent polynomials of large sparsity are hard for the monotone analogues of all the known definitions of VPSPACE, except for the one due to Poizat.
Cite as

Prerona Chatterjee, Kshitij Gajjar, and Anamay Tengse. Monotone Classes Beyond VNP. 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. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.FSTTCS.2023.11,
  author =	{Chatterjee, Prerona and Gajjar, Kshitij and Tengse, Anamay},
  title =	{{Monotone Classes Beyond VNP}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{11:1--11:23},
  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.11},
  URN =		{urn:nbn:de:0030-drops-193846},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.11},
  annote =	{Keywords: Algebraic Complexity, Monotone Computation, VPSPACE, Transparent Polynomials}
}
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
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2023.37
Brief Announcement: Relations Between Space-Bounded and Adaptive Massively Parallel Computations

Authors: Michael Chen, A. Pavan, and N. V. Vinodchandran

Published in: LIPIcs, Volume 281, 37th International Symposium on Distributed Computing (DISC 2023)

Abstract
In this work, we study the class of problems solvable by (deterministic) Adaptive Massively Parallel Computations in constant rounds from a computational complexity theory perspective. A language L is in the class AMPC⁰ if, for every ε > 0, there is a deterministic AMPC algorithm running in constant rounds with a polynomial number of processors, where the local memory of each machine s = O(N^ε). We prove that the space-bounded complexity class ReachUL is a proper subclass of AMPC⁰. The complexity class ReachUL lies between the well-known space-bounded complexity classes Deterministic Logspace (DLOG) and Nondeterministic Logspace (NLOG). In contrast, we establish that it is unlikely that PSPACE admits AMPC algorithms, even with polynomially many rounds. We also establish that showing PSPACE is a subclass of nonuniform-AMPC with polynomially many rounds leads to a significant separation result in complexity theory, namely PSPACE is a proper subclass of EXP^{Σ₂^{𝖯}}.
Cite as

Michael Chen, A. Pavan, and N. V. Vinodchandran. Brief Announcement: Relations Between Space-Bounded and Adaptive Massively Parallel Computations. In 37th International Symposium on Distributed Computing (DISC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 281, pp. 37:1-37:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.DISC.2023.37,
  author =	{Chen, Michael and Pavan, A. and Vinodchandran, N. V.},
  title =	{{Brief Announcement: Relations Between Space-Bounded and Adaptive Massively Parallel Computations}},
  booktitle =	{37th International Symposium on Distributed Computing (DISC 2023)},
  pages =	{37:1--37:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-301-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{281},
  editor =	{Oshman, Rotem},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2023.37},
  URN =		{urn:nbn:de:0030-drops-191634},
  doi =		{10.4230/LIPIcs.DISC.2023.37},
  annote =	{Keywords: Massively Parallel Computation, AMPC, Complexity Classes, LogSpace, NL, PSPACE}
}
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.2023.1
Algorithms Transcending the SAT-Symmetry Interface

Authors: Markus Anders, Pascal Schweitzer, and Mate Soos

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

Abstract
Dedicated treatment of symmetries in satisfiability problems (SAT) is indispensable for solving various classes of instances arising in practice. However, the exploitation of symmetries usually takes a black box approach. Typically, off-the-shelf external, general-purpose symmetry detection tools are invoked to compute symmetry groups of a formula. The groups thus generated are a set of permutations passed to a separate tool to perform further analyzes to understand the structure of the groups. The result of this second computation is in turn used for tasks such as static symmetry breaking or dynamic pruning of the search space. Within this pipeline of tools, the detection and analysis of symmetries typically incurs the majority of the time overhead for symmetry exploitation. In this paper we advocate for a more holistic view of what we call the SAT-symmetry interface. We formulate a computational setting, centered around a new concept of joint graph/group pairs, to analyze and improve the detection and analysis of symmetries. Using our methods, no information is lost performing computational tasks lying on the SAT-symmetry interface. Having access to the entire input allows for simpler, yet efficient algorithms. Specifically, we devise algorithms and heuristics for computing finest direct disjoint decompositions, finding equivalent orbits, and finding natural symmetric group actions. Our algorithms run in what we call instance-quasi-linear time, i.e., almost linear time in terms of the input size of the original formula and the description length of the symmetry group returned by symmetry detection tools. Our algorithms improve over both heuristics used in state-of-the-art symmetry exploitation tools, as well as theoretical general-purpose algorithms.
Cite as

Markus Anders, Pascal Schweitzer, and Mate Soos. Algorithms Transcending the SAT-Symmetry Interface. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.SAT.2023.1,
  author =	{Anders, Markus and Schweitzer, Pascal and Soos, Mate},
  title =	{{Algorithms Transcending the SAT-Symmetry Interface}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{1:1--1:21},
  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.1},
  URN =		{urn:nbn:de:0030-drops-184635},
  doi =		{10.4230/LIPIcs.SAT.2023.1},
  annote =	{Keywords: boolean satisfiability, symmetry exploitation, computational group theory}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.2
Proof Complexity of Propositional Model Counting

Authors: Olaf Beyersdorff, Tim Hoffmann, and Luc Nicolas Spachmann

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

Abstract
Recently, the proof system MICE for the model counting problem #SAT was introduced by Fichte, Hecher and Roland (SAT'22). As demonstrated by Fichte et al., the system MICE can be used for proof logging for state-of-the-art #SAT solvers. We perform a proof-complexity study of MICE. For this we first simplify the rules of MICE and obtain a calculus MICE' that is polynomially equivalent to MICE. Our main result establishes an exponential lower bound for the number of proof steps in MICE' (and hence also in MICE) for a specific family of CNFs.
Cite as

Olaf Beyersdorff, Tim Hoffmann, and Luc Nicolas Spachmann. Proof Complexity of Propositional Model Counting. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.SAT.2023.2,
  author =	{Beyersdorff, Olaf and Hoffmann, Tim and Spachmann, Luc Nicolas},
  title =	{{Proof Complexity of Propositional Model Counting}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{2:1--2:18},
  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.2},
  URN =		{urn:nbn:de:0030-drops-184647},
  doi =		{10.4230/LIPIcs.SAT.2023.2},
  annote =	{Keywords: model counting, #SAT, proof complexity, proof systems, lower bounds}
}
  • Refine by Author
  • 23 Mahajan, Meena
  • 7 Beyersdorff, Olaf
  • 4 Szeider, Stefan
  • 3 Biere, Armin
  • 3 Dahiya, Yogesh
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 10 QBF
  • 10 proof complexity
  • 8 resolution
  • 5 CDCL
  • 5 Complexity
  • Show More...

  • Refine by Type
  • 104 document
  • 2 volume

  • Refine by Publication Year
  • 46 2010
  • 38 2023
  • 4 2024
  • 3 2016
  • 3 2020
  • Show More...

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 About DROPS Imprint Privacy Contact