Correction to ``Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem''
type: Item
instance of: scholarly article
title: Correction to ``Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem''
zbMATH Open document ID: 0617.68046
DOI: 10.1016/0166-218X(87)90032-1
author: John W. Rosenthal
author: John V. Franco
author: J. M. Plotkin
published in: Discrete Applied Mathematics
publication date: 1987-01-01T00:00:00Z
review text: \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.
Mathematics Subject Classification ID: 68Q25
Mathematics Subject Classification ID: 68Q17
zbMATH DE Number: 4001483
zbMATH Keywords: probabilistic analysis
zbMATH Keywords: satisfiability problem
zbMATH Keywords: instance distributions
zbMATH Keywords: Davis-Putnam procedure
zbMATH Keywords: polynomial average complexity
zbMATH Keywords: NP-completeness
MaRDI profile type: Publication
cites work: Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
full work available at URL: 0166-218x(87)90032-1
OpenAlex ID: W2055638404
description: scientific article; zbMATH DE number 4001483