An exponential lower bound for the pure literal rule (Q1104093): Difference between revisions
From MaRDI portal
Set profile property. |
ReferenceBot (talk | contribs) Changed an Item |
||
(One intermediate revision by one other user not shown) | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/0020-0190(88)90028-2 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2076029782 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A machine program for theorem-proving / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Corrigendum to ``Average time analyses of simplified Davis-Putnam procedures'' / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5585020 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Polynomial-average-time satisfiability problems / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The Pure Literal Rule and Polynomial Average Time / rank | |||
Normal rank |
Latest revision as of 17:39, 18 June 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | An exponential lower bound for the pure literal rule |
scientific article |
Statements
An exponential lower bound for the pure literal rule (English)
0 references
1988
0 references
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.)
0 references
Davis-Putnam procedure
0 references
pure literal rule
0 references
average time analysis
0 references