\input zb-basic
\input zb-ioport
\iteman{io-port 01565917}
\itemau{G\'enisson, Richard; J\'egou, Philippe}
\itemti{On the relations between SAT and CSP enumerative algorithms.}
\itemso{Discrete Appl. Math. 107, No.1-3, 27-40 (2000).}
\itemab
Summary: We show the equivalence between the so-called Davis-Putnam procedure [{\it M. Davis}, {\it G. Logemann} and {\it D. Loveland}, Commun. ACM 5, 394-397 (1962; Zbl 0217.54002); {\it M. Davis} and {\it H. Putnam}, J. ACM 7, 201-215 (1960; Zbl 0212.34203)] and the Forward Checking of {\it R. M. Haralick} and {\it G. L. Elliot} [Artif. Intell. 14, 263-313 (1980)]. Both apply the paradigm `choose and propagate' in two different formalisms, namely the propositional calculus and the constraint satisfaction problems formalism. They happen to be strictly equivalent as soon as a compatible instantiation order is chosen. This equivalence is shown considering the resolution of the clausal expression of a CSP by the Davis-Putnam procedure.
\itemrv{~}
\itemcc{}
\itemut{Davis-Putnam procedure; Forward Checking; propositional calculus; constraint satisfaction}
\itemli{doi:10.1016/S0166-218X(99)00205-X}
\end