Kernelization, Proof Complexity and Social Choice

TL;DR

This paper connects kernelization and data reduction techniques from parameterized complexity to proof complexity, demonstrating that certain reductions lead to subexponential proofs in propositional logic, with applications to social choice and combinatorics.

Contribution

It introduces a framework linking data reduction rules to proof size bounds, improving bounds for the Kneser-Lovász Theorem and proving subexponential proofs for social choice impossibility theorems.

Findings

Polynomial size Frege proofs for fixed k in Kneser-Lovász Theorem.

Subexponential Frege proofs for Arrow and Gibbard-Satterthwaite theorems.

Extension of previous quasipolynomial bounds to polynomial bounds for certain cases.

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\'asz Theorem have polynomial size Frege proofs for each constant value of the parameter k. Previously only quasipolynomial bounds were known (and only for the ordinary Kneser-Lov\'asz Theorem). 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.