Syllabus and literature for lectures on

Proof complexity and automated proof search Jan Krajicek

Kod predmetu: NMAG564

Studentsky logicky seminar.

The course is concerned with the complexity of automated proof search in propositional logic from the point of view of complexity theory; in particular, of proof complexity. The basic problem is how hard it is to find a proof of a formula in a given proof system (or in any proof system).

Syllabus (may evolve):

  • Cook-Reckhow proof systems, the lengths of proofs, the NP vs. coNP problem.

  • Polynomial simulation, the existence of an optimal proof system.

  • DPLL algorithms and resolution.

  • Provability of the correctness of a SAT algorithm and its simulation by a proof system.

  • Feasible counter-examples to SAT algorithms.

  • Automatizability of a proof system, feasible interpolation, disjoint NP pairs.

  • Automatizability and the existence of one-way permutations.

  • Constructing short propositional proofs via bounded arithmetic.

  • Non-automatizability of Extended Frege systems and of some weaker proof systems.

  • Quasi-polynomial automatizability of tree-like resolution and non-automatizability of general resolution.

  • Systems R(k) and generalized (weaker) automatizability.

  • Polynomail calculus.

  • The existence of short proofs of unsatisfiability of random 3DNF formulas of high density.

  • Heuristic automatizers.

    Bibliography (may evolve):

    Background

  • Sanjeev Arora a Boaz Barak, "Complexity Theory: A Modern Approach", book draft.

  • 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, a set of lecture notes, (1973).

  • 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.

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

  • 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.

  • Jan Krajicek, Propositional proof complexity I. a Proof complexity and arithmetic, dvoje skripta.

  • Alexander Nadel, Understanding and Improving a Modern SAT Solver. PhD thesis, (2009), Tel Aviv University.

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

    Technical texts

  • M.Alekhnovich a A.A.Razborov, Resolution is Not Automatizable Unless W[P] is Tractable, SIAM Journal on Computing, Vol. 38, No 4, (2008), pp.1347-1363.

  • A.Atserias a M. L. Bonet, On the Automatizability of Resolution and Related Propositional Proof Systems, Information and Computation, 189(2), (2004), pp.182-201.

  • Paul Beame and Toniann Pitassi, Simplified and improved resolution lower bounds. In Proceedings 37th Annual Symposium on Foundations of Computer Science, pages 274-282, Burlington, VT, October 1996. IEEE.

  • E.Ben-Sasson a A.Wigderson, Short Proofs are Narrow- Resolution made Simple, Journal of the ACM, 48(2), (2001).

  • Marķa Luisa Bonet, Toniann Pitassi, and Ran Raz, ``On Interpolation and Automatization for Frege Proof Systems'', SIAM Journal of Computing, 29 (6), (2000), pp.1939-1967.

  • Marķa Luisa Bonet, Carlos Domingo, Ricard Gavaldą, Alexis Maciel and Toniann Pitassi, ``Non-automatizability of Bounded-depth Frege Proofs'', Computational Complexity, 13, (2004), pp.47-68..

  • M.Clegg, J.Edmonds, and R.Impagliazzo, Using the Groebner basis algorithm to find proofs of unsatisfiability, In Proceedings of the Twenty-Eighth Annual ACM Symp. on Theory of Computing, (1996), pp.174-183.

  • 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.

  • U.Feige a E.Ofek, Easily refutable subformulas of large random 3CNF formulas, Th. of Comp., 3, (2007), pp.25-43.

  • Edward Hirsch, Dmitry Itsykson, Ivan Monakhov, Alexander Smal On optimal heuristic randomized semidecision procedures, with applications to proof complexity and cryptography, ECCC 2010.

  • 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, "On the weak pigeonhole principle", Fundamenta Mathematicae, Vol.170(1-3), (2001), pp.123-140.

  • J.Krajicek, Substitutions into propositional tautologies, Information Processing Letters, 101, (2007), pp.163-167.

  • 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.

  • Ashish Sabharwal, Algorithmic Applications of Propositional Proof Complexity, PH.D. THESIS, University of Washington, Seattle, 2005.