An exponential lower bound for the pure literal rule
type: Item
instance of: scholarly article
title: An exponential lower bound for the pure literal rule
zbMATH Open document ID: 0646.68061
DOI: 10.1016/0020-0190(88)90028-2
author: Khaled M. Bugrara
author: Paul Walton jun. Purdom
published in: Information Processing Letters
publication date: 1988-01-01T00:00:00Z
review text: 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 cl…
Mathematics Subject Classification ID: 68Q25
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 4055047
zbMATH Keywords: Davis-Putnam procedure
zbMATH Keywords: pure literal rule
zbMATH Keywords: average time analysis
MaRDI profile type: Publication
full work available at URL: 0020-0190(88)90028-2
OpenAlex ID: W2076029782
cites work: A machine program for theorem-proving
cites work: Corrigendum to ``Average time analyses of simplified Davis-Putnam procedures''
cites work: Q5585020
cites work: Polynomial-average-time satisfiability problems
cites work: The Pure Literal Rule and Polynomial Average Time
description: scientific article; zbMATH DE number 4055047