Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style


Jan Pich

Faculty of Mathematics and Physics,
Charles University in Prague, 2011

Hard tautologies



We investigate the unprovability of NP $\not\subseteq$    P/poly in various fragments of arithmetic. The unprovability is usually obtained by showing hardness of propositional formulas encoding superpolynomial circuit lower bounds.
Firstly, we discuss few relevant techniques and known theorems. Namely, natural proofs, feasible interpolation, KPT theorem, iterability, gadget generators etc.
Then we prove some original results. We show the unprovability of superpolynomial circuit lower bounds for systems admitting certain forms of feasible interpolation (modulo a hardness assumption) and for systems roughly described as tree-like Frege systems working with formulas using only a small fraction of variables of the statement that is supposed to be proved.
These results are obtained by proving the hardness of the Nisan-Wigderson generators in corresponding proof systems.

Table of Contents

Introduction                                                        1
1. Bounded Arithmetic and Propositional proof systems               3
    1.1 Propositional proof systems                                 3
    1.2 Feasible provability                                        4
    1.3 Ajtai's method                                              6
2. Proof complexity generators                                      7
3. General strategy and known techniques                            8
    3.1 Natural proofs                                              8
    3.2 Feasible interpolation                                      9
    3.3 KPT theorem                                                 10
    3.4 Formulas hard for all proof systems                         11
    3.5 Iterability                                                 12
    3.6 Gadget generators                                           12
    3.7 The best known hardness result for circuit lower bounds     13
4. Nisan-Wigderson generators                                       15
    4.1 Previous results                                            16
    4.2 NW-generators in proof systems with EIP                     17
    4.3 NW-generators in strongly-sound local systems               20
5. NW-generators in strong proof systems                            23
    5.1 Interactive communication and KPT theorem                   24
    5.2 Collection schema                                           26

Conclusions                                                         27

References                                                          29

Number of pages: 36

ISSN 1433-8092 | Imprint