An exponential lower bound for the pure literal rule (Q1104093): Difference between revisions

A pure literal is a literal in a logic formula (usually in conjective normal form) that occurs only positively or only negatively. The Davis- Putnam procedure [cf. \textit{M. Davis, G. Logemann} and \textit{D. Loveland}, Commun. ACM 5, 394-397 (1962; Zbl 0217.540)] was developed to find one solution to a logic formula, and it contains several techniques for speeding up the typical solution time. One of these techniques is the pure literal rule: a variable that occurs only positively or only negatively (a pure literal) needs to have only one value considered, the value that makes all of its clauses true. To facilitate average time analysis, \textit{A. Goldberg} [(*)\ Average case complexity of the satisfiability problem, Proc. 4th Workshop Autom. Deduction, 1-6 (1979)] developed a simplified algorithm which consisted of just splitting (trying each value for a variable, simplifying the resulting subproblems, and considering each subproblem recursively) and the pure literal rule. The running time for this pure literal rule algorithm gives an upper bound for the running time of the full Davis- Putnam procedure. The pure literal rule algorithm takes polynomial average time for some random sets of problems [(*) and \textit{A. Goldberg, P. Purdom} and \textit{C. Brown}, Inf. Process. Lett. 15, 72-75 (1982; Zbl 0529.68065), ibid. 16, 213 (1983; Zbl 0545.68080)]. A detailed upper bound analysis [(**)\ \textit{P. W. Purdom} jun. and \textit{C. A. Brown}, SIAM J. Comput. 14, 943-953 (1985; Zbl 0575.68060)] showed that there was an extensive region where the average time is polynomial. This paper has the first lower bound analysis for this algorithm. We show that there is also an extensive region where the average time for this algorithm is exponential. In many cases, the current lower bound is much lower than the best upper bound (**). (We are writing up an improved analysis which shows that true behavior of the algorithm is close to the upper bound in (**) when the average clause length is not too large.)