A. Gupta, R. Gross, et al.
SPIE Advances in Semiconductors and Superconductors 1990
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.
A. Gupta, R. Gross, et al.
SPIE Advances in Semiconductors and Superconductors 1990
Maciel Zortea, Miguel Paredes, et al.
IGARSS 2021
Michael D. Moffitt
ICCAD 2009
Nanda Kambhatla
ACL 2004