On the relations between SAT and CSP enumerative algorithms Original Research Article

We show the equivalence between the so-called Davis–Putnam procedure (Davis et al., Comm. ACM 5 (1962) 394–397; Davis and Putnam (J. ACM 7 (1960) 201–215)) and the Forward Checking of Haralick and Elliot (Artificial Intelligence 14 (1980) 263–313). 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.