2 Search Results for "Miksa, Mladen"

Document
DOI: 10.4230/LIPIcs.CCC.2015.467
A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds

Authors: Mladen Miksa and Jakob Nordström

Published in: LIPIcs, Volume 33, 30th Conference on Computational Complexity (CCC 2015)

Abstract
We study the problem of establishing lower bounds for polynomial calculus (PC) and polynomial calculus resolution (PCR) on proof degree, and hence by [Impagliazzo et al. '99] also on proof size. [Alekhnovich and Razborov '03] established that if the clause-variable incidence graph of a CNF formula F is a good enough expander, then proving that F is unsatisfiable requires high PC/PCR degree. We further develop the techniques in [AR03] to show that if one can "cluster" clauses and variables in a way that "respects the structure" of the formula in a certain sense, then it is sufficient that the incidence graph of this clustered version is an expander. As a corollary of this, we prove that the functional pigeonhole principle (FPHP) formulas require high PC/PCR degree when restricted to constant-degree expander graphs. This answers an open question in [Razborov '02], and also implies that the standard CNF encoding of the FPHP formulas require exponential proof size in polynomial calculus resolution.
Cite as

Mladen Miksa and Jakob Nordström. A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds. In 30th Conference on Computational Complexity (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 33, pp. 467-487, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{miksa_et_al:LIPIcs.CCC.2015.467,
  author =	{Miksa, Mladen and Nordstr\"{o}m, Jakob},
  title =	{{A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds}},
  booktitle =	{30th Conference on Computational Complexity (CCC 2015)},
  pages =	{467--487},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-81-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{33},
  editor =	{Zuckerman, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2015.467},
  URN =		{urn:nbn:de:0030-drops-50775},
  doi =		{10.4230/LIPIcs.CCC.2015.467},
  annote =	{Keywords: proof complexity, polynomial calculus, polynomial calculus resolution, PCR, degree, size, functional pigeonhole principle, lower bound}
}
Document
DOI: 10.4230/LIPIcs.STACS.2014.300
From Small Space to Small Width in Resolution

Authors: Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström, and Marc Vinyals

Published in: LIPIcs, Volume 25, 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)

Abstract
In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools from finite model theory. We give an alternative, completely elementary, proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexity measure that works against any resolution refutation -- previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.
Cite as

Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström, and Marc Vinyals. From Small Space to Small Width in Resolution. In 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 25, pp. 300-311, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{filmus_et_al:LIPIcs.STACS.2014.300,
  author =	{Filmus, Yuval and Lauria, Massimo and Miksa, Mladen and Nordstr\"{o}m, Jakob and Vinyals, Marc},
  title =	{{From Small Space to Small Width in Resolution}},
  booktitle =	{31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)},
  pages =	{300--311},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-65-1},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{25},
  editor =	{Mayr, Ernst W. and Portier, Natacha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2014.300},
  URN =		{urn:nbn:de:0030-drops-44661},
  doi =		{10.4230/LIPIcs.STACS.2014.300},
  annote =	{Keywords: proof complexity, resolution, width, space, polynomial calculus, PCR}
}
  • Refine by Author
  • 2 Miksa, Mladen
  • 2 Nordström, Jakob
  • 1 Filmus, Yuval
  • 1 Lauria, Massimo
  • 1 Vinyals, Marc

  • Refine by Classification

  • Refine by Keyword
  • 2 PCR
  • 2 polynomial calculus
  • 2 proof complexity
  • 1 degree
  • 1 functional pigeonhole principle
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2014
  • 1 2015

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