Davis-Putnam Procedure (DP)

The Davis-Putnam procedure (DP) is a technique for deciding the satisfiability of propositional formulas in clausal form. The procedure shown here is not the Davis-Putnam-Longemann-Loveland (DPLL) procedure which is a later development.

Algorithm

The following three rules are applied until they can be applied no more:

The 1-literal rule: Any clause that contains a single literal is removed along with any other clause that contains this literal. The negation of this literal is then removed from all clauses. This is also known as unit propagation.
The affirmative-negative rule: The set of all literals that occur either only positively or negatively is calculated. These literals are called pure. Any clause that contains a pure literal is deleted.
The resolution rule: A literal is chosen that occurs only positively in one clause and only negatively in another clause. We then form all resolvents for this literal and combine the result with the clauses that were not used in the resolution.

Implementation

The following code can be found in the examples directory of the Barry's Prolog distribution.

The following Prolog code in this section implements the algorithm given above. First we fix a set of operators which we will need to represent the formulas of propositional logic.

:-op(200, fy, ~).                   % Negation
:-op(0, yfx, (/\)).
:-op(400, xfy, (/\)).               % Conjunction (not ISO associativity which is yfx)
:-op(0, yfx, (\/)).
:-op(500, xfy, (\/)).               % Disjunction (not ISO associativity which is yfx)
:-op(600, xfy, =>).                 % Implication
:-op(700, xfy, <=>).                % Equivalence

The 1-literal rule

The procedure pl_dp_one_literal_rule/2 chooses a clause that contains only one literal, removes all clauses that contain this literal (pl_dp_one_literal_rule_remove_clauses/3), then removes all negations of this literal from the remaining clauses (pl_dp_one_literal_rule_remove_negated_literals/3).


	pl_negate(~A, A) :- !.
pl_negate(A, ~A).

pl_dp_one_literal_rule_remove_negated_literals([], _, []).
pl_dp_one_literal_rule_remove_negated_literals([Phi|Phis], Neg, [Psi|Psis]) :- 
	delete_all(Neg, Phi, Psi),
	!,
	pl_dp_one_literal_rule_remove_negated_literals(Phis, Neg, Psis).

pl_dp_one_literal_rule_remove_clauses([], _, []).
pl_dp_one_literal_rule_remove_clauses([Phi|Phis], P, Result) :- 
	member(P, Phi),
	!,
	pl_dp_one_literal_rule_remove_clauses(Phis, P, Result).
pl_dp_one_literal_rule_remove_clauses([Phi|Phis], P, [Phi|Result]) :- 
	pl_dp_one_literal_rule_remove_clauses(Phis, P, Result).

pl_dp_one_literal_rule(Phi, Psi) :-
	member([P], Phi),
	pl_negate(P, NegP),
	pl_dp_one_literal_rule_remove_clauses(Phi, P, Mid),
	pl_dp_one_literal_rule_remove_negated_literals(Mid, NegP, Psi).

The affirmative-negative rule

The procedure pl_dp_affirmative_negative_rule/2 finds all positive and negative pure literals. If there are no pure literals then the procedure fails. Otherwise, these literals are then used to filter out any clauses that contain them with pl_affirmitive_negative_rule_remove_clauses/3. In this implementation we make use of a library which represents sets as ordered lists. The procedure ord_subtract/3 is from this library.


	pl_affirmitive_negative_rule_remove_clauses([], _, []).
pl_affirmitive_negative_rule_remove_clauses([Phi|Phis], Pures, Result) :- 
	member(P, Pures),
	(member(P, Phi) ; member(~P, Phi)),
	!,
	pl_affirmitive_negative_rule_remove_clauses(Phis, Pures, Result).
pl_affirmitive_negative_rule_remove_clauses([Phi|Phis], Pures, [Phi|Result]) :- 
	pl_affirmitive_negative_rule_remove_clauses(Phis, Pures, Result).

pl_dp_affirmative_negative_rule(Phi, Psi) :-
	setof(Pos, Clause^(member(Clause, Phi), member(Pos, Clause), Pos \= ~_), Positives),
	setof(Neg, Clause^(member(Clause, Phi), member(~Neg, Clause)), Negatives),
	ord_subtract(Positives, Negatives, OnlyPositives),
	ord_subtract(Negatives, Positives, OnlyNegatives),
	append(OnlyPositives, OnlyNegatives, Pures),
	Pures \= [],                                                  % must have them!
	pl_affirmitive_negative_rule_remove_clauses(Phi, Pures, Psi).

The resolution rule

Here we choose a literal that occurs only positively in one clause, and only negatively in another, then we form all propositional resolvents using combine_all_pairs/3. As resolution can introduce clauses which are trivially satisfied, i.e., they contain both a positive and negative occurrence of a literal, we filter these out with a call to pl_filter_trivial. The procedure ord_union/3 is from the same library as ord_subtract/3 used earlier.


	pl_filter_trivial([], []).
pl_filter_trivial([Clause|Clauses], Result) :-
	member(Lit, Clause),
	pl_negate(Lit, NegLit),
	member(NegLit, Clause),
	!,
	pl_filter_trivial(Clauses, Result).
pl_filter_trivial([Clause|Clauses], [Clause|Result]) :-
	pl_filter_trivial(Clauses, Result).

combine_all_pairs([], S, S) :- !.
combine_all_pairs(S, [], S) :- !.
combine_all_pairs(S1, S2, S4) :- 
	combine_all_pairs(S1, S2, [], S4).

combine_all_pairs([], _, Result, Result).
combine_all_pairs([H|T], S2, Acc, Result) :-
	combine(S2, H, P),
	ord_union(P, Acc, NewAcc),
	combine_all_pairs(T, S2, NewAcc, Result).

combine([], _, []).
combine([H|T], E, [Set|Sets]) :-
	ord_union(E, H, Set),
	combine(T, E, Sets).

pl_dp_resolution_clauses([], _, _, [], [], []).
pl_dp_resolution_clauses([Clause|Clauses], Lit, NegLit, [Clause1|ResultPos], ResultNeg, Others) :-
	member(Lit, Clause),
	\+ member(NegLit, Clause),
	delete_all(Lit, Clause, Clause1),
	!,
	pl_dp_resolution_clauses(Clauses, Lit, NegLit, ResultPos, ResultNeg, Others).	
pl_dp_resolution_clauses([Clause|Clauses], Lit, NegLit, ResultPos, [Clause1|ResultNeg], Others) :-
	member(NegLit, Clause),
	\+ member(Lit, Clause),
	delete_all(NegLit, Clause, Clause1),
	!,
	pl_dp_resolution_clauses(Clauses, Lit, NegLit, ResultPos, ResultNeg, Others).	
pl_dp_resolution_clauses([Clause|Clauses], Lit, NegLit, ResultPos, ResultNeg, [Clause|Others]) :-
	pl_dp_resolution_clauses(Clauses, Lit, NegLit, ResultPos, ResultNeg, Others).	

pl_dp_resolution_rule(Clauses0, Result) :-
	del(C0, Clauses0, Clauses1),       % Choose a clause C0.
	del(Lit, C0, Alpha),               % Choose a literal from C0. 
	pl_negate(Lit, NegLit),            % Negate this literal.
	\+ member(NegLit, Alpha),          % The negated literal cannot occur in C0.
	del(C1, Clauses1, _),              % Choose another clause C1.
	del(NegLit, C1, Beta),             % The negated literal must occur in C1.
	\+ member(Lit, Beta),              % The original literal cannot occur in C1.
	!,
	pl_dp_resolution_clauses(Clauses0, Lit, NegLit, ClausesPos, ClausesNeg, ClausesOthers),
	combine_all_pairs(ClausesPos, ClausesNeg, Resolvents),   % Form all resolvants for Lit.
	ord_union(Resolvents, ClausesOthers, Mid),
	pl_filter_trivial(Mid, Result).

Entry-point

The driver for the procedure is pl_dp_loop/2. In each loop we try the 1-literal rule before the affirmative-negative rule, and we try the affirmative-negative rule before the resolution rule. We stop when no rule can be applied.


	pl_dp_loop(ClausesIn, ClausesOut) :-
	pl_dp_one_literal_rule(ClausesIn, ClausesMid),	
	!,
	pl_dp_loop(ClausesMid, ClausesOut).
pl_dp_loop(ClausesIn, ClausesOut) :-
	pl_dp_affirmative_negative_rule(ClausesIn, ClausesMid),
	!,
	pl_dp_loop(ClausesMid, ClausesOut).
pl_dp_loop(ClausesIn, ClausesOut) :-
	pl_dp_resolution_rule(ClausesIn, ClausesMid),
	!,
	pl_dp_loop(ClausesMid, ClausesOut).
pl_dp_loop(Clauses, Clauses).

Misc.

The procedure pl_dp_sat/1 succeeds if the argument, which is a formula, is satisfiable. The procedure cnf_transform/2 transforms a formula into conjunctive normal form (CNF). The procedure pl_clausal_form/2 transforms a formula in CNF into clausal form.


	pl_dp_sat(Phi) :-
	cnf_transform(Phi, CNF),
	pl_clausal_form(CNF, Clauses),
	pl_dp_loop(Clauses, []).

The procedure pl_dp_tautology/1 succeeds if the argument is a tautology, i.e. the negation of the argument is unsatisfiable.


	pl_dp_tautology(Phi) :-
	\+ pl_dp_sat(~Phi).

References

Chang, C-L, Lee, R C-T. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.
Fitting, Melvin. First-Order Logic and Automated Theorem Proving. Springer, 1990.
Harrison, John. Handbook of Practical Logic and Automated Reasoning. Cambridge, 2009.