J.P. Locquet, J. Perret, et al.
SPIE Optical Science, Engineering, and Instrumentation 1998
Paper
On the complexity of regular resolution and the Davis-Putnam procedure
Abstract
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.
Related
Hang-Yip Liu, Steffen Schulze, et al.
Proceedings of SPIE - The International Society for Optical Engineering
Conference paper
A quantitative analysis of OS noise
Alessandro Morari, Roberto Gioiosa, et al.
IPDPS 2011
Arun Viswanathan, Nancy Feldman, et al.
IEEE Communications Magazine