Proceedings of 37th Conference on Foundations of Computer Science (1996)
Oct. 14, 1996 to Oct. 16, 1996
P. Beame , Dept. of Comput. Sci. & Eng., Washington Univ., Seattle, WA, USA
T. Pitassi , Dept. of Comput. Sci. & Eng., Washington Univ., Seattle, WA, USA
We give simple new lower bounds on the lengths of resolution proofs for the pigeonhole principle and for randomly generated formulas. For random formulas, our bounds significantly extend the range of formula sizes for which non-trivial lower bounds are known. For example, we show that with probability approaching 1, any resolution refutation of a randomly chosen 3-CNF formula with at most n/sup 6/5-/spl epsiv// clauses requires exponential size. Previous bounds applied only when the number of clauses was at most linear in the number of variables. For the pigeonhole principle our bound is a small improvement over previous bounds. Our proofs are more elementary than previous arguments, and establish a connection between resolution proof size and maximum clause size.
computability; resolution lower bounds; lower bounds; pigeonhole principle; randomly generated formulas; random formulas; randomly chosen 3-CNF formula
P. Beame and T. Pitassi, "Simplified and improved resolution lower bounds," Proceedings of 37th Conference on Foundations of Computer Science(FOCS), Burlington, VT, 1996, pp. 274.