Conference paper
Some experimental results on placement techniques
Maurice Hanan, Peter K. Wolff, et al.
DAC 1976
For infinitely many n > 0 we construct contradictory formulas αn in conjunctive form with n literals such that every regular proof tree which proves the contradiction must contain 2cn distinct clauses for some c > 0. This implies a 2cn lower bound for the number of distinct clauses which are generated by the Davis-Putnam procedure applied to αn using any order of variable elimination. © 1977.
Maurice Hanan, Peter K. Wolff, et al.
DAC 1976
Hang-Yip Liu, Steffen Schulze, et al.
Proceedings of SPIE - The International Society for Optical Engineering
Marshall W. Bern, Howard J. Karloff, et al.
Theoretical Computer Science
Michael C. McCord, Violetta Cavalli-Sforza
ACL 2007