Davis-Putnam-Longemann-Loveland Procedure (DPLL)

The Davis-Putnam-Longemann-Loveland procedure (DPLL) is a technique for deciding the satisfiability of propositional formulas in clausal form. The procedure shown here is a later development of the Davis-Putnam (DP) procedure. The two procedures only differ in one rule application.

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, a unit clause, 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 split rule: From the clausal form we choose a literal and form two new clausal forms: one with the addition of a unit clause with this literal, and one with the addition of a unit clause with the negation of this literal. We then recurse on these.

Implementation

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

The implementation has a great deal of code in common with the DP procedure. 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 split rule

The procedure pl_dpll_split_rule/3 just chooses a literal from some clause and build two new clausal forms:

The original clausal form with a new unit clause containing the literal.
The original clausal form with a new unit clause containing the negation of the literal.

The main loop will then recurse on both of these new clausal forms. The 1-literal rule will process this unit clause.


	pl_dpll_split_rule(ClausesIn, [[Lit]|ClausesIn], [[LitNeg]|ClausesIn]) :-
	member(Clause, ClausesIn),
	member(Lit, Clause),
	pl_negate(Lit, LitNeg).

Entry-point

The driver for the procedure is pl_dpll_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 split rule. We stop when no rule can be applied.


	pl_dpll_loop(ClausesIn, ClausesOut) :-
	pl_dp_one_literal_rule(ClausesIn, ClausesMid),	
	!,
	pl_dpll_loop(ClausesMid, ClausesOut).
pl_dpll_loop(ClausesIn, ClausesOut) :-
	pl_dp_affirmative_negative_rule(ClausesIn, ClausesMid),
	!,
	pl_dpll_loop(ClausesMid, ClausesOut).
pl_dpll_loop(ClausesIn, ClausesOut) :-
	pl_dpll_split_rule(ClausesIn, ClausesMid0, ClausesMid1),
	!,
	(pl_dpll_loop(ClausesMid0, ClausesOut)
    ;
	pl_dpll_loop(ClausesMid1, ClausesOut)
        ).
pl_dpll_loop(Clauses, Clauses).

Misc.

The procedure pl_dpll_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_dpll_sat(Phi) :-
	cnf_transform(Phi, CNF),
	pl_clausal_form(CNF, Clauses),
	pl_dpll_loop(Clauses, []).

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


	pl_dpll_tautology(Phi) :-
	\+ pl_dpll_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.