104 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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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
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-dev.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}
}
Document
CadiBack: Extracting Backbones with CaDiCaL

Authors: Armin Biere, Nils Froleyks, and Wenxi Wang

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


Abstract
The backbone of a satisfiable formula is the set of literals that are true in all its satisfying assignments. Backbone computation can improve a wide range of SAT-based applications, such as verification, fault localization and product configuration. In this tool paper, we introduce a new backbone extraction tool called CadiBack. It takes advantage of unique features available in our state-of-the-art SAT solver CaDiCaL including transparent inprocessing and single clause assumptions, which have not been evaluated in this context before. In addition, CaDiCaL is enhanced with an improved algorithm to support model rotation by utilizing watched literal data structures. In our comprehensive experiments with a large number of benchmarks, CadiBack solves 60% more instances than the state-of-the-art backbone extraction tool MiniBones. Our tool is thoroughly tested with fuzzing, internal correctness checking and cross-checking on a large benchmark set. It is publicly available as open source, well documented and easy to extend.

Cite as

Armin Biere, Nils Froleyks, and Wenxi Wang. CadiBack: Extracting Backbones with CaDiCaL. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 3:1-3:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{biere_et_al:LIPIcs.SAT.2023.3,
  author =	{Biere, Armin and Froleyks, Nils and Wang, Wenxi},
  title =	{{CadiBack: Extracting Backbones with CaDiCaL}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{3:1--3:12},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.3},
  URN =		{urn:nbn:de:0030-drops-184655},
  doi =		{10.4230/LIPIcs.SAT.2023.3},
  annote =	{Keywords: Satisfiability, Backbone, Incremental Solving}
}
Document
QCDCL vs QBF Resolution: Further Insights

Authors: Benjamin Böhm and Olaf Beyersdorff

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


Abstract
We continue the investigation on the relations of QCDCL and QBF resolution systems. In particular, we introduce QCDCL versions that tightly characterise QU-Resolution and (a slight variant of) long-distance Q-Resolution. We show that most QCDCL variants - parameterised by different policies for decisions, unit propagations and reductions - lead to incomparable systems for almost all choices of these policies.

Cite as

Benjamin Böhm and Olaf Beyersdorff. QCDCL vs QBF Resolution: Further Insights. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{bohm_et_al:LIPIcs.SAT.2023.4,
  author =	{B\"{o}hm, Benjamin and Beyersdorff, Olaf},
  title =	{{QCDCL vs QBF Resolution: Further Insights}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{4:1--4:17},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.4},
  URN =		{urn:nbn:de:0030-drops-184660},
  doi =		{10.4230/LIPIcs.SAT.2023.4},
  annote =	{Keywords: QBF, CDCL, resolution, proof complexity, simulations, lower bounds}
}
  • Refine by Author
  • 22 Mahajan, Meena
  • 7 Beyersdorff, Olaf
  • 4 Szeider, Stefan
  • 3 Biere, Armin
  • 3 Kirchweger, Markus
  • Show More...

  • Refine by Classification
  • 11 Theory of computation → Automated reasoning
  • 11 Theory of computation → Proof complexity
  • 6 Theory of computation → Algebraic complexity theory
  • 5 Theory of computation → Logic and verification
  • 4 Hardware → Theorem proving and SAT solving
  • Show More...

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

  • Refine by Type
  • 102 document
  • 2 volume

  • Refine by Publication Year
  • 46 2010
  • 38 2023
  • 3 2016
  • 3 2020
  • 2 2017
  • 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