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.