DROPS

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

DOI: 10.4230/LIPIcs.ICALP.2021.135

Kernelization, Proof Complexity and Social Choice

Authors: Gabriel Istrate, Cosmin Bonchiş, and Adrian Crăciun

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract

We display an application of the notions of kernelization and data reduction from parameterized complexity to proof complexity: Specifically, we show that the existence of data reduction rules for a parameterized problem having (a). a small-length reduction chain, and (b). small-size (extended) Frege proofs certifying the soundness of reduction steps implies the existence of subexponential size (extended) Frege proofs for propositional formalizations of the given problem. We apply our result to infer the existence of subexponential Frege and extended Frege proofs for a variety of problems. Improving earlier results of Aisenberg et al. (ICALP 2015), we show that propositional formulas expressing (a stronger form of) the Kneser-Lovász Theorem have quasipolynomial size Frege proofs for each constant value of the parameter k. Another notable application of our framework is to impossibility results in computational social choice: we show that, for any fixed number of agents, propositional translations of the Arrow and Gibbard-Satterthwaite impossibility theorems have subexponential size Frege proofs.

Cite as

Gabriel Istrate, Cosmin Bonchiş, and Adrian Crăciun. Kernelization, Proof Complexity and Social Choice. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 135:1-135:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{istrate_et_al:LIPIcs.ICALP.2021.135,
  author =	{Istrate, Gabriel and Bonchi\c{s}, Cosmin and Cr\u{a}ciun, Adrian},
  title =	{{Kernelization, Proof Complexity and Social Choice}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{135:1--135:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.135},
  URN =		{urn:nbn:de:0030-drops-142043},
  doi =		{10.4230/LIPIcs.ICALP.2021.135},
  annote =	{Keywords: Kernelization, Frege proofs, Kneser-Lov\'{a}sz Theorem, Arrow’s theorem, Gibbard-Satterthwaite theorem}
}

Search Results

Documents authored by Bonchiş, Cosmin

Kernelization, Proof Complexity and Social Choice

Abstract

Cite as

Thanks for your feedback!

Could not send message