Correction to ``Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem'' (Q1822244)
From MaRDI portal
| This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Correction to ``Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem |
scientific article; zbMATH DE number 4001483
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Correction to ``Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem'' |
scientific article; zbMATH DE number 4001483 |
Statements
Correction to ``Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem'' (English)
0 references
1987
0 references
\textit{J. Franco} and \textit{M. Paull} [ibid. 5, 77--87 (1983; Zbl 0497.68021)] have defined a family of distributions \(F\) on inputs to the Davis Putnam Procedure (DPP) and then have used this to analyze a variant, DPP', which omits the pure literal rule. The main theorem asserts that for almost all inputs, DPP' requires exponential time. Although this result is correct, the proof is not. We briefly note the errors and then correct them.
0 references
probabilistic analysis
0 references
satisfiability problem
0 references
instance distributions
0 references
Davis-Putnam procedure
0 references
polynomial average complexity
0 references
NP-completeness
0 references