Proof complexity and the P vs. NP problem
Jan Krajicek

Course code: NALG139 (winter semester of 2011/12)
Time and place: see the special semester page.

Student logic seminar.


The course is concerned with the so called Cook's program which reduces the P vs. NP problem to the task to prove lengths-of-proofs lower bounds for propositional proofs. Even partial advances in the program have various consequences (e.g. for automated theorem proving or in mathematical logic).

A variety of formal systems for proving propositional tautologies fall under a general definition of a propositional proof system by Cook and Reckhow. The main problem is whether there exists such a proof system in which any tautology admits a proof of the length bounded above by a polynomial in the length of the tautology. This problem is equivalent to the question whether the computational complexity class NP is closed under complementation. The negative answer would imply that P and NP differ.

The lectures will concentrate on lengths-of-proofs lower bounds. We will present some known lower bounds for various proof systems and the methods used, but the core of the lectures will be in discussing possible approaches towards new lower bounds.

Some past courses (in 1996, 1997a and 1997b, 1999, 2003, 2005 and 2011) offer a related material and references.

Prerequisites:

I shall expect that the participants of the course are familiar with basic concepts of mathematical logic and of computational complexity theory on an undergraduate level (e.g., formal logical systems, p-time computations, NP-completeness, boolean circuits).

Approximate syllabus:

Part 1: Basic concepts and examples

  • Cook-Reckhow proof systems, (p)-simulation, links to NP vs. coNP problem.

  • Examples of proof systems: logical (Frege systems, resolution, ER, EF, SF), algebraic (polynomial calculus, NS, group-based), geometric (cutting planes, LS), auxiliary (implicit proof systems, from a first-order theory, ... ).

    Part 2: The provability of the soundness of algorithms and proof systems, and (p)-simulations

  • Translation of coNP properties into propositional logic.

  • Soundness of SAT algorithms and of proof systems, its provability and (p)-simulations.

  • Consequences of lengths-of-proof lower bounds:
    - time lower bounds,
    - the consistency of P \neq NP,
    - explicit examples of hard instances, both satisfiable as well as unsatisfiable.

  • Translation of b.arithmetic proofs into sequences of short propositional proofs.

  • The existence of an optimal proof system, links to other topics (e.g. finitistic Godel's thm, structural complexity, optimal SAT algorithms,...).
    [this topic may be touched only if we are running out of time]

    Part 3: Lower bound methods

  • Overview of the methods and of their shortcomings.

  • Feasible interpolation, its links to automatizability and possible generalizations.

  • Diagonalization in proof complexity.
    [if time permits]

    Part 4: Proof complexity generators

  • Basic concepts, facts, and examples.

  • NW generator, strengthened Razborov's conjecture and its consistency. Possible improvements.

  • Relevant model theory of bounded arithmetic.
    [if time permits]

    References

    References below will be updated throughout the semester to reflect what was actually covered.

    References for Part 1

    Books and lecture notes:
    My 1995 book and the lecture notes listed below contain essentially all material covered in Parts 1 and 2 (with the exceptions of some examples of proof systems - these are in the 2005 surveys - and of the applications of reflection principles to SAT algorithms).

  • S.A.Cook, a set of lecture notes, (1973).

  • S.A.Cook and P.Nguyen, Logical Foundations of Proof Complexity, Cambridge U.Press, 2010.

  • J.Krajicek, Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, (1995).

  • J.Krajicek, Forcing with random variables and proof complexity, CUP, 2011.
    [Chpt.27 overviews some of proof complexity]

  • J.Krajicek, Propositional proof complexity I. a Proof complexity and arithmetic, two sets of lecture notes.
    Papers:
  • Sam Buss, Towards NP-P via Proof Complexity and Search, preliminary manuscript. 2009.

  • S.A.Cook, The Complexity of Theorem Proving Procedures, Proc. of the 3rd Annual ACM Symposium on Theory of Computing, pp.151-158, (May 1971).

  • S.A.Cook and R.A.Reckhow, The Relative Efficiency of Propositional Proof Systems, J. Symbolic Logic, 44(1), pp.36-50, (1979). Their older paper.

  • J.Krajicek, "Proof complexity, in: Laptev, A. (ed.), European congress of mathematics (ECM), Stockholm, Sweden, June 27--July 2, 2004. Zurich: European Mathematical Society, (2005), pp.221-231. Pdf file.

  • J.Krajicek, "Hardness assumptions in the foundations of theoretical computer science", Archive for Mathematical Logic, 44(6)}, (2005), pp.667-675.
    Pdf file.

  • J.Krajicek, "From feasible proofs to feasible computations", in: Computer Science Logic 2010, A. Dawar and H. Veith (Eds.), LNCS 6247, Springer, Heidelberg (2010), pp.22-31.
    [contains overview of witnessing, propositional translation done a bit differently, feasible interpolation, etc.]

  • P. Pudlak: The lengths of proofs, in Handbook of Proof Theory, S.R. Buss ed., Elsevier, 1998, pp.547-637.

    References specific to Part 2:

  • S.A.Cook, Feasibly constructive proofs and the propositional calculus , Proc. of 7th annual ACM symposium on Theory of computing, Albuerque, New Mexico, pp.83-97, (1975).

  • S.A.Cook and J.Krajicek, Consequences of the provability of NP \subseteq P/poly, 72(4), (2007), pp. 1353-1371.

  • J.Krajicek and P.Pudlak: "Propositional Proof Systems, the Consistency of First Order Theories and the Complexity of Computations", J. Symbolic Logic, 54(3), (1989), pp. 1063-1079.
    [This introduces and discusses the problem of the existence of an optimal proof system, including the links to finitistic Godel's thm. References about the finitistic Godels' thm can be found among the references for my Spring 2011 course.]

    References for Part 3:

  • J.Krajicek, "Lower Bounds to the Size of Constant-Depth Propositional Proofs", J. of Symbolic Logic, 59(1), (1994), pp.73-86.

  • J.Krajicek, "On methods for proving lower bounds in propositional logic", in: {\em Logic and Scientific Methods} Eds. M. L. Dalla Chiara et al., (Vol. 1 of Proc. of the Tenth International Congress of Logic, Methodology and Philosophy of Science, Florence (August 19-25, 1995)), Synthese Library, Vol.259, Kluwer Academic Publ., Dordrecht, (1997), pp.69-83.

  • J.Krajicek, "Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic", J. of Symbolic Logic, {\bf 62(2)}, (1997), pp.457-486.

  • J.Krajicek, Diagonalization in proof complexity, Fundamenta Mathematicae, 182, (2004), pp.181-192. (preprint: ECCC

  • J.Krajicek, A form of feasible interpolation for constant depth Frege systems , J. of Symbolic Logic, 75(2), (2010), pp. 774-784. Pdf file.

  • J.Krajicek a P.Pudlak: Some consequences of cryptographical conjectures for $S^1_2$ and $EF$", Information and Computation, Vol.140(1), (1998), pp.82-94.

  • P. Pudlak: Lower bounds for resolution and cutting planes proofs and monotone computations, J. of Symb. Logic 62(3), 1997, pp.981-998.

  • P.Pudlak: On reducibility and symmetry of disjoint NP-pairs, Theor.Comput.Science, 295, (2003), pp.323-339.

    References for Part 4:

    My 2011 book (see above for a link) contains a survey of proof complexity generators in Chpts 29 and 30, as well as references to all papers on the topic. Below I list only those containing the material covered in the lectures.

  • M. Alekhnovich, E. Ben-Sasson, A.A.Razborov, and A. Wigderson, Pseudorandom Generators in Propositional Proof Complexity, SIAM Journal on Computing, Vol. 34(1) (2004) pp.67-88.

  • J.Krajicek, "On the weak pigeonhole principle", Fundamenta Mathematicae, Vol.170(1-3), (2001), pp.123-140.

  • J.Krajicek, Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds , J. of Symbolic Logic, 69(1), (2004), pp.265-286.

  • A proof complexity generator, in: Logic, Methodology and Philosophy of Science: Proc. of the 13th International Congress, Eds. Clark Glymour, Wei Wang, and Dag Westerstahl, College Publications, London, (2009), pp.185-190.
    ISBN-13: 978-1-904987-45-1. Pdf file.

  • J.Krajicek, On the proof complexity of the Nisan-Wigderson generator based on a hard NP \cap coNP function,
    J. of Mathematical Logic, Vol.11 (1), (2011), pp.11-27.

  • A.A.Razborov, Pseudorandom Generators Hard for k-DNF Resolution and Polynomial Calculus Resolution, preprint 2002-2003.