|
|
|
|
|
Proof Complexity
NP consists of those languages that have short, easily-verifiable proofs of
membership.
For any of our favorite NP-complete problems, such as satisfiability,
there is a dual problem, tautology in the case of satisfiability, that is
complete for co-NP.
Proof complexity is the study of the lengths of
easily-verifiable proofs for co-NP languages.
The `holy grail' of proof complexity is to prove that no short,
easily-verifiable proofs of tautology (or equivalently any other co-NP-complete
language) exist. This would have the consequence of separating NP from co-NP
and, as a result, separate P from NP.
At the heart of all automated theorem
provers is a search for proofs of propositional tautologies (even if they do not
express it in this way). Proof complexity analyzes what it
takes to simply write down the proofs that automated theorem-provers might find,
completely ignoring the computational effort required to find them -
essentially analyzing nondeterministic algorithms.
We have, for example, shown that for very natural statements involving
counting, simply writing down the proofs that could be found by any automated
theorem-provers employing the most widely-used methods: the Davis-Putnam
procedure, Resolution theorem-proving, or bounded-depth Frege proof systems,
must necessarily require exponentially time.
Proof complexity results also give insight into classes of deterministic
algorithms for NP-complete problems. The transcript of a failed search
of a graph 3-coloring algorithm, for example, provides an easily-verifiable
proof that the graph is not 3-colorable.
Different classes of algorithms yield such transcripts with particular
properties.
The classifications given by proof complexity and lower bounds on the sizes
of these proofs permit us to show that large classes of deterministic
algorithms require exponential time to solve the problems. For example,
we have shown that a wide-range of algorithms for graph 3-coloring
require exponential time on almost all graphs having average degree above
a small constant.
Finally, the study of proof complexity motivates the search for new and
more efficient proof methods. For example, we have developed new proof
systems, based on a result from algebra known as Hilbert's Nullstellensatz,
that both extend the range of cases for which we have efficient proofs
and have the property that finding a proof is not substantially more difficult
than writing it down.
Publications
- Paul Beame, Russell
Impagliazzo, Toniann Pitassi, and Nathan Segerlind.
Memoization and DPLL: Formula Caching proof systems.
Submitted to 2003 Computational Complexity Conference.
- Paul Beame, Henry Kautz, and
Ashish Sabharwal.
On the power of clause learning.
Submitted to IJCAI 2003.
- Paul Beame,
Richard Karp, Toniann Pitassi, and Michael Saks.
The
efficiency of resolution and Davis-Putnam procedures.
SIAM Journal on Computing, 31(4):1048-1075, 2002.
- Joshua
Buresh-Oppenheim, Paul Beame, Toniann Pitassi, Ran Raz, and Ashish Sabharwal.
Bounded-depth
Frege lower bounds for weaker pigeonhole principles.
In Proceedings 43rd Annual Symposium on Foundations of Computer
Science. IEEE, 2002.
To appear.
- Dimitris Achlioptas,
Paul Beame, and Michael Molloy.
A sharp threshold in proof complexity.
In Proceedings of the Thirty-Third Annual ACM Symposium on Theory of
Computing, pages 337-346, Heraklion, Crete, Greece, July 2001.
- Paul Beame, Joe Culberson, and
David Mitchell.
The resolution complexity of random graph k-colourability.
In preparation.
- Paul Beame and
Toniann Pitassi.
Propositional Proof Complexity: Past, Present, and Future.
In G. Paun, G. Rozenberg, and A. Salomaa, editors, Current Trends in
Theoretical Computer Science: Entering the 21st Century, pages 42-70.
World Scientific Publishing, 2001.
- Paul Beame, Russell
Impagliazzo, and Ashish Sabharwal.
The resolution complexity of the independent set problem in random graphs.
In Proceedings Sixteenth Annual IEEE Conference on Computational
Complexity, pages 52-68, Chicago, IL, June 2001.
- Paul Beame and
Samuel R. Buss, editors.
Proof Complexity and Feasible Arithmetics, volume 39 of
DIMACS Series in Discrete Mathematics and Theoretical Computer
Science.
American Mathematical Society, 1998.
- Paul Beame and
Toniann Pitassi.
Propositional Proof Complexity: Past, Present, and Future.
Bulletin of the European Association for Theoretical Computer
Science, 65:66-89, June 1998.
The Computational Complexity Column (ed. E. Allender).
- Paul Beame and Søren
Riis.
More on the
relative strength of counting principles.
In Paul W. Beame and Samuel R. Buss, editors, Proof Complexity and
Feasible Arithmetics, volume 39 of DIMACS Series in Discrete
Mathematics and Theoretical Computer Science, pages 13-35. American
Mathematical Society, 1998.
- Paul Beame,
Stephen A. Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi.
The relative complexity of NP search problems.
Journal of Computer and System Sciences, 57:3-19, 1998.
Special issue of invited papers from 1995 STOC conference.
- Paul Beame, Richard Karp,
Toniann Pitassi, and Michael Saks.
On the complexity of unsatisfiability of random k-CNF formulas.
In Proceedings of the 30th Annual ACM Symposium on Theory of
Computing, pages 561-571, Dallas, TX, May 1998.
- Paul Beame and
Toniann Pitassi.
An exponential separation between the parity principle and the pigeonhole
principle.
Annals of Pure and Applied Logic, 80:197-222, 1996.
- 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.
- Paul Beame,
Russell Impagliazzo, Jan Krajícek, Toniann Pitassi, and Pavel
Pudlák.
Lower bounds on Hilbert's Nullstellensatz and propositional proofs.
Proc. London Math. Soc., 73(3):1-26, 1996.
- Paul Beame, Stephen A.
Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi.
The relative complexity of NP search problems.
In Proceedings of the Twenty-Seventh Annual ACM Symposium on Theory of
Computing, pages 303-314, Las Vegas, NV, May 1995.
- Paul Beame, Russell
Impagliazzo, Jan Krajícek, Toniann Pitassi, and Pavel Pudlák.
Lower bounds
on Hilbert's Nullstellensatz and propositional proofs.
In Proceedings 35th Annual Symposium on Foundations of Computer
Science, pages 794-806, Santa Fe, NM, November 1994. IEEE.
- Paul Beame and Toniann
Pitassi.
An
exponential separation between the matching principle and the pigeonhole
principle.
In 8th Annual IEEE Symposium on Logic in Computer Science, pages
308-319, Montreal, Quebec, June 1993.
- Paul Beame and Toniann
Pitassi.
An exponential separation between the matching principle and the pigeonhole
principle.
Technical Report UW-CSE-93-04-07, Department of Computer Science and
Engineering, University of Washington, April 1993.
- Toniann Pitassi, Paul Beame,
and Russell Impagliazzo.
Exponential lower bounds for the pigeonhole principle.
Computational Complexity, 3(2):97-140, 1993.
- Paul Beame, Russell
Impagliazzo, Jan Krajícek, Toniann Pitassi, Pavel Pudlák, and
Alan Woods.
Exponential lower bounds for the pigeonhole principle.
In Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of
Computing, pages 200-220, Victoria, B.C., Canada, May 1992.
- Paul Beame, Russell
Impagliazzo, and Toniann Pitassi.
Exponential lower bounds for the pigeonhole principle.
Technical Report TR257/91, University of Toronto, Department of Computer
Science, 1991.
|
CSE Home
