Figure 1: Basic Davis-Putnam algorithm.

algorithm DP(S)
repeat
	for each clause C in S do // tautology rule
		if C is a tautology then remove C from S;
	for each pure literal L in S do // ØL does not occur in any clause in S
		delete every clause in S which contains L
	for each unit clause L in S do
		if ØL is also a unit clause in S then return FALSE;
		delete from S every clause containing L // unit subsumption
		delete ØL from every clause in which it occurs // unit resolution
	if S is empty then return TRUE else return FALSE;
until no further changes result in S
Choose some literal L that occurs in the formula
if  DPÈS ( {L}) then return TRUE; // splitting with L; recursive call
else if DPÈS ( {ØL}) then return TRUE; // splitting with ØL
else return FALSE;