Davis-Putnam-Verfahren

Das Davis-Putnam-Verfahren (nach Martin Davis und Hilary Putnam) entscheidet über die Unerfüllbarkeit einer aussagenlogischen Formel in konjunktiver Normalform. Das Verfahren sollte nicht mit der Weiterentwicklung, dem DPLL (Davis-Putnam-Logemann-Loveland)-Algorithmus, verwechselt werden.