[Computational Complexity] Resolving Dagstuhl
This week I am at the Dagstuhl seminar Complexity of Boolean Functions. Schloss Dagstuhl is an isolated conference center in Southwestern Germany that hosts weekly seminars in computer science. They have room and board at the center and it is difficult to go anywhere from here so we are forced to spend time with each other, a good thing for research.
Someone at the workshop pointed out that the STOC 2006 program has been posted and lists the award winners. The best student paper award is going to Anup Rao for Extractors for a Constant Number of Polynomial Min-Entropy Independent Sources and Jakob Nordström for Narrow Proofs May Be Spacious: Separating Space and Width in Resolution. The best paper award is (surprise, surprise) going to Irit Dinur for her PCP Theorem by Gap Amplification.
Nordström gave a talk on his paper Monday. A resolution proof of unsatisfiability of a CNF formula takes a clause containing x and another clause with the negation of x and resolves it into a clause containing the remaining variables of the first two clauses. A CNF formula is unsatisfiable iff there is a resolution proof that leads to the empty clause. In 1985, Haken showed that there are no polynomial-length resolution proofs for all unsatisfiable CNF formula.
The width of a proof is the size of the largest clause produced. The space of the proof is the number of clauses one needs to keep in memory. No immediately obvious reason that the two should be related but in fact the space is an upper bound on the width and conjectured to be the same up to constant factors. Nordström disproves the conjecture by giving a family of formulas where the width is constant but the space is not.
Posted by Lance to Computational Complexity at 3/14/2006 05:04:00 AM