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
    0 references
    0 references
    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
    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