2 Search Results for "Mouli, Sasank"

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 Author
  • 2 Mouli, Sasank
  • 1 Dahiya, Yogesh
  • 1 Impagliazzo, Russell
  • 1 Mahajan, Meena
  • 1 Pitassi, Toniann

  • Refine by Classification
  • 2 Theory of computation → Proof complexity

  • Refine by Keyword
  • 2 Polynomial Calculus
  • 1 AC⁰[p]-Frege
  • 1 Algebraic proof systems
  • 1 Extension variables
  • 1 Fourier basis
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2023
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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