我們展示了從參數化複雜度到證明複雜度的核化和資料簡化概念的應用:具體地，我們證明了具有(a).一個小長度約簡鍊的參數化問題的資料約簡規則的存在性，以及(b)證明約簡步驟完備性的小尺寸(擴充)弗雷格證明暗示了該問題命題形式化的次指數尺寸(擴充)弗雷格證明的存在性。
我們将所得結果應用于次指數弗雷格的存在性的推導，并對各種問題進行了弗雷格證明的推廣。改進了Aisenberg et al. (ICALP 2015)的早期結果，我們證明了表示Kneser-Lovász定理(一種更強形式)的命題公式對于參數k的每個常值都有多項式大小的Frege證明。以前隻有拟多項式的界是已知的(而且隻有普通的Kneser-Lovász定理)。
我們的架構的另一個值得注意的應用是計算社會選擇中的不可能結果:我們證明，對于任何固定數量的代理，阿羅和吉巴德-薩特思韋特不可能定理的命題平移具有次指數大小的弗雷格證明。
原文題目：Kernelization, Proof Complexity and Social Choice
原文：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 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ász 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.
核心化、證明複雜性和社交選擇.pdf