Document Open Access Logo

Kernelization, Proof Complexity and Social Choice

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

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.135.pdf
  • Filesize: 0.76 MB
  • 21 pages

Document Identifiers

Author Details

Gabriel Istrate
  • West University of Timişoara, Romania
Cosmin Bonchiş
  • West University of Timişoara, Romania
Adrian Crăciun
  • West University of Timişoara, Romania

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.ICALP.2021.135

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Kernelization
  • Frege proofs
  • Kneser-Lovász Theorem
  • Arrow’s theorem
  • Gibbard-Satterthwaite theorem

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. James Aisenberg, Maria Luisa Bonet, and Sam Buss. Quasipolynomial size Frege proofs of Frankl’s theorem on the trace of sets. Journal of Symbolic Logic, 81(2):687-710, 2016. Google Scholar
  2. James Aisenberg, Maria Luisa Bonet, Sam Buss, Adrian Crăciun, and Gabriel Istrate. Short proofs of the Kneser-Lovász coloring principle. Information and Computation, 261:296-310, 2018. Google Scholar
  3. E. Babson and D.N. Kozlov. Proof of the Lovász conjecture. Annals of Mathematics, 165:965-1007, 2007. Google Scholar
  4. Yuliy M Baryshnikov. Topological and discrete social choice: in a search of a theory. In Topological social choice, pages 53-63. Springer, 1997. Google Scholar
  5. Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, and Alexander A Razborov. Parameterized bounded-depth Frege is not optimal. ACM Transactions on Computation Theory (TOCT), 4(3):1-16, 2012. Google Scholar
  6. Maria Luisa Bonet, Samuel R Buss, and Toniann Pitassi. Are there hard examples for Frege systems? In Feasible Mathematics II, pages 30-56. Birkhäuser Boston, 1995. Google Scholar
  7. Felix Brandt, Vincent Conitzer, Ulle Endriss, Jérôme Lang, and Ariel D Procaccia. Handbook of computational social choice. Cambridge University Press, 2016. Google Scholar
  8. S. Buss. Polynomial size proofs of the propositional pigeonhole principle. Journal of Symbolic Logic, 52(4):916-927, 1987. Google Scholar
  9. Sam Buss. Quasipolynomial size proofs of the propositional pigeonhole principle. Theoretical Computer Science, 576:77-84, 2015. Google Scholar
  10. Sam Buss and Jakob Nordström. Proof complexity and SAT solving. Chapter to appear in the 2nd edition of Handbook of Satisfiability, 2021. Draft version available at URL: https://www.math.ucsd.edu/~sbuss/ResearchWeb/ProofComplexitySAT.
  11. Lorenzo Carlucci, Nicola Galesi, and Massimo Lauria. Paris-Harrington tautologies. In 2011 IEEE 26th Annual Conference on Computational Complexity, pages 93-103, 2011. Google Scholar
  12. Graciela Chichilnisky. Social choice and the topology of spaces of preferences. Advances in Mathematics, 37(2):165-176, 1980. Google Scholar
  13. Graciela Chichilnisky. The topological equivalence of the Pareto condition and the existence of a dictator. Journal of Mathematical Economics, 9(3):223-233, 1982. Google Scholar
  14. Giovanni Ciná and Ulle Endriss. A syntactic proof of Arrow’s theorem in a modal logic of social choice functions. In Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, pages 1009-1017, 2015. Google Scholar
  15. Stephen A Cook and Robert A Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  16. Stefan Dantchev, Barnaby Martin, and Stefan Szeider. Parameterized proof complexity. Computational Complexity, 20(1):51, 2011. Google Scholar
  17. M. de Longueville. A Course in Topological Combinatorics. Springer, 2012. Google Scholar
  18. Rodney G Downey and Michael R Fellows. Fundamentals of parameterized complexity. Springer, 2013. Google Scholar
  19. Fedor V Fomin, Daniel Lokshtanov, Saket Saurabh, and Meirav Zehavi. Kernelization: theory of parameterized preprocessing. Cambridge University Press, 2019. Google Scholar
  20. Fedor V Fomin, Daniel Lokshtanov, Saket Saurabh, and Meirav Zehavi. Parameterized algorithms. Beyond the Worst-Case Analysis of Algorithms, page 27, 2020. Google Scholar
  21. Christian Geist and Ulrich Endriss. Automated search for impossibility theorems in social choice theory: Ranking sets of objects. Journal of Artificial Intelligence Research, 40:143-174, 2011. Google Scholar
  22. Christian Geist and Dominik Peters. Computer-aided methods for social choice theory. Trends in Computational Social Choice, pages 249-267, 2017. Google Scholar
  23. Umberto Grandi and Ulle Endriss. First-order logic formalisation of Arrow’s theorem. In International Workshop on Logic, Rationality and Interaction, pages 133-146. Springer, 2009. Google Scholar
  24. Pavel Hrubes and Iddo Tzameret. Short proofs for the determinant identities. SIAM Journal on Computing, 44(2):340-383, 2015. Google Scholar
  25. G. Istrate, A. Percus, and S. Boettcher. Spines of random constraint satisfaction problems: Definition and connection with computational complexity. Annals of Mathematics and Artificial Intelligence, 44(4):353-372, 2005. Google Scholar
  26. Gabriel Istrate, Cosmin Bonchis, and Adrian Craciun. Kernelization, proof complexity and social choice, 2021. URL: http://arxiv.org/abs/2104.13681.
  27. Gabriel Istrate and Adrian Craciun. Proof complexity and the kneser-lovász theorem. In International Conference on Theory and Applications of Satisfiability Testing, pages 138-153. Springer, 2014. Google Scholar
  28. Leszek Aleksander Kołodziejczyk, Phuong Nguyen, and Neil Thapen. The provably total NP search problems of weak second order bounded arithmetic. Annals of Pure and Applied Logic, 162(6):419-446, 2011. Google Scholar
  29. D. Kozlov. Combinatorial Algebraic Topology. Springer Verlag, 2008. Google Scholar
  30. Jan Krajíček. Proof complexity, volume 170. Cambridge University Press, 2019. Google Scholar
  31. Massimo Lauria, Pavel Pudlák, Vojtěch Rödl, and Neil Thapen. The complexity of proving that a graph is Ramsey. Combinatorica, 37(2):253-268, 2017. Google Scholar
  32. L. Lovász. Kneser’s conjecture, chromatic number, and homotopy. Journal of Combinatorial Theory, Series A, 25:319-324, 1978. Google Scholar
  33. C. Moore, G. Istrate, D. Demopoulos, and M. Vardi. A continuous-discontinuous second-order transition in the satisfiability of a class of Horn formulas. Random Structures and Algorithms, 31(2):173-185, 2007. Google Scholar
  34. Akihiro Nozaki, Toshiyasu Arai, Noriko H Arai, et al. Polynomal-size Frege proofs of Bollobás' theorem on the trace of sets. Proceedings of the Japan Academy, Series A, Mathematical Sciences, 84(8):159-161, 2008. Google Scholar
  35. A. Schrijver. Vertex-critical subgraphs of Kneser graphs. Nieuw Arch. Wiskd., III. Ser., 26:454-461, 1978. Google Scholar
  36. Michael Soltys and Stephen Cook. The proof complexity of linear algebra. Annals of Pure and Applied Logic, 130(1-3):277-323, 2004. Google Scholar
  37. Pingzhong Tang and Fangzhen Lin. A computer-aided proof to Gibbard-Satterthwaite theorem. Technical report, Technical report, 2008. http://iiis.tsinghua.edu.cn/~kenshin, 2008.
  38. Pingzhong Tang and Fangzhen Lin. Computer-aided proofs of Arrow’s and other impossibility theorems. Artificial Intelligence, 173(11):1041-1053, 2009. Google Scholar
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 About DROPS Imprint Privacy Contact