Correction to ``Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem'' (Q1822244)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Correction to ``Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem'' |
scientific article |
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