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.