4 Search Results for "Mouli, Sasank"

Document
DOI: 10.4230/LIPIcs.ITCS.2026.99
AC⁰[p]-Frege Cannot Efficiently Prove That Constant-Depth Algebraic Circuit Lower Bounds Are Hard

Authors: Jiaqi Lu, Rahul Santhanam, and Iddo Tzameret

Published in: LIPIcs, Volume 362, 17th Innovations in Theoretical Computer Science Conference (ITCS 2026)

Abstract
We study whether lower bounds against constant-depth algebraic circuits computing the Permanent over finite fields (Limaye-Srinivasan-Tavenas [J. ACM, 2025] and Forbes [CCC'24]) are hard to prove in certain proof systems. We focus on a DNF formula that expresses that such lower bounds are hard for constant-depth algebraic proofs. Using an adaptation of the diagonalization framework of Santhanam and Tzameret (SIAM J. Comput., 2025), we show unconditionally that this family of DNF formulas does not admit polynomial-size propositional AC⁰[p]-Frege proofs, infinitely often. This rules out the possibility that the DNF family is easy, and establishes that its status is either that of a hard tautology for AC⁰[p]-Frege or else unprovable (i.e., not a tautology). While it remains open whether the DNFs in question are tautologies, we provide evidence in this direction. In particular, under the plausible assumption that certain (weak) properties of multilinear algebra - specifically, those involving tensor rank - do not admit short constant-depth algebraic proofs, the DNFs are tautologies. We also observe that several weaker variants of the DNF formula are provably tautologies, and we show that the question of whether the DNFs are tautologies connects to conjectures of Razborov (ICALP'96) and Krajíček (J. Symb. Log., 2004). Additionally, our result has the following special features: ii) Existential depth amplification: the DNF formula considered is parameterised by a constant depth d bounding the depth of the algebraic proofs. We show that there exists some fixed depth d such that if there are no small depth-d algebraic proofs of certain circuit lower bounds for the Permanent, then there are no such small algebraic proofs in any constant depth. iii) Necessity: We show that our result is a necessary step towards establishing lower bounds against constant-depth algebraic proofs, and more generally against any sufficiently strong proof system. In particular, showing there are no short proofs for our DNF formulas, obtained by replacing "constant-depth algebraic circuits" with any "reasonable" algebraic circuit class C, is necessary in order to prove any super-polynomial lower bounds against algebraic proofs operating with circuits from C.
Cite as

Jiaqi Lu, Rahul Santhanam, and Iddo Tzameret. AC⁰[p]-Frege Cannot Efficiently Prove That Constant-Depth Algebraic Circuit Lower Bounds Are Hard. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 99:1-99:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{lu_et_al:LIPIcs.ITCS.2026.99,
  author =	{Lu, Jiaqi and Santhanam, Rahul and Tzameret, Iddo},
  title =	{{AC⁰\lbrackp\rbrack-Frege Cannot Efficiently Prove That Constant-Depth Algebraic Circuit Lower Bounds Are Hard}},
  booktitle =	{17th Innovations in Theoretical Computer Science Conference (ITCS 2026)},
  pages =	{99:1--99:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-410-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{362},
  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.ITCS.2026.99},
  URN =		{urn:nbn:de:0030-drops-253865},
  doi =		{10.4230/LIPIcs.ITCS.2026.99},
  annote =	{Keywords: Complexity, Lower bounds, Proof complexity, AC⁰\lbrackp\rbrack-Frege, Diagonalisation, Algebraic complexity}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.6
An Algebraic Approach to MaxCSP

Authors: Ilario Bonacina and Jordi Levy

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Recently, there have been some attempts to base SAT and MaxSAT solvers on calculi beyond Resolution, even trying to solve SAT using MaxSAT proof systems. One of these directions was to perform MaxSAT sound inferences using polynomials over finite fields, extending the proof system Polynomial Calculus, which is known to be more powerful than Resolution. In this work, we extend the use of the Polynomial Calculus for optimization, showing its completeness over many-valued variables. This allows using a more direct and efficient encoding of CSP problems (e.g., k-Coloring) and solving the maximization version of the problem on such encoding (e.g., Max-k-Coloring).
Cite as

Ilario Bonacina and Jordi Levy. An Algebraic Approach to MaxCSP. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bonacina_et_al:LIPIcs.SAT.2025.6,
  author =	{Bonacina, Ilario and Levy, Jordi},
  title =	{{An Algebraic Approach to MaxCSP}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.6},
  URN =		{urn:nbn:de:0030-drops-237407},
  doi =		{10.4230/LIPIcs.SAT.2025.6},
  annote =	{Keywords: MaxCSP, Polynomial Calculus, MaxSAT}
}
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.CCC.2023.7
Lower Bounds for Polynomial Calculus with Extension Variables over Finite Fields

Authors: Russell Impagliazzo, Sasank Mouli, and Toniann Pitassi

Published in: LIPIcs, Volume 264, 38th Computational Complexity Conference (CCC 2023)

Abstract
For every prime p > 0, every n > 0 and κ = O(log n), we show the existence of an unsatisfiable system of polynomial equations over O(n log n) variables of degree O(log n) such that any Polynomial Calculus refutation over 𝔽_p with M extension variables, each depending on at most κ original variables requires size exp(Ω(n²)/10^κ(M + n log n))
Cite as

Russell Impagliazzo, Sasank Mouli, and Toniann Pitassi. Lower Bounds for Polynomial Calculus with Extension Variables over Finite Fields. In 38th Computational Complexity Conference (CCC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 264, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{impagliazzo_et_al:LIPIcs.CCC.2023.7,
  author =	{Impagliazzo, Russell and Mouli, Sasank and Pitassi, Toniann},
  title =	{{Lower Bounds for Polynomial Calculus with Extension Variables over Finite Fields}},
  booktitle =	{38th Computational Complexity Conference (CCC 2023)},
  pages =	{7:1--7:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-282-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{264},
  editor =	{Ta-Shma, Amnon},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2023.7},
  URN =		{urn:nbn:de:0030-drops-182774},
  doi =		{10.4230/LIPIcs.CCC.2023.7},
  annote =	{Keywords: Proof complexity, Algebraic proof systems, Polynomial Calculus, Extension variables, AC⁰\lbrackp\rbrack-Frege}
}
  • Refine by Type
  • 4 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 1 2024
  • 1 2023

  • Refine by Author
  • 2 Mouli, Sasank
  • 1 Bonacina, Ilario
  • 1 Dahiya, Yogesh
  • 1 Impagliazzo, Russell
  • 1 Levy, Jordi
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs

  • Refine by Classification
  • 4 Theory of computation → Proof complexity
  • 1 Computing methodologies → Algebraic algorithms
  • 1 Mathematics of computing → Solvers
  • 1 Theory of computation → Algebraic complexity theory
  • 1 Theory of computation → Proof theory

  • Refine by Keyword
  • 3 Polynomial Calculus
  • 2 AC⁰[p]-Frege
  • 2 Proof complexity
  • 1 Algebraic complexity
  • 1 Algebraic proof systems
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact