Syllabus for P. Pudlak's lectures at the
Fall school(Sept.'02)

Proof systems and integer linear programming

Heuristics for NP-complete problems can be interpreted as propositional proof systems. In integer linear programming a well known cutting plane procedure has been extensively studied and examples have been found that require exponentially many steps. For other systems only partial results are known, in particular, several systems possess the feasible interpolation property.

In this lecture we shall introduce some basic concepts and results in linear programming. Then we shall give a survey of proof systems that has been studied and prove some theorems about them.


  • L. Lovasz: On the Shannon capacity of graphs, IEEE Transactions on Information Theory 25, 1979
  • L.Lovasz: Semidefinite programs and combinatorial optimization.
  • L Lovasz and A. Schrijver: Cones of matrices and set-functions and 0-1 optimization, SIAM J. on Optimization 1, 1991
  • P. Pudlak: Lower bounds for resolution and cutting plane proofs and monotone computations, JSL 62, 1997.
  • P. Pudlak: On the complexity of propositional calculus, Logic Colloquium 1997, Cambridge 1999.
  • S. Dash: On the matrix cuts of Lovasz and Schrijver and their use in integer programming, PhD thesis, TR 01-08.