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.
The following three rules are applied until they can be applied no more:
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 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 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 procedure pl_dpll_split_rule/3
just chooses a literal from some clause and build two new clausal forms:
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).
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).
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).
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.
Copyright © 2014 Barry Watson. All rights reserved.