Propositional proof systems : efficiency and automatizability

The thesis considers two fundamental questions in propositional proof complexity: lower bounds on the size of the shortest proof and automatizability of propositional proof systems. With respect to the first part, we develop a new paradigm for proving lower bounds in propositional calculus. Our method is based on the purely computational concept of pseudorandom generator. Namely, we call a pseudorandom generator Gn: [0, 1 ] - [0, 1]m hard for a propositional proof system P if P cannot efficiently prove the (properly encoded) statement G (xl,...,xn) f b for any string b [0, 1]m. We consider a variety of "combinatorial" pseudorandom generators inspired by the Nisan-Wigderson generator on the one hand, and by the construction of Tseitin tautologies on the other. We prove that under certain circumstances these generators are hard for such proof systems as Resolution, Polynomial Calculus and Polynomial Calculus with Resolution (PCR). As to the second part, we prove that the problem of approximating the size of the shortest proof within factor 2log1-o(1) is NP-hard. This result is very robust in that it holds for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution, Horn resolution, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problem of approximating the length of proofs. Finally, we show that neither Resolution nor tree-like Resolution is automatizable unless the class W[P] from the hierarchy of parameterized problems is fixed-parameter tractable by randomized algorithms with one-sided error.

Department dc:contributor.department

Massachusetts Institute of Technology. Dept. of Mathematics.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2003

Author dc:creator

• Alekhnovitch, Mikhail, 1978-

Advisor dc:contributor.advisor

• Madhu Sudan.

• Mathematics.

Statement dc:rights

• M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/29344

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/29344