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 the normal view instead:

scientific article; zbMATH DE number 4001483
Language Label Description Also known as
default for all languages
No label defined
    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
      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
      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

      Identifiers